The category of lattices #
This defines Lattice
, the category of lattices.
Note that Lattice
doesn't correspond to the literature definition of [Lat
]
(https://ncatlab.org/nlab/show/Lat) as we don't require bottom or top elements. Instead, Lat
corresponds to BoundedLattice
(not yet in mathlib).
TODO #
The free functor from Lattice
to BoundedLattice
is X → with_top (with_bot X)
.
The category of lattices.
Equations
Instances for Lattice
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
- Lattice.lattice_hom.category_theory.bundled_hom = {to_fun := λ (_x _x_1 : Type u_1) (_x_2 : lattice _x) (_x_3 : lattice _x_1), coe_fn, id := lattice_hom.id, comp := lattice_hom.comp, hom_ext := Lattice.lattice_hom.category_theory.bundled_hom._proof_1, id_to_fun := Lattice.lattice_hom.category_theory.bundled_hom._proof_2, comp_to_fun := Lattice.lattice_hom.category_theory.bundled_hom._proof_3}
@[protected, instance]
@[protected, instance]
Equations
- Lattice.has_forget_to_PartialOrder = {forget₂ := {obj := λ (X : Lattice), {α := ↥X, str := semilattice_inf.to_partial_order ↥X (lattice.to_semilattice_inf ↥X)}, map := λ (X Y : Lattice) (f : X ⟶ Y), ↑f, map_id' := Lattice.has_forget_to_PartialOrder._proof_1, map_comp' := Lattice.has_forget_to_PartialOrder._proof_2}, forget_comp := Lattice.has_forget_to_PartialOrder._proof_3}
Constructs an isomorphism of lattices from an order isomorphism between them.
Equations
- Lattice.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
order_dual
as a functor.
Equations
- Lattice.dual = {obj := λ (X : Lattice), Lattice.of (↥X)ᵒᵈ, map := λ (X Y : Lattice), ⇑lattice_hom.dual, map_id' := Lattice.dual._proof_1, map_comp' := Lattice.dual._proof_2}
@[simp]
The equivalence between Lattice
and itself induced by order_dual
both ways.
Equations
- Lattice.dual_equiv = category_theory.equivalence.mk Lattice.dual Lattice.dual (category_theory.nat_iso.of_components (λ (X : Lattice), Lattice.iso.mk (order_iso.dual_dual ↥X)) Lattice.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : Lattice), Lattice.iso.mk (order_iso.dual_dual ↥X)) Lattice.dual_equiv._proof_2)