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 #
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
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 α β] :
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 := {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.
@[simp]
theorem
continuous_open_map.to_fun_eq_coe
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
{f : α →CO β} :
@[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]
id as a continuous_open_map.
Equations
- continuous_open_map.id α = {to_continuous_map := continuous_map.id α _inst_1, map_open' := _}
@[protected, instance]
Equations
- continuous_open_map.inhabited α = {default := continuous_open_map.id α _inst_1}
@[simp]
@[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 β) :
@[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 : α) :
@[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 β) :
@[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) :
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) :