# mathlibdocumentation

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)  :
Type (max u_6 u_7)
• to_continuous_map : C(α, β)
• map_open' :

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))  :
Type (max u_6 u_7 u_8)
• to_continuous_map_class : β
• map_open : ∀ (f : 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} [ β] :
→CO β)
Equations

### Continuous open maps #

@[protected, instance]
def continuous_open_map.continuous_open_map_class {α : Type u_2} {β : Type u_3}  :
α β
Equations
@[protected, instance]
def continuous_open_map.has_coe_to_fun {α : Type u_2} {β : Type u_3}  :
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]
theorem continuous_open_map.to_fun_eq_coe {α : Type u_2} {β : Type u_3} {f : α →CO β} :
@[ext]
theorem continuous_open_map.ext {α : Type u_2} {β : Type u_3} {f g : α →CO β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def continuous_open_map.copy {α : Type u_2} {β : Type u_3} (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
@[protected]
def continuous_open_map.id (α : Type u_2)  :
α →CO α

id as a continuous_open_map.

Equations
@[protected, instance]
def continuous_open_map.inhabited (α : Type u_2)  :
Equations
@[simp]
theorem continuous_open_map.coe_id (α : Type u_2)  :
@[simp]
theorem continuous_open_map.id_apply {α : Type u_2} (a : α) :
= a
def continuous_open_map.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (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} (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} (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} (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} (f : α →CO β) :
= f
@[simp]
theorem continuous_open_map.id_comp {α : Type u_2} {β : Type u_3} (f : α →CO β) :
= f
theorem continuous_open_map.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} {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} {g : β →CO γ} {f₁ f₂ : α →CO β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂