# mathlibdocumentation

order.category.DistribLattice

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

def DistribLattice  :
Type (u_1+1)

The category of distributive lattices.

Equations
Instances for DistribLattice
@[protected, instance]
Equations
@[protected, instance]
Equations

Construct a bundled DistribLattice from a distrib_lattice underlying type and typeclass.

Equations
@[simp]
theorem DistribLattice.coe_of (α : Type u_1)  :
= α
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
def DistribLattice.iso.mk {α β : DistribLattice} (e : α ≃o β) :
α β

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

Equations
@[simp]
theorem DistribLattice.iso.mk_hom {α β : DistribLattice} (e : α ≃o β) :
@[simp]
theorem DistribLattice.iso.mk_inv {α β : DistribLattice} (e : α ≃o β) :
= (e.symm)
@[simp]
@[simp]
theorem DistribLattice.dual_map (X Y : DistribLattice) (ᾰ : Y) :

order_dual as a functor.

Equations

The equivalence between DistribLattice and itself induced by order_dual both ways.

Equations