mathlib documentation

topology.hom.open

Continuous open maps #

This file defines bundled continuous open maps.

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_open_map: Continuous open maps.

Typeclasses #

continuous_open_map_class

structure continuous_open_map (α : Type u_6) (β : Type u_7) [topological_space α] [topological_space β] :

Type (max u_6 u_7)

to_continuous_map : C(α, β)
map_open' : is_open_map self.to_continuous_map.to_fun

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

Instances for continuous_open_map

continuous_open_map.has_sizeof_inst
continuous_open_map.has_coe_t
continuous_open_map.continuous_open_map_class
continuous_open_map.has_coe_to_fun
continuous_open_map.inhabited

@[class]

structure continuous_open_map_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [topological_space α] [topological_space β] :

Type (max u_6 u_7 u_8)

to_continuous_map_class : continuous_map_class F α β
map_open : ∀ (f : F), is_open_map ⇑f

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

You should extend this class when you extend continuous_open_map.

Instances of this typeclass

continuous_open_map.continuous_open_map_class

Instances of other typeclasses for continuous_open_map_class

continuous_open_map_class.has_sizeof_inst

@[protected, instance]

def continuous_open_map.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [continuous_open_map_class F α β] :

has_coe_t F (α →CO β)

Equations

continuous_open_map.has_coe_t = {coe := λ (f : F), {to_continuous_map := ↑f, map_open' := _}}

Continuous open maps #

@[protected, instance]

def continuous_open_map.continuous_open_map_class {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] :

continuous_open_map_class (α →CO β) α β

Equations

continuous_open_map.continuous_open_map_class = {to_continuous_map_class := {to_fun_like := {coe := λ (f : α →CO β), f.to_continuous_map.to_fun, coe_injective' := _}, map_continuous := _}, map_open := _}

@[protected, instance]

def continuous_open_map.has_coe_to_fun {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] :

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

continuous_open_map.has_coe_to_fun = fun_like.has_coe_to_fun

@[simp]

theorem continuous_open_map.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] {f : α →CO β} :

f.to_continuous_map.to_fun = ⇑f

@[ext]

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

f = g

@[protected]

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

α →CO β

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

Equations

f.copy f' h = {to_continuous_map := f.to_continuous_map.copy f' h, map_open' := _}

@[protected]

def continuous_open_map.id (α : Type u_2) [topological_space α] :

α →CO α

id as a continuous_open_map.

Equations

continuous_open_map.id α = {to_continuous_map := continuous_map.id α _inst_1, map_open' := _}

@[protected, instance]

def continuous_open_map.inhabited (α : Type u_2) [topological_space α] :

inhabited (α →CO α)

Equations

continuous_open_map.inhabited α = {default := continuous_open_map.id α _inst_1}

@[simp]

theorem continuous_open_map.coe_id (α : Type u_2) [topological_space α] :

⇑(continuous_open_map.id α) = id

@[simp]

theorem continuous_open_map.id_apply {α : Type u_2} [topological_space α] (a : α) :

⇑(continuous_open_map.id α) a = a

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

α →CO γ

Composition of continuous_open_maps as a continuous_open_map.

Equations

f.comp g = {to_continuous_map := f.to_continuous_map.comp g.to_continuous_map, map_open' := _}

@[simp]

theorem continuous_open_map.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] (f : β →CO γ) (g : α →CO β) :

⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem continuous_open_map.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] (f : β →CO γ) (g : α →CO β) (a : α) :

⇑(f.comp g) a = ⇑f (⇑g a)

@[simp]

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

(f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem continuous_open_map.comp_id {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α →CO β) :

f.comp (continuous_open_map.id α) = f

@[simp]

theorem continuous_open_map.id_comp {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α →CO β) :

(continuous_open_map.id β).comp f = f

theorem continuous_open_map.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] {g₁ g₂ : β →CO γ} {f : α →CO β} (hf : function.surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

theorem continuous_open_map.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] {g : β →CO γ} {f₁ f₂ : α →CO β} (hg : function.injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂