mathlib3 documentation

topology.spectral.hom

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 #

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

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) :
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) :
structure spectral_map (α : Type u_6) (β : Type u_7) [topological_space α] [topological_space β] :
Type (max u_6 u_7)

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)) [topological_space α] [topological_space β] :
Type (max u_6 u_7 u_8)

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.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [spectral_map_class F α β] :
Equations

Spectral maps #

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

Reinterpret a spectral_map as a continuous_map.

Equations
@[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.

Equations
@[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) :

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

Equations
@[simp]
theorem spectral_map.coe_copy {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : spectral_map α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem spectral_map.copy_eq {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : spectral_map α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def spectral_map.id (α : Type u_2) [topological_space α] :

id as a spectral_map.

Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem spectral_map.id_apply {α : Type u_2} [topological_space α] (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 α β) :

Composition of spectral_maps as a spectral_map.

Equations
@[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 α β) :
(f.comp g) = f g
@[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 : α) :
(f.comp g) a = f (g 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 α β) :
(f.comp g) = f.comp g
@[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 α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem spectral_map.comp_id {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : spectral_map α β) :
@[simp]
theorem spectral_map.id_comp {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : spectral_map α β) :
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) :
g₁.comp f = g₂.comp f g₁ = g₂
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) :
g.comp f₁ = g.comp f₂ f₁ = f₂