# Documentation

Mathlib.Order.Category.BddLat

# The category of bounded lattices #

This file defines BddLat, the category of bounded lattices.

In literature, this is sometimes called Lat, the category of lattices, because being a lattice is understood to entail having a bottom and a top element.

structure BddLat :
Type (u_1 + 1)

The category of bounded lattices with bounded lattice morphisms.

Instances For
Equations
instance BddLat.instLatticeαToLat (X : BddLat) :
Lattice X.toLat
Equations
• = X.toLat.str
def BddLat.of (α : Type u_1) [] [] :

Construct a bundled BddLat from Lattice + BoundedOrder.

Equations
Instances For
@[simp]
theorem BddLat.coe_of (α : Type u_1) [] [] :
().toLat = α
Equations
Equations
instance BddLat.instFunLike (X : BddLat) (Y : BddLat) :
FunLike (X Y) X.toLat fun (x : X.toLat) => Y.toLat
Equations
• = let_fun this := inferInstance; this
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BddLat.coe_forget_to_bddOrd (X : BddLat) :
(.obj X).toPartOrd = X.toLat
@[simp]
theorem BddLat.coe_forget_to_lat (X : BddLat) :
(.obj X) = X.toLat
@[simp]
theorem BddLat.coe_forget_to_semilatSup (X : BddLat) :
().X = X.toLat
@[simp]
theorem BddLat.coe_forget_to_semilatInf (X : BddLat) :
().X = X.toLat
@[simp]
theorem BddLat.Iso.mk_inv_toLatticeHom_toSupHom_toFun {α : BddLat} {β : BddLat} (e : α.toLat ≃o β.toLat) (a : β.toLat) :
().inv.toSupHom a = () a
@[simp]
theorem BddLat.Iso.mk_hom_toLatticeHom_toSupHom_toFun {α : BddLat} {β : BddLat} (e : α.toLat ≃o β.toLat) (a : α.toLat) :
().hom.toSupHom a = e a
def BddLat.Iso.mk {α : BddLat} {β : BddLat} (e : α.toLat ≃o β.toLat) :
α β

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

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

OrderDual as a functor.

Equations
Instances For

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

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

The functor that adds a bottom and a top element to a lattice. This is the free functor.

Equations
Instances For

latToBddLat is left adjoint to the forgetful functor, meaning it is the free functor from Lat to BddLat.

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

latToBddLat and OrderDual commute.

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