# mathlibdocumentation

order.category.Lattice

# The category of lattices #

This defines Lattice, the category of lattices.

Note that Lattice 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 BoundedLattice (not yet in mathlib).

## TODO #

The free functor from Lattice to BoundedLattice is X → with_top (with_bot X).

def Lattice  :
Type (u_1+1)

The category of lattices.

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

Construct a bundled Lattice from a lattice.

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

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

Equations
@[simp]
theorem Lattice.iso.mk_inv {α β : Lattice} (e : α ≃o β) :
@[simp]
theorem Lattice.iso.mk_hom {α β : Lattice} (e : α ≃o β) :

order_dual as a functor.

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

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

Equations