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

• 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.

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)

• toFun : α → β

  function between topological spaces

• spectral' : IsSpectralMap s.toFun

  proof that toFun is a spectral map

The type of spectral maps from α to β.

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

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• map_spectral : ∀ (f : F), IsSpectralMap ↑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.

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

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

Spectral maps

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

Reinterpret a SpectralMap as a ContinuousMap.

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

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

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

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

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

@[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₂