# Documentation

Mathlib.Order.Category.BddDistLat

# 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.

Instances For
Equations
Equations
• = 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 = α

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

Equations
Instances For
@[simp]
theorem BddDistLat.coe_toBddLat (X : BddDistLat) :
.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 = () 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]
@[simp]
theorem BddDistLat.dual_map {X : BddDistLat} {Y : BddDistLat} (a : BoundedLatticeHom .toLat .toLat) :
BddDistLat.dual.map a = BoundedLatticeHom.dual a

OrderDual as a functor.

Equations
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