mathlib3 documentation

order.category.HeytAlg

The category of Heyting algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines HeytAlg, the category of Heyting algebras.

source
def HeytAlg  :
Type (u_1+1)

The category of Heyting algebras.

Equations
Instances for HeytAlg
source
@[protected, instance]
def HeytAlg.has_coe_to_sort  :
has_coe_to_sort HeytAlg (Type u_1)
Equations
source
@[protected, instance]
def HeytAlg.heyting_algebra (X : HeytAlg) :
heyting_algebra ↥X
Equations
source
def HeytAlg.of (α : Type u_1) [heyting_algebra α] :
HeytAlg

Construct a bundled HeytAlg from a heyting_algebra.

Equations
source
@[simp]
theorem HeytAlg.coe_of (α : Type u_1) [heyting_algebra α] :
↥(HeytAlg.of α) = α
source
@[protected, instance]
def HeytAlg.inhabited  :
inhabited HeytAlg
Equations
source
@[protected, instance]
def HeytAlg.bundled_hom  :
category_theory.bundled_hom heyting_hom
Equations
source
@[protected, instance]
def HeytAlg.large_category  :
category_theory.large_category HeytAlg
source
@[protected, instance]
def HeytAlg.concrete_category  :
category_theory.concrete_category HeytAlg
source
@[simp]
theorem HeytAlg.has_forget_to_Lat_forget₂_map (X Y : HeytAlg) (f : X ⟶ Y) :
category_theory.has_forget₂.forget₂.map f = ↑f
source
@[simp]
theorem HeytAlg.has_forget_to_Lat_forget₂_obj (X : HeytAlg) :
category_theory.has_forget₂.forget₂.obj X = BddDistLat.of ↥X
source
@[protected, instance]
def HeytAlg.has_forget_to_Lat  :
category_theory.has_forget₂ HeytAlg BddDistLat
Equations
source
@[simp]
theorem HeytAlg.iso.mk_hom {α β : HeytAlg} (e : ↥α ≃o ↥β) :
(HeytAlg.iso.mk e).hom = ↑e
source
@[simp]
theorem HeytAlg.iso.mk_inv {α β : HeytAlg} (e : ↥α ≃o ↥β) :
(HeytAlg.iso.mk e).inv = ↑(e.symm)
source
def HeytAlg.iso.mk {α β : HeytAlg} (e : ↥α ≃o ↥β) :
α ≅ β

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

Equations