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.instBundledHomTypeOmegaCompletePartialOrderContinuousHom : CategoryTheory.BundledHom OmegaCompletePartialOrder.ContinuousHom

Equations

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

instance ωCPO.instConcreteCategoryωCPOInstωCPOLargeCategory : CategoryTheory.ConcreteCategory ωCPO

Equations

• ωCPO.instConcreteCategoryωCPOInstωCPOLargeCategory = id inferInstance

instance ωCPO.instCoeSortωCPOType : CoeSort ωCPO (Type u_1)

Equations

• ωCPO.instCoeSortωCPOType = 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ωCPO : Inhabited ωCPO

Equations

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

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

Equations

• ωCPO.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

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

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ωCPOInstωCPOLargeCategory (J : Type v) (f : J → ωCPO) : CategoryTheory.Limits.HasProduct f

Equations

• (_ : CategoryTheory.Limits.HasProduct f) = (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor f))

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

Equations

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

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

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

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

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

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ωCPOInstωCPOLargeCategory : CategoryTheory.Limits.HasProducts ωCPO

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete x) ωCPO) = (_ : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete x) ωCPO)

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

Equations

• (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)) = (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g))

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

Equations

• ωCPO.instHasEqualizersωCPOInstωCPOLargeCategory = (_ : CategoryTheory.Limits.HasEqualizers ωCPO)

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

Equations

• ωCPO.instHasLimitsωCPOInstωCPOLargeCategory = (_ : CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, v + 1} ωCPO)