mathlib3 documentation

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.

@[protected, instance]
Equations
@[protected, instance]
Equations
def BddLat.of (α : Type u_1) [lattice α] [bounded_order α] :

Construct a bundled BddLat from lattice + bounded_order.

Equations
@[simp]
theorem BddLat.coe_of (α : Type u_1) [lattice α] [bounded_order α] :
(BddLat.of α) = α
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
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 β) :

order_dual as a functor.

Equations

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