The category of distributive lattices #
This file defines DistribLattice
, the category of distributive lattices.
Note that DistLat
in the literature doesn't always
correspond to DistribLattice
as we don't require bottom or top elements. Instead, this DistLat
corresponds to BoundedDistribLattice
.
The category of distributive lattices.
@[protected, instance]
@[protected, instance]
Equations
- X.distrib_lattice = X.str
Construct a bundled DistribLattice
from a distrib_lattice
underlying type and typeclass.
Equations
@[simp]
@[protected, instance]
@[protected, instance]
Equations
- DistribLattice.distrib_lattice.to_lattice.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk
@[protected, instance]
@[protected, instance]
Constructs an equivalence between distributive lattices from an order isomorphism between them.
Equations
- DistribLattice.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
DistribLattice.iso.mk_hom
{α β : DistribLattice}
(e : ↥α ≃o ↥β) :
(DistribLattice.iso.mk e).hom = ↑e
@[simp]
theorem
DistribLattice.iso.mk_inv
{α β : DistribLattice}
(e : ↥α ≃o ↥β) :
(DistribLattice.iso.mk e).inv = ↑(e.symm)
@[simp]
@[simp]
order_dual
as a functor.
Equations
- DistribLattice.dual = {obj := λ (X : DistribLattice), DistribLattice.of (↥X)ᵒᵈ, map := λ (X Y : DistribLattice), ⇑lattice_hom.dual, map_id' := DistribLattice.dual._proof_1, map_comp' := DistribLattice.dual._proof_2}
@[simp]
@[simp]
The equivalence between DistribLattice
and itself induced by order_dual
both ways.
Equations
- DistribLattice.dual_equiv = category_theory.equivalence.mk DistribLattice.dual DistribLattice.dual (category_theory.nat_iso.of_components (λ (X : DistribLattice), DistribLattice.iso.mk (order_iso.dual_dual ↥X)) DistribLattice.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : DistribLattice), DistribLattice.iso.mk (order_iso.dual_dual ↥X)) DistribLattice.dual_equiv._proof_2)