The category of Heyting algebras

This file defines HeytAlg, the category of Heyting algebras.

structure HeytAlg : Type (u_1 + 1)

The category of Heyting algebras.

• carrier : Type u_1

  The underlying Heyting algebra.

• str : HeytingAlgebra ↑self

@[implicit_reducible]

instance HeytAlg.instCoeSortType : CoeSort HeytAlg (Type u_1)

@[reducible, inline]

abbrev HeytAlg.of (X : Type u_1) [HeytingAlgebra X] : HeytAlg

Construct a bundled HeytAlg from the underlying type and typeclass.

structure HeytAlg.Hom (X Y : HeytAlg) : Type u

The type of morphisms in HeytAlg R.

• hom' : HeytingHom ↑X ↑Y

  The underlying HeytingHom.

theorem HeytAlg.Hom.ext {X Y : HeytAlg} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

theorem HeytAlg.Hom.ext_iff {X Y : HeytAlg} {x y : X.Hom Y} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

instance HeytAlg.instCategory : CategoryTheory.Category.{u, u + 1} HeytAlg

@[implicit_reducible]

instance HeytAlg.instConcreteCategoryHeytingHomCarrier : CategoryTheory.ConcreteCategory HeytAlg fun (x1 x2 : HeytAlg) => HeytingHom ↑x1 ↑x2

@[reducible, inline]

abbrev HeytAlg.Hom.hom {X Y : HeytAlg} (f : X.Hom Y) : HeytingHom ↑X ↑Y

Turn a morphism in HeytAlg back into a HeytingHom.

@[reducible, inline]

abbrev HeytAlg.ofHom {X Y : Type u} [HeytingAlgebra X] [HeytingAlgebra Y] (f : HeytingHom X Y) : of X ⟶ of Y

Typecheck a HeytingHom as a morphism in HeytAlg.

def HeytAlg.Hom.Simps.hom (X Y : HeytAlg) (f : X.Hom Y) : HeytingHom ↑X ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem HeytAlg.coe_id {X : HeytAlg} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem HeytAlg.coe_comp {X Y Z : HeytAlg} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem HeytAlg.forget_map {X Y : HeytAlg} (f : X ⟶ Y) : (CategoryTheory.forget HeytAlg).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem HeytAlg.ext {X Y : HeytAlg} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem HeytAlg.ext_iff {X Y : HeytAlg} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem HeytAlg.coe_of (X : Type u) [HeytingAlgebra X] : ↑(of X) = X

@[simp]

theorem HeytAlg.hom_id {X : HeytAlg} : Hom.hom (CategoryTheory.CategoryStruct.id X) = HeytingHom.id ↑X

theorem HeytAlg.id_apply (X : HeytAlg) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem HeytAlg.hom_comp {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem HeytAlg.comp_apply {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem HeytAlg.hom_ext {X Y : HeytAlg} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem HeytAlg.hom_ext_iff {X Y : HeytAlg} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem HeytAlg.hom_ofHom {X Y : Type u} [HeytingAlgebra X] [HeytingAlgebra Y] (f : HeytingHom X Y) : Hom.hom (ofHom f) = f

@[simp]

theorem HeytAlg.ofHom_hom {X Y : HeytAlg} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem HeytAlg.ofHom_id {X : Type u} [HeytingAlgebra X] : ofHom (HeytingHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem HeytAlg.ofHom_comp {X Y Z : Type u} [HeytingAlgebra X] [HeytingAlgebra Y] [HeytingAlgebra Z] (f : HeytingHom X Y) (g : HeytingHom Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem HeytAlg.ofHom_apply {X Y : Type u} [HeytingAlgebra X] [HeytingAlgebra Y] (f : HeytingHom X Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem HeytAlg.inv_hom_apply {X Y : HeytAlg} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem HeytAlg.hom_inv_apply {X Y : HeytAlg} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

@[implicit_reducible]

instance HeytAlg.instInhabited : Inhabited HeytAlg

@[implicit_reducible]

instance HeytAlg.hasForgetToLat : CategoryTheory.HasForget₂ HeytAlg BddDistLat

@[simp]

theorem HeytAlg.hasForgetToLat_forget₂_obj_carrier (X : HeytAlg) : ↑(CategoryTheory.HasForget₂.forget₂.obj X).toDistLat = ↑X

@[simp]

theorem HeytAlg.hasForgetToLat_forget₂_map {X✝ Y✝ : HeytAlg} (f : X✝ ⟶ Y✝) : CategoryTheory.HasForget₂.forget₂.map f = BddDistLat.ofHom (have __src := { toFun := ⇑(Hom.hom f), map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑(Hom.hom f), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })

@[simp]

theorem HeytAlg.hasForgetToLat_forget₂_obj_str (X : HeytAlg) : (CategoryTheory.HasForget₂.forget₂.obj X).str = GeneralizedHeytingAlgebra.toDistribLattice

@[simp]

theorem HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder (X : HeytAlg) : (CategoryTheory.HasForget₂.forget₂.obj X).isBoundedOrder = HeytingAlgebra.toBoundedOrder

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

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

@[simp]

theorem HeytAlg.Iso.mk_hom {α β : HeytAlg} (e : ↑α ≃o ↑β) : (mk e).hom = ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }

@[simp]

theorem HeytAlg.Iso.mk_inv {α β : HeytAlg} (e : ↑α ≃o ↑β) : (mk e).inv = ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }