English
For a closed subalgebra S of a Banach algebra A and x ∈ S, the boundary of the spectrum of x relative to S is contained in the boundary of the spectrum of x viewed as an element of A.
Русский
Для замкнутой подалгебры S Банаховой алгебры A и элемента x ∈ S граница спектра x относительно S содержится в границе спектра x как элемента A.
LaTeX
$$frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (x : A))$$
Lean4
/-- If `S : Subalgebra 𝕜 A` is a closed subalgebra of a Banach algebra `A`, then for any
`x : S`, the boundary of the spectrum of `x` relative to `S` is a subset of the spectrum of
`↑x : A` relative to `A`. -/
theorem _root_.Subalgebra.frontier_spectrum : frontier (σ 𝕜 x) ⊆ σ 𝕜 (x : A) :=
by
have : CompleteSpace S := hS.completeSpace_coe
intro μ hμ
by_contra h
rw [spectrum.notMem_iff] at h
rw [← frontier_compl, (spectrum.isClosed _).isOpen_compl.frontier_eq, mem_diff] at hμ
obtain ⟨hμ₁, hμ₂⟩ := hμ
rw [mem_closure_iff_clusterPt] at hμ₁
apply hμ₂
rw [mem_compl_iff, spectrum.notMem_iff]
refine Subalgebra.isUnit_of_isUnit_val_of_eventually S h ?_ ?_ <| .map hμ₁ (algebraMap 𝕜 S · - x)
·
calc
_ ≤ map _ (𝓝 μ) := map_mono (by simp)
_ ≤ _ := by rw [← Filter.Tendsto, ← ContinuousAt]; fun_prop
· rw [eventually_map]
apply Eventually.filter_mono inf_le_right
simp [spectrum.notMem_iff]
