mathlib3 documentation

topology.hom.open

Continuous open maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Typeclasses #

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

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

Instances for continuous_open_map
@[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)

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 α β] :
has_coe_t F →CO β)
Equations

Continuous open maps #

@[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
@[simp]
@[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
@[simp]
theorem continuous_open_map.coe_copy {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α →CO β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem continuous_open_map.copy_eq {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α →CO β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def continuous_open_map.id (α : Type u_2) [topological_space α] :
α →CO α

id as a continuous_open_map.

Equations
@[protected, instance]
Equations
@[simp]
theorem continuous_open_map.id_apply {α : Type u_2} [topological_space α] (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
@[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 β) :
@[simp]
theorem continuous_open_map.id_comp {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α →CO β) :
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₂