Theorems · Theorem · functional analysis

Subalgebra.spectrum_sUnion_connectedComponentIn

∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A]
  (S : SA) [hS : IsClosed ↑S] (x : ↥S),
  spectrum 𝕜 x = spectrum 𝕜 ↑x ∪ ⋃ z ∈ spectrum 𝕜 x \ spectrum 𝕜 ↑x, connectedComponentIn (spectrum 𝕜 ↑x)ᶜ z

If S is a closed subalgebra of a Banach algebra A, then for any x : S, the spectrum of x is the spectrum of ↑x : A along with the connected components of the complement of the spectrum of ↑x : A which contain an element of the spectrum of x : S.

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

2 results in Mathlib

Foundations

Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedRingCompleteSpaceSetLikeSubringClassNormedFieldNormedAlgebraSMulMemClassIsClosed