English
The complement of the spectrum of a self-adjoint element in a C*-algebra is connected.
Русский
Дополнение спектра сам-сопряженного элемента в C*-алгебре связано.
LaTeX
$$$$\text{IsConnected}(\sigma_{\mathbb{C}}(a))^{c}.$$$$
Lean4
/-- The complement of the spectrum of a selfadjoint element in a C⋆-algebra is connected. -/
theorem isConnected_spectrum_compl {a : A} (ha : IsSelfAdjoint a) : IsConnected (σ ℂ a)ᶜ :=
by
suffices IsConnected (((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}) ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})
by
rw [← Set.inter_union_distrib_left, ← Set.setOf_or] at this
rw [← Set.inter_univ (σ ℂ a)ᶜ]
convert this using 2
exact Eq.symm <| Set.eq_univ_of_forall (fun z ↦ le_total 0 z.im)
refine IsConnected.union ?nonempty ?upper ?lower
case
nonempty =>
have :=
Filter.NeBot.nonempty_of_mem inferInstance <|
Filter.mem_map.mp <| Complex.isometry_ofReal.antilipschitz.tendsto_cobounded (spectrum.isBounded a |>.compl)
exact this.image Complex.ofReal |>.mono <| by simp
case' upper => apply Complex.isConnected_of_upperHalfPlane ?_ <| Set.inter_subset_right
case' lower => apply Complex.isConnected_of_lowerHalfPlane ?_ <| Set.inter_subset_right
all_goals
refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)
rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz
simp_all
