Continuous open maps

This file defines bundled continuous open maps.

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

• ContinuousOpenMap: Continuous open maps.

Typeclasses

• ContinuousOpenMapClass

structure ContinuousOpenMap (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] extends ContinuousMap : Type (max u_6 u_7)

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

• toFun : α → β
• continuous_toFun : Continuous self.toFun
• map_open' : IsOpenMap self.toFun

theorem ContinuousOpenMap.map_open' {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] (self : α →CO β) : IsOpenMap 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 ContinuousOpenMapClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] extends ContinuousMapClass : Prop

ContinuousOpenMapClass F α β states that F is a type of continuous open maps.

You should extend this class when you extend ContinuousOpenMap.

• map_continuous : ∀ (f : F), Continuous ⇑f
• map_open : ∀ (f : F), IsOpenMap ⇑f

theorem ContinuousOpenMapClass.map_open {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} : ∀ {inst : TopologicalSpace α} {inst_1 : TopologicalSpace β} {inst_2 : FunLike F α β} [self : ContinuousOpenMapClass F α β] (f : F), IsOpenMap ⇑f

instance instCoeTCContinuousOpenMapOfContinuousOpenMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousOpenMapClass F α β] : CoeTC F (α →CO β)

Equations

• instCoeTCContinuousOpenMapOfContinuousOpenMapClass = { coe := fun (f : F) => { toContinuousMap := ↑f, map_open' := ⋯ } }

Continuous open maps

instance ContinuousOpenMap.instFunLike {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] : FunLike (α →CO β) α β

Equations

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

instance ContinuousOpenMap.instContinuousOpenMapClass {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] : ContinuousOpenMapClass (α →CO β) α β

Equations

• ⋯ = ⋯

theorem ContinuousOpenMap.toFun_eq_coe {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : α →CO β} : f.toFun = ⇑f

@[simp]

theorem ContinuousOpenMap.coe_toContinuousMap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α →CO β) : ⇑f.toContinuousMap = ⇑f

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

def ContinuousOpenMap.copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α →CO β) (f' : α → β) (h : f' = ⇑f) : α →CO β

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

Equations

• f.copy f' h = { toContinuousMap := f.copy f' h, map_open' := ⋯ }

@[simp]

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

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

def ContinuousOpenMap.id (α : Type u_2) [TopologicalSpace α] : α →CO α

id as a ContinuousOpenMap.

Equations

• ContinuousOpenMap.id α = { toContinuousMap := ContinuousMap.id α, map_open' := ⋯ }

instance ContinuousOpenMap.instInhabited (α : Type u_2) [TopologicalSpace α] : Inhabited (α →CO α)

Equations

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

@[simp]

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

@[simp]

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

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

Composition of ContinuousOpenMaps as a ContinuousOpenMap.

Equations

• f.comp g = { toContinuousMap := f.comp g.toContinuousMap, map_open' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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