The category of complete lattices

This file defines CompleteLat, the category of complete lattices.

def CompleteLat : Type (u_1 + 1)

The category of complete lattices.

Equations

• CompleteLat = CategoryTheory.Bundled CompleteLattice

instance CompleteLat.instCoeSortType : CoeSort CompleteLat (Type u_1)

Equations

• CompleteLat.instCoeSortType = CategoryTheory.Bundled.coeSort

instance CompleteLat.instCompleteLatticeα (X : CompleteLat) : CompleteLattice ↑X

Equations

• X.instCompleteLatticeα = X.str

def CompleteLat.of (α : Type u_1) [CompleteLattice α] : CompleteLat

Construct a bundled CompleteLat from a CompleteLattice.

Equations

• CompleteLat.of α = CategoryTheory.Bundled.of α

@[simp]

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.instBundledHomCompleteLatticeCompleteLatticeHom : CategoryTheory.BundledHom CompleteLatticeHom

Equations

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

instance instCompleteLatLargeCategory : CategoryTheory.LargeCategory CompleteLat

Equations

• instCompleteLatLargeCategory = CategoryTheory.BundledHom.category CompleteLatticeHom

instance CompleteLat.instHasForget : CategoryTheory.HasForget CompleteLat

Equations

• CompleteLat.instHasForget = id inferInstance

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

• CompleteLat.Iso.mk e = { hom := { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }, inv := { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CompleteLat.Iso.mk_inv_toFun {α β : CompleteLat} (e : ↑α ≃o ↑β) (a : ↑β) : (mk e).inv.toFun a = e.symm a

@[simp]

theorem CompleteLat.Iso.mk_hom_toFun {α β : CompleteLat} (e : ↑α ≃o ↑β) (a : ↑α) : (mk e).hom.toFun a = e a

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_obj (X : CompleteLat) : dual.obj X = of (↑X)ᵒᵈ

@[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