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

structure ωCPO : Type (u + 1)

The category of types with an omega complete partial order.

• carrier : Type u

  The underlying type.

• str : OmegaCompletePartialOrder self.carrier

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

Equations

• ωCPO.instCoeSortType = { coe := ωCPO.carrier }

@[reducible, inline]

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

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

Equations

• ωCPO.of α = { carrier := α, str := inst✝ }

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

instance ωCPO.instLargeCategory : CategoryTheory.LargeCategory ωCPO

Equations

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

instance ωCPO.instConcreteCategoryContinuousHomCarrier : CategoryTheory.ConcreteCategory ωCPO fun (x1 x2 : ωCPO) => x1.carrier →𝒄 x2.carrier

Equations

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

instance ωCPO.instInhabited : Inhabited ωCPO

Equations

• ωCPO.instInhabited = { default := ωCPO.of PUnit.{?u.2 + 1} }

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).carrier)) fun (j : J) => { toOrderHom := Pi.evalOrderHom j, map_ωSup' := ⋯ }

def ωCPO.HasProducts.isProduct (J : Type v) (f : J → ωCPO) : CategoryTheory.Limits.IsLimit (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

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, map_ωSup' := ⋯ }

def ωCPO.HasEqualizers.equalizer {X Y : ωCPO} (f 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 Y : ωCPO} (f g : X ⟶ Y) : CategoryTheory.Limits.IsLimit (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

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

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

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