The category of Heyting algebras

This file defines HeytAlg, the category of Heyting algebras.

def HeytAlg : Type (u_1 + 1)

The category of Heyting algebras.

Equations

• HeytAlg = CategoryTheory.Bundled HeytingAlgebra

instance HeytAlg.instCoeSortHeytAlgType : CoeSort HeytAlg (Type u_1)

Equations

• HeytAlg.instCoeSortHeytAlgType = CategoryTheory.Bundled.coeSort

instance HeytAlg.instHeytingAlgebraα (X : HeytAlg) : HeytingAlgebra ↑X

Equations

• HeytAlg.instHeytingAlgebraα X = X.str

def HeytAlg.of (α : Type u_1) [HeytingAlgebra α] : HeytAlg

Construct a bundled HeytAlg from a HeytingAlgebra.

Equations

• HeytAlg.of α = CategoryTheory.Bundled.of α

@[simp]

theorem HeytAlg.coe_of (α : Type u_1) [HeytingAlgebra α] : ↑(HeytAlg.of α) = α

instance HeytAlg.instInhabitedHeytAlg : Inhabited HeytAlg

Equations

• HeytAlg.instInhabitedHeytAlg = { default := HeytAlg.of PUnit.{u_1 + 1} }

instance HeytAlg.bundledHom : CategoryTheory.BundledHom HeytingHom

Equations

• HeytAlg.bundledHom = CategoryTheory.BundledHom.mk (fun (α β : Type u_1) [HeytingAlgebra α] [HeytingAlgebra β] => DFunLike.coe) HeytingHom.id @HeytingHom.comp

instance HeytAlg.instConcreteCategoryHeytAlgInstHeytAlgLargeCategory : CategoryTheory.ConcreteCategory HeytAlg

Equations

• HeytAlg.instConcreteCategoryHeytAlgInstHeytAlgLargeCategory = id inferInstance

instance HeytAlg.instFunLikeHomHeytAlgToQuiverToCategoryStructInstHeytAlgLargeCategoryαHeytingAlgebra {X : HeytAlg} {Y : HeytAlg} : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• HeytAlg.instFunLikeHomHeytAlgToQuiverToCategoryStructInstHeytAlgLargeCategoryαHeytingAlgebra = HeytingHom.instFunLike

instance HeytAlg.instHeytingHomClassHomHeytAlgToQuiverToCategoryStructInstHeytAlgLargeCategoryαHeytingAlgebraInstHeytingAlgebraαInstFunLikeHomHeytAlgToQuiverToCategoryStructInstHeytAlgLargeCategoryαHeytingAlgebra {X : HeytAlg} {Y : HeytAlg} : HeytingHomClass (X ⟶ Y) ↑X ↑Y

Equations

• (_ : HeytingHomClass (X ⟶ Y) ↑X ↑Y) = (_ : HeytingHomClass (HeytingHom ↑X ↑Y) ↑X ↑Y)

@[simp]

theorem HeytAlg.hasForgetToLat_forget₂_obj (X : HeytAlg) : CategoryTheory.HasForget₂.forget₂.toPrefunctor.obj X = BddDistLat.of ↑X

@[simp]

theorem HeytAlg.hasForgetToLat_forget₂_map_toLatticeHom_toSupHom_toFun {X : HeytAlg} {Y : HeytAlg} (f : X ⟶ Y) (a : ↑X) : (CategoryTheory.HasForget₂.forget₂.toPrefunctor.map f).toSupHom a = f a

instance HeytAlg.hasForgetToLat : CategoryTheory.HasForget₂ HeytAlg BddDistLat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HeytAlg.Iso.mk_inv_toFun {α : HeytAlg} {β : HeytAlg} (e : ↑α ≃o ↑β) (a : ↑β) : (HeytAlg.Iso.mk e).inv a = (OrderIso.symm e) a

@[simp]

theorem HeytAlg.Iso.mk_hom_toFun {α : HeytAlg} {β : HeytAlg} (e : ↑α ≃o ↑β) (a : ↑α) : (HeytAlg.Iso.mk e).hom a = e a

def HeytAlg.Iso.mk {α : HeytAlg} {β : HeytAlg} (e : ↑α ≃o ↑β) : α ≅ β

Constructs an isomorphism of Heyting algebras from an order isomorphism between them.

Equations

• One or more equations did not get rendered due to their size.