The category of bounded lattices #
This file defines BddLat
, the category of bounded lattices.
In literature, this is sometimes called Lat
, the category of lattices, because being a lattice is
understood to entail having a bottom and a top element.
- to_Lat : Lat
- is_bounded_order : bounded_order ↥(self.to_Lat)
The category of bounded lattices with bounded lattice morphisms.
Instances for BddLat
- BddLat.has_sizeof_inst
- BddLat.has_coe_to_sort
- BddLat.inhabited
- BddLat.category_theory.large_category
- BddLat.category_theory.concrete_category
- BddLat.has_forget_to_BddOrd
- BddLat.has_forget_to_Lat
- BddLat.has_forget_to_SemilatSup
- BddLat.has_forget_to_SemilatInf
- BddDistLat.has_forget_to_BddLat
- CompleteLat.has_forget_to_BddLat
@[protected, instance]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
- BddLat.category_theory.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : BddLat), bounded_lattice_hom ↥X ↥Y}, id := λ (X : BddLat), bounded_lattice_hom.id ↥X, comp := λ (X Y Z : BddLat) (f : X ⟶ Y) (g : Y ⟶ Z), bounded_lattice_hom.comp g f}, id_comp' := BddLat.category_theory.large_category._proof_1, comp_id' := BddLat.category_theory.large_category._proof_2, assoc' := BddLat.category_theory.large_category._proof_3}
@[protected, instance]
Equations
- BddLat.category_theory.concrete_category = category_theory.concrete_category.mk {obj := coe_sort BddLat.has_coe_to_sort, map := λ (X Y : BddLat), coe_fn, map_id' := BddLat.category_theory.concrete_category._proof_1, map_comp' := BddLat.category_theory.concrete_category._proof_2}
@[protected, instance]
Equations
- BddLat.has_forget_to_BddOrd = {forget₂ := {obj := λ (X : BddLat), BddOrd.of ↥X, map := λ (X Y : BddLat), bounded_lattice_hom.to_bounded_order_hom, map_id' := BddLat.has_forget_to_BddOrd._proof_1, map_comp' := BddLat.has_forget_to_BddOrd._proof_2}, forget_comp := BddLat.has_forget_to_BddOrd._proof_3}
@[protected, instance]
Equations
@[protected, instance]
Equations
- BddLat.has_forget_to_SemilatSup = {forget₂ := {obj := λ (X : BddLat), SemilatSup.mk ↥X, map := λ (X Y : BddLat), bounded_lattice_hom.to_sup_bot_hom, map_id' := BddLat.has_forget_to_SemilatSup._proof_1, map_comp' := BddLat.has_forget_to_SemilatSup._proof_2}, forget_comp := BddLat.has_forget_to_SemilatSup._proof_3}
@[protected, instance]
Equations
- BddLat.has_forget_to_SemilatInf = {forget₂ := {obj := λ (X : BddLat), SemilatInf.mk ↥X, map := λ (X Y : BddLat), bounded_lattice_hom.to_inf_top_hom, map_id' := BddLat.has_forget_to_SemilatInf._proof_1, map_comp' := BddLat.has_forget_to_SemilatInf._proof_2}, forget_comp := BddLat.has_forget_to_SemilatInf._proof_3}
@[simp]
@[simp]
@[simp]
theorem
BddLat.coe_forget_to_SemilatSup
(X : BddLat) :
↥((category_theory.forget₂ BddLat SemilatSup).obj X) = ↥X
@[simp]
theorem
BddLat.coe_forget_to_SemilatInf
(X : BddLat) :
↥((category_theory.forget₂ BddLat SemilatInf).obj X) = ↥X
Constructs an equivalence between bounded lattices from an order isomorphism between them.
Equations
- BddLat.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
order_dual
as a functor.
The equivalence between BddLat
and itself induced by order_dual
both ways.
Equations
- BddLat.dual_equiv = category_theory.equivalence.mk BddLat.dual BddLat.dual (category_theory.nat_iso.of_components (λ (X : BddLat), BddLat.iso.mk (order_iso.dual_dual ↥X)) BddLat.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : BddLat), BddLat.iso.mk (order_iso.dual_dual ↥X)) BddLat.dual_equiv._proof_2)
The functor that adds a bottom and a top element to a lattice. This is the free functor.
Lat_to_BddLat
is left adjoint to the forgetful functor, meaning it is the free
functor from Lat
to BddLat
.
Equations
- Lat_to_BddLat_forget_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Lat) (Y : BddLat), {to_fun := λ (f : Lat_to_BddLat.obj X ⟶ Y), {to_sup_hom := {to_fun := ⇑f ∘ option.some ∘ option.some, map_sup' := _}, map_inf' := _}, inv_fun := lattice_hom.with_top_with_bot' Y.is_bounded_order, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Lat_to_BddLat_forget_adjunction._proof_5, hom_equiv_naturality_right' := Lat_to_BddLat_forget_adjunction._proof_6}
@[simp]
theorem
Lat_to_BddLat_comp_dual_iso_dual_comp_Lat_to_BddLat_inv_app_to_lattice_hom_to_sup_hom
(X : Lat) :
(Lat_to_BddLat_comp_dual_iso_dual_comp_Lat_to_BddLat.inv.app X).to_lattice_hom.to_sup_hom = (⇑lattice_hom.dual ((Lat_to_BddLat_forget_adjunction.comp BddLat.dual_equiv.to_adjunction).unit.app X) ≫ ⇑lattice_hom.dual ((category_theory.forget₂ BddLat Lat).map (⇑bounded_lattice_hom.dual (𝟙 (BddLat.of (↥(Lat_to_BddLat.obj X))ᵒᵈ)))) ≫ Lat.dual_equiv.to_adjunction.counit.app ((category_theory.forget₂ BddLat Lat).obj (BddLat.of (↥(Lat_to_BddLat.obj X))ᵒᵈ))).to_sup_hom.with_bot'.to_sup_hom.with_top'
Lat_to_BddLat
and order_dual
commute.
@[simp]
theorem
Lat_to_BddLat_comp_dual_iso_dual_comp_Lat_to_BddLat_hom_app_to_lattice_hom
(X : Lat) :
(Lat_to_BddLat_comp_dual_iso_dual_comp_Lat_to_BddLat.hom.app X).to_lattice_hom = (BddLat.dual_equiv.counit_iso.hom.app (Lat_to_BddLat.obj (Lat.of (↥X)ᵒᵈ))).to_lattice_hom.comp (⇑lattice_hom.dual (Lat_to_BddLat.map ((Lat.dual_equiv.to_adjunction.comp Lat_to_BddLat_forget_adjunction).unit.app X) ≫ Lat_to_BddLat_forget_adjunction.counit.app (BddLat.dual.obj ((Lat.dual ⋙ Lat_to_BddLat).obj X)) ≫ ⇑bounded_lattice_hom.dual (𝟙 (Lat_to_BddLat.obj (Lat.of (↥X)ᵒᵈ)))).to_lattice_hom)