# 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 #

• IsSpectralMap: Predicate for a map to be spectral.
• SpectralMap: Bundled spectral maps.
• SpectralMapClass: Typeclass for a type to be a type of spectral maps.

## TODO #

Once we have SpectralSpace, IsSpectralMap should move to Mathlib.Topology.Spectral.Basic.

structure IsSpectralMap {α : Type u_2} {β : Type u_3} [] [] (f : αβ) extends :

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

• isOpen_preimage : ∀ (s : Set β), IsOpen (f ⁻¹' s)
• isCompact_preimage_of_isOpen : ∀ ⦃s : Set β⦄, IsCompact (f ⁻¹' s)

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

Instances For
theorem IsSpectralMap.isCompact_preimage_of_isOpen {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (self : ) ⦃s : Set β :
IsCompact (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 IsCompact.preimage_of_isOpen {α : Type u_2} {β : Type u_3} [] [] {f : αβ} {s : Set β} (hf : ) (h₀ : ) (h₁ : ) :
theorem IsSpectralMap.continuous {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (hf : ) :
theorem isSpectralMap_id {α : Type u_2} [] :
theorem IsSpectralMap.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : βγ} {g : αβ} (hf : ) (hg : ) :
structure SpectralMap (α : Type u_6) (β : Type u_7) [] [] :
Type (max u_6 u_7)

The type of spectral maps from α to β.

• toFun : αβ

function between topological spaces

• spectral' : IsSpectralMap self.toFun

proof that toFun is a spectral map

Instances For
theorem SpectralMap.spectral' {α : Type u_6} {β : Type u_7} [] [] (self : ) :
IsSpectralMap self.toFun

proof that toFun is a spectral map

class SpectralMapClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [] [] [FunLike F α β] :

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

You should extend this class when you extend SpectralMap.

• map_spectral : ∀ (f : F),

statement that F is a type of spectral maps

Instances
@[simp]
theorem SpectralMapClass.map_spectral {F : Type u_6} {α : Type u_7} {β : Type u_8} [] [] [FunLike F α β] [self : ] (f : F) :

statement that F is a type of spectral maps

@[instance 100]
instance SpectralMapClass.toContinuousMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] :
Equations
• =
instance instCoeTCSpectralMapOfSpectralMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] :
CoeTC F ()
Equations
• instCoeTCSpectralMapOfSpectralMapClass = { coe := fun (f : F) => { toFun := f, spectral' := } }

### Spectral maps #

def SpectralMap.toContinuousMap {α : Type u_2} {β : Type u_3} [] [] (f : ) :
C(α, β)

Reinterpret a SpectralMap as a ContinuousMap.

Equations
• f.toContinuousMap = { toFun := f.toFun, continuous_toFun := }
Instances For
instance SpectralMap.instFunLike {α : Type u_2} {β : Type u_3} [] [] :
FunLike () α β
Equations
• SpectralMap.instFunLike = { coe := SpectralMap.toFun, coe_injective' := }
instance SpectralMap.instSpectralMapClass {α : Type u_2} {β : Type u_3} [] [] :
Equations
• =
@[simp]
theorem SpectralMap.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] {f : } :
f.toFun = f
theorem SpectralMap.ext {α : Type u_2} {β : Type u_3} [] [] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def SpectralMap.copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :

Copy of a SpectralMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• f.copy f' h = { toFun := f', spectral' := }
Instances For
@[simp]
theorem SpectralMap.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem SpectralMap.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def SpectralMap.id (α : Type u_2) [] :

id as a SpectralMap.

Equations
• = { toFun := id, spectral' := }
Instances For
instance SpectralMap.instInhabited (α : Type u_2) [] :
Equations
• = { default := }
@[simp]
theorem SpectralMap.coe_id (α : Type u_2) [] :
() = id
@[simp]
theorem SpectralMap.id_apply {α : Type u_2} [] (a : α) :
() a = a
def SpectralMap.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :

Composition of SpectralMaps as a SpectralMap.

Equations
• f.comp g = { toFun := (f.toContinuousMap.comp g.toContinuousMap), spectral' := }
Instances For
@[simp]
theorem SpectralMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem SpectralMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
(f.comp g) a = f (g a)
theorem SpectralMap.coe_comp_continuousMap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
f g = f g
@[simp]
theorem SpectralMap.coe_comp_continuousMap' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
(f.comp g) = (f).comp g
@[simp]
theorem SpectralMap.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 SpectralMap.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
f.comp () = f
@[simp]
theorem SpectralMap.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
().comp f = f
@[simp]
theorem SpectralMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g₁ : } {g₂ : } {f : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem SpectralMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g : } {f₁ : } {f₂ : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂