# mathlib3documentation

order.category.DistLat

# The category of distributive lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines DistLat, the category of distributive lattices.

Note that DistLat in the literature doesn't always correspond to DistLat as we don't require bottom or top elements. Instead, this DistLat corresponds to BddDistLat.

def DistLat  :
Type (u_1+1)

The category of distributive lattices.

Equations
Instances for DistLat
@[protected, instance]
Equations
@[protected, instance]
Equations
def DistLat.of (α : Type u_1)  :

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

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

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

Equations
@[simp]
theorem DistLat.dual_map (X Y : DistLat) (ᾰ : Y) :

order_dual as a functor.

Equations
@[simp]
theorem DistLat.dual_obj (X : DistLat) :
@[simp]

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

Equations
@[simp]