# Documentation

Mathlib.Order.Category.Lat

# The category of lattices #

This defines Lat, the category of lattices.

Note that Lat doesn't correspond to the literature definition of [Lat] (https://ncatlab.org/nlab/show/Lat) as we don't require bottom or top elements. Instead, Lat corresponds to BddLat.

## TODO #

The free functor from Lat to BddLat is X → WithTop (WithBot X).

def Lat :
Type (u_1 + 1)

The category of lattices.

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

Construct a bundled Lat from a Lattice.

Equations
Instances For
@[simp]
theorem Lat.coe_of (α : Type u_1) [] :
() = α
Equations
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Lat.Iso.mk_hom_toSupHom_toFun {α : Lat} {β : Lat} (e : α ≃o β) (a : α) :
().hom.toSupHom a = e a
@[simp]
theorem Lat.Iso.mk_inv_toSupHom_toFun {α : Lat} {β : Lat} (e : α ≃o β) (a : β) :
().inv.toSupHom a = () a
def Lat.Iso.mk {α : Lat} {β : Lat} (e : α ≃o β) :
α β

Constructs an isomorphism of lattices from an order isomorphism between them.

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

OrderDual as a functor.

Equations
Instances For

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

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