# Documentation

Mathlib.Topology.Order.Hom.Basic

# Continuous order homomorphisms #

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 FunLike 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 #

• ContinuousOrderHom: Continuous monotone functions, aka Priestley homomorphisms.

## Typeclasses #

• ContinuousOrderHomClass
structure ContinuousOrderHom (α : Type u_6) (β : Type u_7) [] [] [] [] extends :
Type (max u_6 u_7)

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

Instances For
Instances For
class ContinuousOrderHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_continuous : ∀ (f : F),
• map_monotone : ∀ (f : F), Monotone f

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

You should extend this class when you extend ContinuousOrderHom.

Instances
instance ContinuousOrderHomClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] :
def ContinuousOrderHomClass.toContinuousOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] (f : F) :
α →Co β

Turn an element of a type F satisfying ContinuousOrderHomClass F α β into an actual ContinuousOrderHom. This is declared as the default coercion from F to α →Co β.

Instances For
instance ContinuousOrderHomClass.instCoeTCContinuousOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] [] [] :
CoeTC F (α →Co β)

### Top homomorphisms #

def ContinuousOrderHom.toContinuousMap {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →Co β) :
C(α, β)

Reinterpret a ContinuousOrderHom as a ContinuousMap.

Instances For
@[simp]
theorem ContinuousOrderHom.coe_toOrderHom {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →Co β) :
f.toOrderHom = f
theorem ContinuousOrderHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] [] [] {f : α →Co β} :
f.toFun = f
theorem ContinuousOrderHom.ext {α : Type u_2} {β : Type u_3} [] [] [] [] {f : α →Co β} {g : α →Co β} (h : ∀ (a : α), f a = g a) :
f = g
def ContinuousOrderHom.copy {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →Co β) (f' : αβ) (h : f' = f) :
α →Co β

Copy of a ContinuousOrderHom with a new ContinuousMap equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem ContinuousOrderHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →Co β) (f' : αβ) (h : f' = f) :
↑() = f'
theorem ContinuousOrderHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →Co β) (f' : αβ) (h : f' = f) :
= f
def ContinuousOrderHom.id (α : Type u_2) [] [] :
α →Co α

id as a ContinuousOrderHom.

Instances For
@[simp]
theorem ContinuousOrderHom.coe_id (α : Type u_2) [] [] :
= id
@[simp]
theorem ContinuousOrderHom.id_apply {α : Type u_2} [] [] (a : α) :
↑() a = a
def ContinuousOrderHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →Co γ) (g : α →Co β) :
α →Co γ

Composition of ContinuousOrderHoms as a ContinuousOrderHom.

Instances For
@[simp]
theorem ContinuousOrderHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →Co γ) (g : α →Co β) :
↑() = f g
@[simp]
theorem ContinuousOrderHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] (f : β →Co γ) (g : α →Co β) (a : α) :
↑() a = f (g a)
@[simp]
theorem ContinuousOrderHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] [] [] [] [] (f : γ →Co δ) (g : β →Co γ) (h : α →Co β) :
@[simp]
theorem ContinuousOrderHom.comp_id {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →Co β) :
@[simp]
theorem ContinuousOrderHom.id_comp {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α →Co β) :
@[simp]
theorem ContinuousOrderHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] {g₁ : β →Co γ} {g₂ : β →Co γ} {f : α →Co β} (hf : ) :
g₁ = g₂
@[simp]
theorem ContinuousOrderHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] [] [] {g : β →Co γ} {f₁ : α →Co β} {f₂ : α →Co β} (hg : ) :
f₁ = f₂
instance ContinuousOrderHom.instPreorderContinuousOrderHom {α : Type u_2} {β : Type u_3} [] [] [] [] :
Preorder (α →Co β)