# mathlib3documentation

topology.order.hom.basic

# Continuous order homomorphisms #

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

This file defines continuous order homomorphisms, that is maps which are both continuous and monotone. They are also called Priestley homomorphisms because they are the morphisms of the category of Priestley spaces.

We use the fun_like design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

## Types of morphisms #

• continuous_order_hom: Continuous monotone functions, aka Priestley homomorphisms.

## Typeclasses #

• continuous_order_hom_class
structure continuous_order_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β]  :
Type (max u_6 u_7)
• to_order_hom : α →o β
• continuous_to_fun :

The type of continuous monotone maps from α to β, aka Priestley homomorphisms.

Instances for continuous_order_hom
@[instance]
def continuous_order_hom_class.to_rel_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [self : β] :
@[class]
structure continuous_order_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β]  :
Type (max u_6 u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_rel : (f : F) {a b : α}, a b f a f b
• map_continuous : (f : F),

continuous_order_hom_class F α β states that F is a type of continuous monotone maps.

You should extend this class when you extend continuous_order_hom.

Instances of this typeclass
Instances of other typeclasses for continuous_order_hom_class
• continuous_order_hom_class.has_sizeof_inst
@[protected, instance]
def continuous_order_hom_class.to_continuous_map_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
β
Equations
@[protected, instance]
def continuous_order_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] :
→Co β)
Equations

### Top homomorphisms #

def continuous_order_hom.to_continuous_map {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →Co β) :
C(α, β)

Reinterpret a continuous_order_hom as a continuous_map.

Equations
@[protected, instance]
def continuous_order_hom.continuous_order_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
α β
Equations
@[protected, instance]
def continuous_order_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
has_coe_to_fun →Co β) (λ (_x : α →Co β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem continuous_order_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f : α →Co β} :
@[ext]
theorem continuous_order_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α →Co β} (h : (a : α), f a = g a) :
f = g
@[protected]
def continuous_order_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →Co β) (f' : α β) (h : f' = f) :
α →Co β

Copy of a continuous_order_hom with a new continuous_map equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem continuous_order_hom.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →Co β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem continuous_order_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →Co β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def continuous_order_hom.id (α : Type u_2) [preorder α] :
α →Co α

id as a continuous_order_hom.

Equations
@[protected, instance]
Equations
@[simp]
theorem continuous_order_hom.coe_id (α : Type u_2) [preorder α] :
@[simp]
theorem continuous_order_hom.id_apply {α : Type u_2} [preorder α] (a : α) :
= a
def continuous_order_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : β →Co γ) (g : α →Co β) :
α →Co γ

Composition of continuous_order_homs as a continuous_order_hom.

Equations
@[simp]
theorem continuous_order_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : β →Co γ) (g : α →Co β) :
(f.comp g) = f g
@[simp]
theorem continuous_order_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : β →Co γ) (g : α →Co β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem continuous_order_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] (f : γ →Co δ) (g : β →Co γ) (h : α →Co β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem continuous_order_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →Co β) :
= f
@[simp]
theorem continuous_order_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →Co β) :
= f
theorem continuous_order_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {g₁ g₂ : β →Co γ} {f : α →Co β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem continuous_order_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {g : β →Co γ} {f₁ f₂ : α →Co β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def continuous_order_hom.preorder {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
preorder →Co β)
Equations
@[protected, instance]
def continuous_order_hom.partial_order {α : Type u_2} {β : Type u_3} [preorder α]  :
Equations