mathlib documentation

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).

@[protected, instance]
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
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]