# Documentation

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

• 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 topology.spectral.basic.

structure IsSpectralMap {α : Type u_2} {β : Type u_3} [] [] (f : αβ) extends :
• 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.

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 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)
• toFun : αβ

function between topological spaces

• spectral' : IsSpectralMap s.toFun

proof that toFun is a spectral map

The type of spectral maps from α to β.

Instances For
class SpectralMapClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_spectral : ∀ (f : F),

statement that F is a type of spectral maps

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

You should extend this class when you extend SpectralMap.

Instances
instance SpectralMapClass.toContinuousMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
instance instCoeTCSpectralMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
CoeTC F ()

### Spectral maps #

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

Reinterpret a SpectralMap as a ContinuousMap.

Instances For
instance SpectralMap.instSpectralMapClassSpectralMap {α : Type u_2} {β : Type u_3} [] [] :
@[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.

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

id as a SpectralMap.

Instances For
@[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.

Instances For
@[simp]
theorem SpectralMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
↑() = f g
@[simp]
theorem SpectralMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) (a : α) :
↑() a = f (g a)
@[simp]
theorem SpectralMap.coe_comp_continuousMap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
f g = f g
theorem SpectralMap.coe_comp_continuousMap' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : ) (g : ) :
↑() =
@[simp]
theorem SpectralMap.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : ) (g : ) (h : ) :
=
@[simp]
theorem SpectralMap.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : ) :
= f
@[simp]
theorem SpectralMap.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : ) :
= f
@[simp]
theorem SpectralMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g₁ : } {g₂ : } {f : } (hf : ) :
= g₁ = g₂
@[simp]
theorem SpectralMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g : } {f₁ : } {f₂ : } (hg : ) :
= f₁ = f₂