The categories of semilattices #
This defines SemilatticeSup
and SemilatticeInf
, the categories of sup-semilattices with a bottom
element and inf-semilattices with a top element.
References #
- X : Type ?
- is_semilattice_sup : semilattice_sup self.X
- is_order_bot : order_bot self.X
The category of sup-semilattices with a bottom element.
Instances for SemilatticeSup
- X : Type ?
- is_semilattice_inf : semilattice_inf self.X
- is_order_top : order_top self.X
The category of inf-semilattices with a top element.
Instances for SemilatticeInf
@[protected, instance]
Equations
Construct a bundled SemilatticeSup
from a semilattice_sup
.
Equations
@[simp]
theorem
SemilatticeSup.coe_of
(α : Type u_1)
[semilattice_sup α]
[order_bot α] :
↥(SemilatticeSup.of α) = α
@[protected, instance]
@[protected, instance]
Equations
- SemilatticeSup.category_theory.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : SemilatticeSup), sup_bot_hom ↥X ↥Y}, id := λ (X : SemilatticeSup), sup_bot_hom.id ↥X, comp := λ (X Y Z : SemilatticeSup) (f : X ⟶ Y) (g : Y ⟶ Z), sup_bot_hom.comp g f}, id_comp' := SemilatticeSup.category_theory.large_category._proof_1, comp_id' := SemilatticeSup.category_theory.large_category._proof_2, assoc' := SemilatticeSup.category_theory.large_category._proof_3}
@[protected, instance]
Equations
- SemilatticeSup.category_theory.concrete_category = category_theory.concrete_category.mk {obj := SemilatticeSup.X, map := λ (X Y : SemilatticeSup), coe_fn, map_id' := SemilatticeSup.category_theory.concrete_category._proof_1, map_comp' := SemilatticeSup.category_theory.concrete_category._proof_2}
@[protected, instance]
Equations
- SemilatticeSup.has_forget_to_PartialOrder = {forget₂ := {obj := λ (X : SemilatticeSup), {α := ↥X, str := semilattice_sup.to_partial_order ↥X X.is_semilattice_sup}, map := λ (X Y : SemilatticeSup) (f : X ⟶ Y), ↑f, map_id' := SemilatticeSup.has_forget_to_PartialOrder._proof_1, map_comp' := SemilatticeSup.has_forget_to_PartialOrder._proof_2}, forget_comp := SemilatticeSup.has_forget_to_PartialOrder._proof_3}
@[simp]
@[protected, instance]
Equations
Construct a bundled SemilatticeInf
from a semilattice_inf
.
Equations
@[simp]
theorem
SemilatticeInf.coe_of
(α : Type u_1)
[semilattice_inf α]
[order_top α] :
↥(SemilatticeInf.of α) = α
@[protected, instance]
@[protected, instance]
Equations
- SemilatticeInf.category_theory.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : SemilatticeInf), inf_top_hom ↥X ↥Y}, id := λ (X : SemilatticeInf), inf_top_hom.id ↥X, comp := λ (X Y Z : SemilatticeInf) (f : X ⟶ Y) (g : Y ⟶ Z), inf_top_hom.comp g f}, id_comp' := SemilatticeInf.category_theory.large_category._proof_1, comp_id' := SemilatticeInf.category_theory.large_category._proof_2, assoc' := SemilatticeInf.category_theory.large_category._proof_3}
@[protected, instance]
Equations
- SemilatticeInf.category_theory.concrete_category = category_theory.concrete_category.mk {obj := SemilatticeInf.X, map := λ (X Y : SemilatticeInf), coe_fn, map_id' := SemilatticeInf.category_theory.concrete_category._proof_1, map_comp' := SemilatticeInf.category_theory.concrete_category._proof_2}
@[protected, instance]
Equations
- SemilatticeInf.has_forget_to_PartialOrder = {forget₂ := {obj := λ (X : SemilatticeInf), {α := ↥X, str := semilattice_inf.to_partial_order ↥X X.is_semilattice_inf}, map := λ (X Y : SemilatticeInf) (f : X ⟶ Y), ↑f, map_id' := SemilatticeInf.has_forget_to_PartialOrder._proof_1, map_comp' := SemilatticeInf.has_forget_to_PartialOrder._proof_2}, forget_comp := SemilatticeInf.has_forget_to_PartialOrder._proof_3}
@[simp]
Order dual #
Constructs an isomorphism of lattices from an order isomorphism between them.
Equations
- SemilatticeSup.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
SemilatticeSup.iso.mk_inv
{α β : SemilatticeSup}
(e : ↥α ≃o ↥β) :
(SemilatticeSup.iso.mk e).inv = ↑(e.symm)
@[simp]
theorem
SemilatticeSup.iso.mk_hom
{α β : SemilatticeSup}
(e : ↥α ≃o ↥β) :
(SemilatticeSup.iso.mk e).hom = ↑e
order_dual
as a functor.
Equations
- SemilatticeSup.dual = {obj := λ (X : SemilatticeSup), SemilatticeInf.of (↥X)ᵒᵈ, map := λ (X Y : SemilatticeSup), ⇑sup_bot_hom.dual, map_id' := SemilatticeSup.dual._proof_1, map_comp' := SemilatticeSup.dual._proof_2}
@[simp]
@[simp]
@[simp]
theorem
SemilatticeInf.iso.mk_inv
{α β : SemilatticeInf}
(e : ↥α ≃o ↥β) :
(SemilatticeInf.iso.mk e).inv = ↑(e.symm)
@[simp]
theorem
SemilatticeInf.iso.mk_hom
{α β : SemilatticeInf}
(e : ↥α ≃o ↥β) :
(SemilatticeInf.iso.mk e).hom = ↑e
Constructs an isomorphism of lattices from an order isomorphism between them.
Equations
- SemilatticeInf.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
order_dual
as a functor.
Equations
- SemilatticeInf.dual = {obj := λ (X : SemilatticeInf), SemilatticeSup.of (↥X)ᵒᵈ, map := λ (X Y : SemilatticeInf), ⇑inf_top_hom.dual, map_id' := SemilatticeInf.dual._proof_1, map_comp' := SemilatticeInf.dual._proof_2}
@[simp]
@[simp]
The equivalence between SemilatticeSup
and SemilatticeInf
induced by order_dual
both ways.
Equations
- SemilatticeSup_equiv_SemilatticeInf = category_theory.equivalence.mk SemilatticeSup.dual SemilatticeInf.dual (category_theory.nat_iso.of_components (λ (X : SemilatticeSup), SemilatticeSup.iso.mk (order_iso.dual_dual ↥X)) SemilatticeSup_equiv_SemilatticeInf._proof_1) (category_theory.nat_iso.of_components (λ (X : SemilatticeInf), SemilatticeInf.iso.mk (order_iso.dual_dual ↥X)) SemilatticeSup_equiv_SemilatticeInf._proof_2)