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 DFunLike 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) [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] extends α →o β : Type (max u_6 u_7)

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

• toFun : α → β
• monotone' : Monotone self.toFun
• continuous_toFun : Continuous self.toFun

def «term_→Co_» : Lean.TrailingParserDescr

Equations

• «term_→Co_» = Lean.ParserDescr.trailingNode `«term_→Co_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →Co ") (Lean.ParserDescr.cat `term 25))

class ContinuousOrderHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] extends ContinuousMapClass F α β : Prop

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

You should extend this class when you extend ContinuousOrderHom.

• map_continuous (f : F) : Continuous ⇑f
• map_monotone (f : F) : Monotone ⇑f

@[instance 100]

instance ContinuousOrderHomClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousOrderHomClass F α β] : OrderHomClass F α β

def ContinuousOrderHomClass.toContinuousOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousOrderHomClass F α β] (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 β.

Equations

• ↑f = { toFun := ⇑f, monotone' := ⋯, continuous_toFun := ⋯ }

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

Equations

• ContinuousOrderHomClass.instCoeTCContinuousOrderHom = { coe := ContinuousOrderHomClass.toContinuousOrderHom }

Top homomorphisms

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

Reinterpret a ContinuousOrderHom as a ContinuousMap.

Equations

• f.toContinuousMap = { toFun := f.toFun, continuous_toFun := ⋯ }

instance ContinuousOrderHom.instFunLike {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] : FunLike (α →Co β) α β

Equations

• ContinuousOrderHom.instFunLike = { coe := fun (f : α →Co β) => f.toFun, coe_injective' := ⋯ }

instance ContinuousOrderHom.instContinuousOrderHomClass {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] : ContinuousOrderHomClass (α →Co β) α β

@[simp]

theorem ContinuousOrderHom.coe_toOrderHom {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) : ⇑f.toOrderHom = ⇑f

theorem ContinuousOrderHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] {f : α →Co β} : f.toFun = ⇑f

theorem ContinuousOrderHom.ext {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] {f g : α →Co β} (h : ∀ (a : α), f a = g a) : f = g

def ContinuousOrderHom.copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (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.

Equations

• f.copy f' h = { toOrderHom := f.copy f' h, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousOrderHom.coe_copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem ContinuousOrderHom.copy_eq {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def ContinuousOrderHom.id (α : Type u_2) [TopologicalSpace α] [Preorder α] : α →Co α

id as a ContinuousOrderHom.

Equations

• ContinuousOrderHom.id α = { toOrderHom := OrderHom.id, continuous_toFun := ⋯ }

instance ContinuousOrderHom.instInhabited (α : Type u_2) [TopologicalSpace α] [Preorder α] : Inhabited (α →Co α)

Equations

• ContinuousOrderHom.instInhabited α = { default := ContinuousOrderHom.id α }

@[simp]

theorem ContinuousOrderHom.coe_id (α : Type u_2) [TopologicalSpace α] [Preorder α] : ⇑(ContinuousOrderHom.id α) = id

@[simp]

theorem ContinuousOrderHom.id_apply {α : Type u_2} [TopologicalSpace α] [Preorder α] (a : α) : (ContinuousOrderHom.id α) a = a

def ContinuousOrderHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (f : β →Co γ) (g : α →Co β) : α →Co γ

Composition of ContinuousOrderHoms as a ContinuousOrderHom.

Equations

• f.comp g = { toOrderHom := f.comp g.toOrderHom, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousOrderHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (f : β →Co γ) (g : α →Co β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem ContinuousOrderHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (f : β →Co γ) (g : α →Co β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem ContinuousOrderHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] [TopologicalSpace δ] [Preorder δ] (f : γ →Co δ) (g : β →Co γ) (h : α →Co β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem ContinuousOrderHom.comp_id {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) : f.comp (ContinuousOrderHom.id α) = f

@[simp]

theorem ContinuousOrderHom.id_comp {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) : (ContinuousOrderHom.id β).comp f = f

@[simp]

theorem ContinuousOrderHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] {g₁ g₂ : β →Co γ} {f : α →Co β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem ContinuousOrderHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] {g : β →Co γ} {f₁ f₂ : α →Co β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance ContinuousOrderHom.instPreorder {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] : Preorder (α →Co β)

Equations

• ContinuousOrderHom.instPreorder = Preorder.lift DFunLike.coe

instance ContinuousOrderHom.instPartialOrder {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [PartialOrder β] : PartialOrder (α →Co β)

Equations

• ContinuousOrderHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯