mathlibdocumentation

order.category.omega_complete_partial_order

Category of types with a omega complete partial order #

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

Main definitions #

• ωCPO
• an instance of category and concrete_category
def ωCPO  :
Type (u+1)

The category of types with a omega complete partial order.

Equations
Instances for ωCPO
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def ωCPO.has_coe_to_sort  :
(Type u_1)
Equations
def ωCPO.of (α : Type u_1)  :

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

Equations
@[simp]
theorem ωCPO.coe_of (α : Type u_1)  :
(ωCPO.of α) = α
@[protected, instance]
Equations
@[protected, instance]
Equations
def ωCPO.has_products.product {J : Type v} (f : J → ωCPO) :

The pi-type gives a cone for a product.

Equations
def ωCPO.has_products.is_product (J : Type v) (f : J → ωCPO) :

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

Equations
@[protected, instance]
@[protected, instance]
def ωCPO.omega_complete_partial_order_equalizer {α : Type u_1} {β : Type u_2} (f g : α →𝒄 β) :
Equations
def ωCPO.has_equalizers.equalizer_ι {α : Type u_1} {β : Type u_2} (f g : α →𝒄 β) :
{a // f a = g a} →𝒄 α

The equalizer inclusion function as a continuous_hom.

Equations
def ωCPO.has_equalizers.equalizer {X Y : ωCPO} (f g : X Y) :

A construction of the equalizer fork.

Equations
def ωCPO.has_equalizers.is_equalizer {X Y : ωCPO} (f g : X Y) :

The equalizer fork is a limit.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]