Spectral maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[topological_space α]
[topological_space β]
(f : α → β) :
Prop
- to_continuous : continuous f
- is_compact_preimage_of_is_open : ∀ ⦃s : set β⦄, is_open s → is_compact s → 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_is_open
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set β}
(hf : is_spectral_map f)
(h₀ : is_compact s)
(h₁ : is_open s) :
is_compact (f ⁻¹' s)
theorem
is_spectral_map.continuous
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : is_spectral_map f) :
theorem
is_spectral_map.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : β → γ}
{g : α → β}
(hf : is_spectral_map f)
(hg : is_spectral_map g) :
is_spectral_map (f ∘ g)
structure
spectral_map
(α : Type u_6)
(β : Type u_7)
[topological_space α]
[topological_space β] :
Type (max u_6 u_7)
- to_fun : α → β
- spectral' : is_spectral_map self.to_fun
The type of spectral maps from α to β.
Instances for spectral_map
- spectral_map.has_sizeof_inst
- spectral_map.has_coe_t
- spectral_map.spectral_map_class
- spectral_map.has_coe_to_fun
- spectral_map.inhabited
@[class]
structure
spectral_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)
- coe : F → Π (a : α), (λ (_x : α), β) a
- coe_injective' : function.injective spectral_map_class.coe
- map_spectral : ∀ (f : F), is_spectral_map ⇑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
@[instance]
def
spectral_map_class.to_fun_like
(F : Type u_6)
(α : out_param (Type u_7))
(β : out_param (Type u_8))
[topological_space α]
[topological_space β]
[self : spectral_map_class F α β] :
fun_like F α (λ (_x : α), β)
@[protected, instance]
def
spectral_map_class.to_continuous_map_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[spectral_map_class F α β] :
continuous_map_class F α β
Equations
- spectral_map_class.to_continuous_map_class = {coe := spectral_map_class.coe _inst_3, coe_injective' := _, map_continuous := _}
@[protected, instance]
def
spectral_map.has_coe_t
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[spectral_map_class F α β] :
has_coe_t F (spectral_map α β)
Spectral maps #
def
spectral_map.to_continuous_map
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
(f : spectral_map α β) :
Reinterpret a spectral_map as a continuous_map.
Equations
- f.to_continuous_map = {to_fun := f.to_fun, continuous_to_fun := _}
@[protected, instance]
def
spectral_map.spectral_map_class
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β] :
spectral_map_class (spectral_map α β) α β
Equations
- spectral_map.spectral_map_class = {coe := spectral_map.to_fun _inst_2, coe_injective' := _, map_spectral := _}
@[protected, instance]
def
spectral_map.has_coe_to_fun
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β] :
has_coe_to_fun (spectral_map α β) (λ (_x : spectral_map α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[simp]
theorem
spectral_map.to_fun_eq_coe
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
{f : spectral_map α β} :
@[ext]
theorem
spectral_map.ext
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
{f g : spectral_map α β}
(h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
@[protected]
def
spectral_map.copy
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
(f : spectral_map α β)
(f' : α → β)
(h : f' = ⇑f) :
spectral_map α β
Copy of a spectral_map with a new to_fun equal to the old one. Useful to fix definitional
equalities.
@[simp]
theorem
spectral_map.coe_copy
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
(f : spectral_map α β)
(f' : α → β)
(h : f' = ⇑f) :
theorem
spectral_map.copy_eq
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
(f : spectral_map α β)
(f' : α → β)
(h : f' = ⇑f) :
@[protected]
id as a spectral_map.
@[protected, instance]
Equations
- spectral_map.inhabited α = {default := spectral_map.id α _inst_1}
@[simp]
@[simp]
theorem
spectral_map.id_apply
{α : Type u_2}
[topological_space α]
(a : α) :
⇑(spectral_map.id α) a = a
def
spectral_map.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
(f : spectral_map β γ)
(g : spectral_map α β) :
spectral_map α γ
Composition of spectral_maps as a spectral_map.
Equations
- f.comp g = {to_fun := ⇑(f.to_continuous_map.comp g.to_continuous_map), spectral' := _}
@[simp]
theorem
spectral_map.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
(f : spectral_map β γ)
(g : spectral_map α β) :
@[simp]
theorem
spectral_map.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
(f : spectral_map β γ)
(g : spectral_map α β)
(a : α) :
@[simp]
theorem
spectral_map.coe_comp_continuous_map
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
(f : spectral_map β γ)
(g : spectral_map α β) :
@[simp]
theorem
spectral_map.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(f : spectral_map γ δ)
(g : spectral_map β γ)
(h : spectral_map α β) :
@[simp]
theorem
spectral_map.comp_id
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
(f : spectral_map α β) :
f.comp (spectral_map.id α) = f
@[simp]
theorem
spectral_map.id_comp
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
(f : spectral_map α β) :
(spectral_map.id β).comp f = f
theorem
spectral_map.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
{g₁ g₂ : spectral_map β γ}
{f : spectral_map α β}
(hf : function.surjective ⇑f) :
theorem
spectral_map.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : spectral_map β γ}
{f₁ f₂ : spectral_map α β}
(hg : function.injective ⇑g) :