English
Gelfand–Mazur theorem: for a complex Banach division algebra A, the natural algebra map ℂ → A is an algebra isomorphism; its inverse is given by the unique element of the spectrum, and the map is an isometry.
Русский
Теорема Гельфанда-Мазура: для комплексной банаховой деловой алгебры A естественная алгебраическая карта ℂ → A является алгеброизоморфизмом; ее обратная карта задаётся единственным элементом спектра, а эта карта сохраняет норму (есть изометрия).
LaTeX
$$$\\mathbb{C} \\cong_{\\mathbb{C}} A$ (existence of an algebra isomorphism) when A is a complex Banach division algebra$$
Lean4
/-- In a (nontrivial) complex Banach algebra, every element has nonempty spectrum. -/
protected theorem nonempty (a : A) : (spectrum ℂ a).Nonempty := by
/- Suppose `σ a = ∅`, then resolvent set is `ℂ`, any `(z • 1 - a)` is a unit, and `resolvent a`
is differentiable on `ℂ`. -/
by_contra! h
have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h
have H₁ : Differentiable ℂ fun z : ℂ => resolvent a z := fun z =>
(hasDerivAt_resolvent (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)).differentiableAt
have H₃ :=
H₁.apply_eq_of_tendsto_cocompact 0 <| by
simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)
exact not_isUnit_zero <| H₃ ▸ (isUnit_resolvent.mp <| H₀.symm ▸ Set.mem_univ 0)
