The category of complete lattices

This file defines CompleteLat, the category of complete lattices.

structure CompleteLat : Type (u_1 + 1)

The category of complete lattices.

• carrier : Type u_1

  The underlying lattice.

• str : CompleteLattice ↑self

instance CompleteLat.instCoeSortType : CoeSort CompleteLat (Type u_1)

Equations

• CompleteLat.instCoeSortType = { coe := CompleteLat.carrier }

@[reducible, inline]

abbrev CompleteLat.of (X : Type u_1) [CompleteLattice X] : CompleteLat

Construct a bundled CompleteLat from the underlying type and typeclass.

Equations

• CompleteLat.of X = CompleteLat.mk X

theorem CompleteLat.coe_of (α : Type u_1) [CompleteLattice α] : ↑(of α) = α

instance CompleteLat.instInhabited : Inhabited CompleteLat

Equations

• CompleteLat.instInhabited = { default := CompleteLat.of PUnit.{?u.3 + 1} }

instance CompleteLat.instLargeCategory : CategoryTheory.LargeCategory CompleteLat

Equations

• CompleteLat.instLargeCategory = CategoryTheory.Category.mk @CompleteLat.instLargeCategory.proof_1 @CompleteLat.instLargeCategory.proof_2 @CompleteLat.instLargeCategory.proof_3

instance CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier : CategoryTheory.ConcreteCategory CompleteLat fun (x1 x2 : CompleteLat) => CompleteLatticeHom ↑x1 ↑x2

Equations

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

instance CompleteLat.hasForgetToBddLat : CategoryTheory.HasForget₂ CompleteLat BddLat

Equations

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

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

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

Equations

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

@[simp]

theorem CompleteLat.Iso.mk_inv {α β : CompleteLat} (e : ↑α ≃o ↑β) : (mk e).inv = CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }

@[simp]

theorem CompleteLat.Iso.mk_hom {α β : CompleteLat} (e : ↑α ≃o ↑β) : (mk e).hom = CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }

def CompleteLat.dual : CategoryTheory.Functor CompleteLat CompleteLat

OrderDual as a functor.

Equations

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

@[simp]

theorem CompleteLat.dual_map {x✝ x✝¹ : CompleteLat} (a : CompleteLatticeHom ↑x✝ ↑x✝¹) : dual.map a = CompleteLatticeHom.dual a

def CompleteLat.dualEquiv : CompleteLat ≌ CompleteLat

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

Equations

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

@[simp]

theorem CompleteLat.dualEquiv_inverse : dualEquiv.inverse = dual

@[simp]

theorem CompleteLat.dualEquiv_functor : dualEquiv.functor = dual

theorem completeLat_dual_comp_forget_to_bddLat : CompleteLat.dual.comp (CategoryTheory.forget₂ CompleteLat BddLat) = (CategoryTheory.forget₂ CompleteLat BddLat).comp BddLat.dual