The category of frames

This file defines Frm, the category of frames.

References

• nLab, Frm

def Frm : Type (u_1 + 1)

The category of frames.

Equations

• Frm = CategoryTheory.Bundled Order.Frame

instance Frm.instCoeSortType : CoeSort Frm (Type u_1)

Equations

• Frm.instCoeSortType = CategoryTheory.Bundled.coeSort

instance Frm.instFrameα (X : Frm) : Order.Frame ↑X

Equations

• X.instFrameα = X.str

def Frm.of (α : Type u_1) [Order.Frame α] : Frm

Construct a bundled Frm from a Frame.

Equations

• Frm.of α = CategoryTheory.Bundled.of α

@[simp]

theorem Frm.coe_of (α : Type u_1) [Order.Frame α] : ↑(of α) = α

instance Frm.instInhabited : Inhabited Frm

Equations

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

@[reducible, inline]

abbrev Frm.Hom (α : Type u_1) (β : Type u_2) [Order.Frame α] [Order.Frame β] : Type (max u_2 u_1)

An abbreviation of FrameHom that assumes Frame instead of the weaker CompleteLattice. Necessary for the category theory machinery.

Equations

• Frm.Hom α β = FrameHom α β

instance Frm.bundledHom : CategoryTheory.BundledHom Hom

Equations

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

instance instFrmLargeCategory : CategoryTheory.LargeCategory Frm

Equations

• instFrmLargeCategory = CategoryTheory.BundledHom.category Frm.Hom

instance instFrmCategory : CategoryTheory.Category.{u_1, u_1 + 1} Frm

Equations

• instFrmCategory = CategoryTheory.BundledHom.category Frm.Hom

instance Frm.instHasForget : CategoryTheory.HasForget Frm

Equations

• Frm.instHasForget = id inferInstance

instance Frm.hasForgetToLat : CategoryTheory.HasForget₂ Frm Lat

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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