# mathlib3documentation

order.category.BddDistLat

# The category of bounded distributive lattices #

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

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 BddDistLat
@[protected, instance]
Equations
@[protected, instance]
Equations
def BddDistLat.of (α : Type u_1)  :

Construct a bundled BddDistLat from a bounded_order distrib_lattice.

Equations
@[simp]
theorem BddDistLat.coe_of (α : Type u_1)  :
= α
@[protected, instance]
Equations

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

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

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

Equations
@[simp]
theorem BddDistLat.iso.mk_inv {α β : BddDistLat} (e : α ≃o β) :
@[simp]
theorem BddDistLat.dual_obj (X : BddDistLat) :
@[simp]
theorem BddDistLat.dual_map (X Y : BddDistLat) (ᾰ : (Y.to_BddLat)) :

order_dual as a functor.

Equations
@[simp]

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

Equations
@[simp]