# mathlibdocumentation

topology.spectral.hom

# Spectral maps #

This file defines spectral maps. A map is spectral when it's continuous and the preimage of a compact open set is compact open.

## Main declarations #

• is_spectral_map: Predicate for a map to be spectral.
• spectral_map: Bundled spectral maps.
• spectral_map_class: Typeclass for a type to be a type of spectral maps.

## TODO #

Once we have spectral_space, is_spectral_map should move to topology.spectral.basic.

structure is_spectral_map {α : Type u_2} {β : Type u_3} (f : α → β) :
Prop
• to_continuous :
• compact_preimage_of_open : ∀ ⦃s : set β⦄, is_compact (f ⁻¹' s)

A function between topological spaces is spectral if it is continuous and the preimage of every compact open set is compact open.

theorem is_compact.preimage_of_open {α : Type u_2} {β : Type u_3} {f : α → β} {s : set β} (hf : is_spectral_map f) (h₀ : is_compact s) (h₁ : is_open s) :
theorem is_spectral_map.continuous {α : Type u_2} {β : Type u_3} {f : α → β} (hf : is_spectral_map f) :
theorem is_spectral_map_id {α : Type u_2}  :
theorem is_spectral_map.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : β → γ} {g : α → β} (hf : is_spectral_map f) (hg : is_spectral_map g) :
structure spectral_map (α : Type u_6) (β : Type u_7)  :
Type (max u_6 u_7)
• to_fun : α → β
• spectral' :

The type of spectral maps from α to β.

Instances for spectral_map
@[class]
structure spectral_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_fun_like : α (λ (_x : α), β)
• map_spectral : ∀ (f : F),

spectral_map_class F α β states that F is a type of spectral maps.

You should extend this class when you extend spectral_map.

Instances of this typeclass
Instances of other typeclasses for spectral_map_class
• spectral_map_class.has_sizeof_inst
@[protected, instance]
def spectral_map_class.to_continuous_map_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] :
β
Equations
@[protected, instance]
def spectral_map.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] :
β)
Equations

### Spectral maps #

def spectral_map.to_continuous_map {α : Type u_2} {β : Type u_3} (f : β) :
C(α, β)

Reinterpret a spectral_map as a continuous_map.

Equations
@[protected, instance]
def spectral_map.spectral_map_class {α : Type u_2} {β : Type u_3}  :
α β
Equations
@[protected, instance]
def spectral_map.has_coe_to_fun {α : Type u_2} {β : Type u_3}  :
(λ (_x : β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem spectral_map.to_fun_eq_coe {α : Type u_2} {β : Type u_3} {f : β} :
@[ext]
theorem spectral_map.ext {α : Type u_2} {β : Type u_3} {f g : β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def spectral_map.copy {α : Type u_2} {β : Type u_3} (f : β) (f' : α → β) (h : f' = f) :
β

Copy of a spectral_map with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def spectral_map.id (α : Type u_2)  :
α

id as a spectral_map.

Equations
@[protected, instance]
def spectral_map.inhabited (α : Type u_2)  :
Equations
@[simp]
theorem spectral_map.coe_id (α : Type u_2)  :
@[simp]
theorem spectral_map.id_apply {α : Type u_2} (a : α) :
a = a
def spectral_map.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (f : γ) (g : β) :
γ

Composition of spectral_maps as a spectral_map.

Equations
@[simp]
theorem spectral_map.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (f : γ) (g : β) :
(f.comp g) = f g
@[simp]
theorem spectral_map.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} (f : γ) (g : β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem spectral_map.coe_comp_continuous_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} (f : γ) (g : β) :
(f.comp g) = f.comp g
@[simp]
theorem spectral_map.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} (f : δ) (g : γ) (h : β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem spectral_map.comp_id {α : Type u_2} {β : Type u_3} (f : β) :
f.comp = f
@[simp]
theorem spectral_map.id_comp {α : Type u_2} {β : Type u_3} (f : β) :
.comp f = f
theorem spectral_map.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} {g₁ g₂ : γ} {f : β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem spectral_map.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} {g : γ} {f₁ f₂ : β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂