English
If for x ∈ S the complement of the spectrum of x in the ambient algebra is preconnected, then the spectrum of x in S equals the spectrum of x in A.
Русский
Если комплемент спектра x в области A предварительно связный, то спектр x в S равен спектру x в A.
LaTeX
$$σ 𝕜 x = σ 𝕜 (x : A) under IsPreconnected ((σ 𝕜 (x : A))ᶜ)$$
Lean4
/-- 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`. -/
theorem spectrum_sUnion_connectedComponentIn :
σ 𝕜 x = σ 𝕜 (x : A) ∪ (⋃ z ∈ (σ 𝕜 x \ σ 𝕜 (x : A)), connectedComponentIn (σ 𝕜 (x : A))ᶜ z) :=
by
suffices IsClopen ((σ 𝕜 (x : A))ᶜ ↓∩ (σ 𝕜 x \ σ 𝕜 (x : A))) by
rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _), union_diff_cancel (spectrum.subset_subalgebra x)]
have : CompleteSpace S := hS.completeSpace_coe
have h_open : IsOpen (σ 𝕜 x \ σ 𝕜 (x : A)) :=
by
rw [← (spectrum.isClosed (𝕜 := 𝕜) x).closure_eq, closure_eq_interior_union_frontier, union_diff_distrib,
diff_eq_empty.mpr (frontier_spectrum S x), diff_eq_compl_inter, union_empty]
exact (spectrum.isClosed _).isOpen_compl.inter isOpen_interior
apply isClopen_preimage_val h_open
suffices h_frontier : frontier (σ 𝕜 x \ σ 𝕜 (x : A)) ⊆ frontier (σ 𝕜 (x : A)) from
disjoint_of_subset_left h_frontier <| disjoint_compl_right.frontier_left (spectrum.isClosed _).isOpen_compl
rw [diff_eq_compl_inter]
apply (frontier_inter_subset _ _).trans
rw [frontier_compl]
apply union_subset <| inter_subset_left
refine inter_subset_inter_right _ ?_ |>.trans <| inter_subset_right
exact frontier_subset_frontier S x
