The category of lattices

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 → WithTop (WithBot X).

def Lat : Type (u_1 + 1)

The category of lattices.

Equations

• Lat = CategoryTheory.Bundled Lattice

instance Lat.instCoeSortLatType : CoeSort Lat (Type u_1)

Equations

• Lat.instCoeSortLatType = CategoryTheory.Bundled.coeSort

instance Lat.instLatticeα (X : Lat) : Lattice ↑X

Equations

• Lat.instLatticeα X = X.str

def Lat.of (α : Type u_1) [Lattice α] : Lat

Construct a bundled Lat from a Lattice.

Equations

• Lat.of α = CategoryTheory.Bundled.of α

@[simp]

theorem Lat.coe_of (α : Type u_1) [Lattice α] : ↑(Lat.of α) = α

instance Lat.instInhabitedLat : Inhabited Lat

Equations

• Lat.instInhabitedLat = { default := Lat.of Bool }

instance Lat.instBundledHomTypeLatticeLatticeHom : CategoryTheory.BundledHom LatticeHom

Equations

• Lat.instBundledHomTypeLatticeLatticeHom = CategoryTheory.BundledHom.mk (fun {α β : Type u_1} (x : Lattice α) (x_1 : Lattice β) (f : LatticeHom α β) => f.toFun) LatticeHom.id @LatticeHom.comp

instance Lat.instLargeCategoryLat : CategoryTheory.LargeCategory Lat

Equations

• Lat.instLargeCategoryLat = CategoryTheory.BundledHom.category LatticeHom

instance Lat.instConcreteCategoryLatInstLargeCategoryLat : CategoryTheory.ConcreteCategory Lat

Equations

• Lat.instConcreteCategoryLatInstLargeCategoryLat = CategoryTheory.BundledHom.concreteCategory LatticeHom

instance Lat.hasForgetToPartOrd : CategoryTheory.HasForget₂ Lat PartOrd

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Lat.Iso.mk_hom_toSupHom_toFun {α : Lat} {β : Lat} (e : ↑α ≃o ↑β) (a : ↑α) : (Lat.Iso.mk e).hom.toSupHom a = e a

@[simp]

theorem Lat.Iso.mk_inv_toSupHom_toFun {α : Lat} {β : Lat} (e : ↑α ≃o ↑β) (a : ↑β) : (Lat.Iso.mk e).inv.toSupHom a = (OrderIso.symm e) a

def Lat.Iso.mk {α : Lat} {β : Lat} (e : ↑α ≃o ↑β) : α ≅ β

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Lat.dual_map : ∀ {X Y : Lat} (a : LatticeHom ↑X ↑Y), Lat.dual.toPrefunctor.map a = LatticeHom.dual a

@[simp]

theorem Lat.dual_obj (X : Lat) : Lat.dual.toPrefunctor.obj X = Lat.of (↑X)ᵒᵈ

def Lat.dual : CategoryTheory.Functor Lat Lat

OrderDual as a functor.

Equations

• Lat.dual = CategoryTheory.Functor.mk { obj := fun (X : Lat) => Lat.of (↑X)ᵒᵈ, map := fun {X Y : Lat} => ⇑LatticeHom.dual }

@[simp]

theorem Lat.dualEquiv_inverse : Lat.dualEquiv.inverse = Lat.dual

@[simp]

theorem Lat.dualEquiv_functor : Lat.dualEquiv.functor = Lat.dual

def Lat.dualEquiv : Lat ≌ Lat

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

Equations

• One or more equations did not get rendered due to their size.

theorem Lat_dual_comp_forget_to_partOrd : CategoryTheory.Functor.comp Lat.dual (CategoryTheory.forget₂ Lat PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ Lat PartOrd) PartOrd.dual