Category of types with an omega complete partial order

In this file, we bundle the class OmegaCompletePartialOrder into a concrete category and prove that continuous functions also form an OmegaCompletePartialOrder.

Main definitions

• ωCPO
  • an instance of Category and ConcreteCategory

def ωCPO : Type (u + 1)

The category of types with an omega complete partial order.

Equations

• ωCPO = CategoryTheory.Bundled OmegaCompletePartialOrder

instance ωCPO.instBundledHomOmegaCompletePartialOrderContinuousHom : CategoryTheory.BundledHom OmegaCompletePartialOrder.ContinuousHom

Equations

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

instance ωCPO.instConcreteCategory : CategoryTheory.ConcreteCategory ωCPO

Equations

• ωCPO.instConcreteCategory = id inferInstance

instance ωCPO.instCoeSortType : CoeSort ωCPO (Type u_1)

Equations

• ωCPO.instCoeSortType = CategoryTheory.Bundled.coeSort

def ωCPO.of (α : Type u_1) [OmegaCompletePartialOrder α] : ωCPO

Construct a bundled ωCPO from the underlying type and typeclass.

Equations

• ωCPO.of α = CategoryTheory.Bundled.of α

@[simp]

theorem ωCPO.coe_of (α : Type u_1) [OmegaCompletePartialOrder α] : ↑(ωCPO.of α) = α

instance ωCPO.instInhabited : Inhabited ωCPO

Equations

• ωCPO.instInhabited = { default := ωCPO.of PUnit.{u_1 + 1} }

instance ωCPO.instOmegaCompletePartialOrderα (α : ωCPO) : OmegaCompletePartialOrder ↑α

Equations

• α.instOmegaCompletePartialOrderα = α.str

def ωCPO.HasProducts.product {J : Type v} (f : J → ωCPO) : CategoryTheory.Limits.Fan f

The pi-type gives a cone for a product.

Equations

• ωCPO.HasProducts.product f = CategoryTheory.Limits.Fan.mk (ωCPO.of ((j : J) → ↑(f j))) fun (j : J) => { toOrderHom := Pi.evalOrderHom j, cont := ⋯ }

def ωCPO.HasProducts.isProduct (J : Type v) (f : J → ωCPO) : CategoryTheory.Limits.IsLimit (ωCPO.HasProducts.product f)

The pi-type is a limit cone for the product.

Equations

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

instance ωCPO.HasProducts.instHasProduct (J : Type v) (f : J → ωCPO) : CategoryTheory.Limits.HasProduct f

Equations

• ⋯ = ⋯

instance ωCPO.omegaCompletePartialOrderEqualizer {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) : OmegaCompletePartialOrder { a : α // f a = g a }

Equations

• ωCPO.omegaCompletePartialOrderEqualizer f g = OmegaCompletePartialOrder.subtype (fun (a : α) => f a = g a) ⋯

def ωCPO.HasEqualizers.equalizerι {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) : { a : α // f a = g a } →𝒄 α

The equalizer inclusion function as a ContinuousHom.

Equations

• ωCPO.HasEqualizers.equalizerι f g = { toOrderHom := OrderHom.Subtype.val fun (a : α) => f a = g a, cont := ⋯ }

def ωCPO.HasEqualizers.equalizer {X : ωCPO} {Y : ωCPO} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.Fork f g

A construction of the equalizer fork.

Equations

• ωCPO.HasEqualizers.equalizer f g = CategoryTheory.Limits.Fork.ofι (ωCPO.HasEqualizers.equalizerι f g) ⋯

def ωCPO.HasEqualizers.isEqualizer {X : ωCPO} {Y : ωCPO} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.IsLimit (ωCPO.HasEqualizers.equalizer f g)

The equalizer fork is a limit.

Equations

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

instance ωCPO.instHasProducts : CategoryTheory.Limits.HasProducts ωCPO

Equations

• ⋯ = ⋯

instance ωCPO.instHasLimitWalkingParallelPairParallelPair {X : ωCPO} {Y : ωCPO} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)

Equations

• ⋯ = ⋯

instance ωCPO.instHasEqualizers : CategoryTheory.Limits.HasEqualizers ωCPO

Equations

• ωCPO.instHasEqualizers = ⋯

instance ωCPO.instHasLimits : CategoryTheory.Limits.HasLimits ωCPO

Equations

• ωCPO.instHasLimits = ⋯