# mathlib3documentation

order.category.Lat

# The category of lattices #

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

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 → with_top (with_bot X).

def Lat  :
Type (u_1+1)

The category of lattices.

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

Construct a bundled Lat from a lattice.

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

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

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

order_dual as a functor.

Equations
@[simp]
@[simp]
def Lat.dual_equiv  :

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

Equations