Category of types with a omega complete partial order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

def ωCPO :

Type (u+1)

The category of types with a omega complete partial order.

Equations

ωCPO = category_theory.bundled omega_complete_partial_order

Instances for ωCPO

source

@[protected, instance]

def ωCPO.omega_complete_partial_order.continuous_hom.category_theory.bundled_hom :

category_theory.bundled_hom omega_complete_partial_order.continuous_hom

Equations

ωCPO.omega_complete_partial_order.continuous_hom.category_theory.bundled_hom = {to_fun := omega_complete_partial_order.continuous_hom.simps.apply, id := omega_complete_partial_order.continuous_hom.id, comp := omega_complete_partial_order.continuous_hom.comp, hom_ext := omega_complete_partial_order.continuous_hom.coe_inj, id_to_fun := ωCPO.omega_complete_partial_order.continuous_hom.category_theory.bundled_hom._proof_1, comp_to_fun := ωCPO.omega_complete_partial_order.continuous_hom.category_theory.bundled_hom._proof_2}

source

@[protected, instance]

def ωCPO.concrete_category :

category_theory.concrete_category ωCPO

source

@[protected, instance]

def ωCPO.large_category :

category_theory.large_category ωCPO

source

@[protected, instance]

def ωCPO.has_coe_to_sort :

has_coe_to_sort ωCPO (Type u_1)

Equations

ωCPO.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

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

ωCPO

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

Equations

ωCPO.of α = category_theory.bundled.of α

source

@[simp]

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

↥(ωCPO.of α) = α

source

@[protected, instance]

def ωCPO.inhabited :

inhabited ωCPO

Equations

ωCPO.inhabited = {default := ωCPO.of punit (complete_lattice.omega_complete_partial_order punit)}

source

@[protected, instance]

def ωCPO.omega_complete_partial_order (α : ωCPO) :

omega_complete_partial_order ↥α

Equations

α.omega_complete_partial_order = α.str

source

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

category_theory.limits.fan f

The pi-type gives a cone for a product.

Equations

ωCPO.has_products.product f = category_theory.limits.fan.mk (ωCPO.of (Π (j : J), ↥(f j))) (λ (j : J), omega_complete_partial_order.continuous_hom.of_mono (pi.eval_order_hom j) _)

source

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

category_theory.limits.is_limit (ωCPO.has_products.product f)

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

Equations

ωCPO.has_products.is_product J f = {lift := λ (s : category_theory.limits.cone (category_theory.discrete.functor f)), {to_order_hom := {to_fun := λ (t : ↥(s.X)) (j : J), ⇑(s.π.app {as := j}) t, monotone' := _}, cont := _}, fac' := _, uniq' := _}

source

@[protected, instance]

def ωCPO.has_products.category_theory.limits.has_product (J : Type v) (f : J → ωCPO) :

category_theory.limits.has_product f

source

@[protected, instance]

def ωCPO.omega_complete_partial_order_equalizer {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) :

omega_complete_partial_order {a // ⇑f a = ⇑g a}

Equations

ωCPO.omega_complete_partial_order_equalizer f g = omega_complete_partial_order.subtype (λ (a : α), ⇑f a = ⇑g a) _

source

def ωCPO.has_equalizers.equalizer_ι {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) :

{a // ⇑f a = ⇑g a} →𝒄 α

The equalizer inclusion function as a continuous_hom.

Equations

ωCPO.has_equalizers.equalizer_ι f g = omega_complete_partial_order.continuous_hom.of_mono (order_hom.subtype.val (λ (a : α), ⇑f a = ⇑g a)) _

source

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

category_theory.limits.fork f g

A construction of the equalizer fork.

Equations

ωCPO.has_equalizers.equalizer f g = category_theory.limits.fork.of_ι (ωCPO.has_equalizers.equalizer_ι f g) _

source

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

category_theory.limits.is_limit (ωCPO.has_equalizers.equalizer f g)

The equalizer fork is a limit.

Equations

ωCPO.has_equalizers.is_equalizer f g = category_theory.limits.fork.is_limit.mk' (ωCPO.has_equalizers.equalizer f g) (λ (s : category_theory.limits.fork f g), ⟨{to_order_hom := {to_fun := λ (x : ↥(((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.zero)), ⟨⇑(s.ι) x, _⟩, monotone' := _}, cont := _}, _⟩)

source

@[protected, instance]

def ωCPO.category_theory.limits.has_products :

category_theory.limits.has_products ωCPO

source

@[protected, instance]

def ωCPO.category_theory.limits.parallel_pair.category_theory.limits.has_limit {X Y : ωCPO} (f g : X ⟶ Y) :

category_theory.limits.has_limit (category_theory.limits.parallel_pair f g)

source

@[protected, instance]

def ωCPO.category_theory.limits.has_equalizers :

category_theory.limits.has_equalizers ωCPO

source

@[protected, instance]

def ωCPO.category_theory.limits.has_limits :

category_theory.limits.has_limits ωCPO