# The category of bounded distributive lattices #

This defines BddDistLat, the category of bounded distributive lattices.

Note that this category is sometimes called DistLat when being a lattice is understood to entail having a bottom and a top element.

structure BddDistLat :
Type (u_1 + 1)

The category of bounded distributive lattices with bounded lattice morphisms.

• toDistLat : DistLat

The underlying distrib lattice of a bounded distributive lattice.

• isBoundedOrder : BoundedOrder self.toDistLat
Instances For
Equations
Equations
• X.instDistribLatticeαToDistLat = X.toDistLat.str
def BddDistLat.of (α : Type u_1) [] [] :

Construct a bundled BddDistLat from a BoundedOrder DistribLattice.

Equations
Instances For
@[simp]
theorem BddDistLat.coe_of (α : Type u_1) [] [] :
().toDistLat = α
Equations

Turn a BddDistLat into a BddLat by forgetting it is distributive.

Equations
Instances For
@[simp]
theorem BddDistLat.coe_toBddLat (X : BddDistLat) :
X.toBddLat.toLat = X.toDistLat
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BddDistLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BddDistLat} {β : BddDistLat} (e : α.toDistLat ≃o β.toDistLat) (a : α.toDistLat) :
.hom.toSupHom a = e a
@[simp]
theorem BddDistLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BddDistLat} {β : BddDistLat} (e : α.toDistLat ≃o β.toDistLat) (a : β.toDistLat) :
.inv.toSupHom a = e.symm a
def BddDistLat.Iso.mk {α : BddDistLat} {β : BddDistLat} (e : α.toDistLat ≃o β.toDistLat) :
α β

Constructs an equivalence between bounded distributive lattices from an order isomorphism between them.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem BddDistLat.dual_map {X : BddDistLat} {Y : BddDistLat} (a : BoundedLatticeHom X.toBddLat.toLat Y.toBddLat.toLat) :
BddDistLat.dual.map a = BoundedLatticeHom.dual a
@[simp]

OrderDual as a functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The equivalence between BddDistLat and itself induced by OrderDual both ways.

Equations
• One or more equations did not get rendered due to their size.
Instances For