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

source

def ωCPO :

Type (u + 1)

The category of types with an omega complete partial order.

Instances For

source

instance ωCPO.instBundledHomTypeOmegaCompletePartialOrderContinuousHom :

CategoryTheory.BundledHom OmegaCompletePartialOrder.ContinuousHom

source

instance ωCPO.instConcreteCategoryωCPOInstωCPOLargeCategory :

CategoryTheory.ConcreteCategory ωCPO

source

instance ωCPO.instCoeSortωCPOType :

CoeSort ωCPO (Type u_1)

source

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

ωCPO

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

Instances For

source

@[simp]

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

↑(ωCPO.of α) = α

source

instance ωCPO.instInhabitedωCPO :

Inhabited ωCPO

source

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

OmegaCompletePartialOrder ↑α

source

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

CategoryTheory.Limits.Fan f

The pi-type gives a cone for a product.

Instances For

source

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.

Instances For

source

instance ωCPO.HasProducts.instHasProductωCPOInstωCPOLargeCategory (J : Type v) (f : J → ωCPO) :

CategoryTheory.Limits.HasProduct f

source

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

OmegaCompletePartialOrder { a // ↑f a = ↑g a }

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

instance ωCPO.instHasProductsωCPOInstωCPOLargeCategory :

CategoryTheory.Limits.HasProducts ωCPO

source

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

CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)

source

instance ωCPO.instHasEqualizersωCPOInstωCPOLargeCategory :

CategoryTheory.Limits.HasEqualizers ωCPO

source

instance ωCPO.instHasLimitsωCPOInstωCPOLargeCategory :

CategoryTheory.Limits.HasLimits ωCPO