# mathlib3documentation

order.category.BddLat

# The category of bounded lattices #

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

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 BddLat
@[protected, instance]
Equations
@[protected, instance]
def BddLat.lattice (X : BddLat) :
Equations
def BddLat.of (α : Type u_1) [lattice α]  :

Construct a bundled BddLat from lattice + bounded_order.

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

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

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

order_dual as a functor.

Equations

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

Equations
@[simp]
@[simp]
def Lat_to_BddLat  :

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

Equations

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

Equations

Lat_to_BddLat and order_dual commute.

Equations