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.instCoeSortType : CoeSort HeytAlg (Type u_1)

Equations

• HeytAlg.instCoeSortType = CategoryTheory.Bundled.coeSort

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

Equations

• X.instHeytingAlgebraα = 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 α] : ↑(of α) = α

instance HeytAlg.instInhabited : Inhabited HeytAlg

Equations

• HeytAlg.instInhabited = { default := HeytAlg.of PUnit.{?u.3 + 1} }

instance HeytAlg.bundledHom : CategoryTheory.BundledHom HeytingHom

Equations

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

instance instHeytAlgLargeCategory : CategoryTheory.LargeCategory HeytAlg

Equations

• instHeytAlgLargeCategory = CategoryTheory.BundledHom.category HeytingHom

instance HeytAlg.instHasForget : CategoryTheory.HasForget HeytAlg

Equations

• HeytAlg.instHasForget = id inferInstance

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

Equations

• HeytAlg.instFunLikeHomαHeytingAlgebra = HeytingHom.instFunLike

instance HeytAlg.instHeytingHomClassHomαHeytingAlgebra {X Y : HeytAlg} : HeytingHomClass (X ⟶ Y) ↑X ↑Y

instance HeytAlg.hasForgetToLat : CategoryTheory.HasForget₂ HeytAlg BddDistLat

Equations

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

@[simp]

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

@[simp]

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

def HeytAlg.Iso.mk {α β : 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.

@[simp]

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

@[simp]

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