The category of bounded lattices #
This file defines BoundedLattice
, 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_Lattice : Lattice
- is_bounded_order : bounded_order ↥(self.to_Lattice)
The category of bounded lattices with bounded lattice morphisms.
Instances for BoundedLattice
- BoundedLattice.has_sizeof_inst
- BoundedLattice.has_coe_to_sort
- BoundedLattice.inhabited
- BoundedLattice.category_theory.large_category
- BoundedLattice.category_theory.concrete_category
- BoundedLattice.has_forget_to_BoundedOrder
- BoundedLattice.has_forget_to_Lattice
- BoundedLattice.has_forget_to_SemilatticeSup
- BoundedLattice.has_forget_to_SemilatticeInf
- BoundedDistribLattice.has_forget_to_BoundedLattice
- CompleteLattice.has_forget_to_BoundedLattice
@[protected, instance]
Equations
- BoundedLattice.has_coe_to_sort = {coe := λ (X : BoundedLattice), ↥(X.to_Lattice)}
@[protected, instance]
Equations
- X.lattice = X.to_Lattice.str
Construct a bundled BoundedLattice
from lattice
+ bounded_order
.
Equations
- BoundedLattice.of α = BoundedLattice.mk {α := α, str := _inst_1}
@[simp]
theorem
BoundedLattice.coe_of
(α : Type u_1)
[lattice α]
[bounded_order α] :
↥(BoundedLattice.of α) = α
@[protected, instance]
@[protected, instance]
Equations
- BoundedLattice.category_theory.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : BoundedLattice), bounded_lattice_hom ↥X ↥Y}, id := λ (X : BoundedLattice), bounded_lattice_hom.id ↥X, comp := λ (X Y Z : BoundedLattice) (f : X ⟶ Y) (g : Y ⟶ Z), bounded_lattice_hom.comp g f}, id_comp' := BoundedLattice.category_theory.large_category._proof_1, comp_id' := BoundedLattice.category_theory.large_category._proof_2, assoc' := BoundedLattice.category_theory.large_category._proof_3}
@[protected, instance]
Equations
- BoundedLattice.category_theory.concrete_category = category_theory.concrete_category.mk {obj := coe_sort BoundedLattice.has_coe_to_sort, map := λ (X Y : BoundedLattice), coe_fn, map_id' := BoundedLattice.category_theory.concrete_category._proof_1, map_comp' := BoundedLattice.category_theory.concrete_category._proof_2}
@[protected, instance]
Equations
- BoundedLattice.has_forget_to_BoundedOrder = {forget₂ := {obj := λ (X : BoundedLattice), BoundedOrder.of ↥X, map := λ (X Y : BoundedLattice), bounded_lattice_hom.to_bounded_order_hom, map_id' := BoundedLattice.has_forget_to_BoundedOrder._proof_1, map_comp' := BoundedLattice.has_forget_to_BoundedOrder._proof_2}, forget_comp := BoundedLattice.has_forget_to_BoundedOrder._proof_3}
@[protected, instance]
Equations
- BoundedLattice.has_forget_to_Lattice = {forget₂ := {obj := λ (X : BoundedLattice), {α := ↥X, str := X.lattice}, map := λ (X Y : BoundedLattice), bounded_lattice_hom.to_lattice_hom, map_id' := BoundedLattice.has_forget_to_Lattice._proof_1, map_comp' := BoundedLattice.has_forget_to_Lattice._proof_2}, forget_comp := BoundedLattice.has_forget_to_Lattice._proof_3}
@[protected, instance]
Equations
- BoundedLattice.has_forget_to_SemilatticeSup = {forget₂ := {obj := λ (X : BoundedLattice), SemilatticeSup.mk ↥X, map := λ (X Y : BoundedLattice), bounded_lattice_hom.to_sup_bot_hom, map_id' := BoundedLattice.has_forget_to_SemilatticeSup._proof_1, map_comp' := BoundedLattice.has_forget_to_SemilatticeSup._proof_2}, forget_comp := BoundedLattice.has_forget_to_SemilatticeSup._proof_3}
@[protected, instance]
Equations
- BoundedLattice.has_forget_to_SemilatticeInf = {forget₂ := {obj := λ (X : BoundedLattice), SemilatticeInf.mk ↥X, map := λ (X Y : BoundedLattice), bounded_lattice_hom.to_inf_top_hom, map_id' := BoundedLattice.has_forget_to_SemilatticeInf._proof_1, map_comp' := BoundedLattice.has_forget_to_SemilatticeInf._proof_2}, forget_comp := BoundedLattice.has_forget_to_SemilatticeInf._proof_3}
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
BoundedLattice.iso.mk_hom
{α β : BoundedLattice}
(e : ↥α ≃o ↥β) :
(BoundedLattice.iso.mk e).hom = ↑e
@[simp]
theorem
BoundedLattice.iso.mk_inv
{α β : BoundedLattice}
(e : ↥α ≃o ↥β) :
(BoundedLattice.iso.mk e).inv = ↑(e.symm)
Constructs an equivalence between bounded lattices from an order isomorphism between them.
Equations
- BoundedLattice.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
order_dual
as a functor.
Equations
- BoundedLattice.dual = {obj := λ (X : BoundedLattice), BoundedLattice.of (↥X)ᵒᵈ, map := λ (X Y : BoundedLattice), ⇑bounded_lattice_hom.dual, map_id' := BoundedLattice.dual._proof_1, map_comp' := BoundedLattice.dual._proof_2}
@[simp]
@[simp]
@[simp]
The equivalence between BoundedLattice
and itself induced by order_dual
both ways.
Equations
- BoundedLattice.dual_equiv = category_theory.equivalence.mk BoundedLattice.dual BoundedLattice.dual (category_theory.nat_iso.of_components (λ (X : BoundedLattice), BoundedLattice.iso.mk (order_iso.dual_dual ↥X)) BoundedLattice.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : BoundedLattice), BoundedLattice.iso.mk (order_iso.dual_dual ↥X)) BoundedLattice.dual_equiv._proof_2)