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} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) extends Continuous : Prop

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 s → IsOpen (f ⁻¹' s)
• isCompact_preimage_of_isOpen : ∀ ⦃s : Set β⦄, IsOpen s → IsCompact s → 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} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set β} (hf : IsSpectralMap f) (h₀ : IsCompact s) (h₁ : IsOpen s) : IsCompact (f ⁻¹' s)

theorem IsSpectralMap.continuous {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsSpectralMap f) : Continuous f

theorem isSpectralMap_id {α : Type u_2} [TopologicalSpace α] : IsSpectralMap id

theorem IsSpectralMap.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : β → γ} {g : α → β} (hf : IsSpectralMap f) (hg : IsSpectralMap g) : IsSpectralMap (f ∘ g)

structure SpectralMap (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] : 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

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

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

You should extend this class when you extend SpectralMap.

• map_spectral : ∀ (f : F), IsSpectralMap ⇑f

  statement that F is a type of spectral maps

instance SpectralMapClass.toContinuousMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [SpectralMapClass F α β] : ContinuousMapClass F α β

Equations

• ⋯ = ⋯

instance instCoeTCSpectralMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [SpectralMapClass F α β] : CoeTC F (SpectralMap α β)

Equations

• instCoeTCSpectralMap = { coe := fun (f : F) => { toFun := ⇑f, spectral' := ⋯ } }

Spectral maps

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

Reinterpret a SpectralMap as a ContinuousMap.

Equations

• SpectralMap.toContinuousMap f = { toFun := f.toFun, continuous_toFun := ⋯ }

instance SpectralMap.instFunLike {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] : FunLike (SpectralMap α β) α β

Equations

• SpectralMap.instFunLike = { coe := SpectralMap.toFun, coe_injective' := ⋯ }

instance SpectralMap.instSpectralMapClassSpectralMapInstFunLike {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] : SpectralMapClass (SpectralMap α β) α β

Equations

• ⋯ = ⋯

@[simp]

theorem SpectralMap.toFun_eq_coe {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : SpectralMap α β} : f.toFun = ⇑f

theorem SpectralMap.ext {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : SpectralMap α β} {g : SpectralMap α β} (h : ∀ (a : α), f a = g a) : f = g

def SpectralMap.copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : SpectralMap α β) (f' : α → β) (h : f' = ⇑f) : SpectralMap α β

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

Equations

• SpectralMap.copy f f' h = { toFun := f', spectral' := ⋯ }

@[simp]

theorem SpectralMap.coe_copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : SpectralMap α β) (f' : α → β) (h : f' = ⇑f) : ⇑(SpectralMap.copy f f' h) = f'

theorem SpectralMap.copy_eq {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : SpectralMap α β) (f' : α → β) (h : f' = ⇑f) : SpectralMap.copy f f' h = f

def SpectralMap.id (α : Type u_2) [TopologicalSpace α] : SpectralMap α α

id as a SpectralMap.

Equations

• SpectralMap.id α = { toFun := id, spectral' := ⋯ }

instance SpectralMap.instInhabitedSpectralMap (α : Type u_2) [TopologicalSpace α] : Inhabited (SpectralMap α α)

Equations

• SpectralMap.instInhabitedSpectralMap α = { default := SpectralMap.id α }

@[simp]

theorem SpectralMap.coe_id (α : Type u_2) [TopologicalSpace α] : ⇑(SpectralMap.id α) = id

@[simp]

theorem SpectralMap.id_apply {α : Type u_2} [TopologicalSpace α] (a : α) : (SpectralMap.id α) a = a

def SpectralMap.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β) : SpectralMap α γ

Composition of SpectralMaps as a SpectralMap.

Equations

• SpectralMap.comp f g = { toFun := ⇑(ContinuousMap.comp (SpectralMap.toContinuousMap f) (SpectralMap.toContinuousMap g)), spectral' := ⋯ }

@[simp]

theorem SpectralMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β) : ⇑(SpectralMap.comp f g) = ⇑f ∘ ⇑g

@[simp]

theorem SpectralMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β) (a : α) : (SpectralMap.comp f g) a = f (g a)

@[simp]

theorem SpectralMap.coe_comp_continuousMap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β) : ⇑f ∘ ⇑g = ⇑↑f ∘ ⇑↑g

theorem SpectralMap.coe_comp_continuousMap' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β) : ↑(SpectralMap.comp f g) = ContinuousMap.comp ↑f ↑g

@[simp]

theorem SpectralMap.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (f : SpectralMap γ δ) (g : SpectralMap β γ) (h : SpectralMap α β) : SpectralMap.comp (SpectralMap.comp f g) h = SpectralMap.comp f (SpectralMap.comp g h)

@[simp]

theorem SpectralMap.comp_id {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : SpectralMap α β) : SpectralMap.comp f (SpectralMap.id α) = f

@[simp]

theorem SpectralMap.id_comp {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : SpectralMap α β) : SpectralMap.comp (SpectralMap.id β) f = f

@[simp]

theorem SpectralMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g₁ : SpectralMap β γ} {g₂ : SpectralMap β γ} {f : SpectralMap α β} (hf : Function.Surjective ⇑f) : SpectralMap.comp g₁ f = SpectralMap.comp g₂ f ↔ g₁ = g₂

@[simp]

theorem SpectralMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : SpectralMap β γ} {f₁ : SpectralMap α β} {f₂ : SpectralMap α β} (hg : Function.Injective ⇑g) : SpectralMap.comp g f₁ = SpectralMap.comp g f₂ ↔ f₁ = f₂