Theorems · Definition · functional analysis

NormedRing.algEquivComplexOfComplete

• 1000+ list: Gelfand–Mazur theorem

{A : Type u_2} →
  [inst : NormedRing A] → [inst_1 : NormedAlgebra ℂ A] → [CompleteSpace A] → (∀ {a : A}, IsUnit a ↔ a ≠ 0) → ℂ ≃ₐ[ℂ] A

Gelfand-Mazur theorem: For a complex Banach division algebra, the natural algebraMap ℂ A is an algebra isomorphism whose inverse is given by selecting the (unique) element of spectrum ℂ a. In addition, algebraMap_isometry guarantees this map is an isometry. Note: because NormedDivisionRing requires the field norm_mul : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖, we don't use this type class and instead opt for a NormedRing in which the nonzero elements are precisely the units. This allows for the application of this isomorphism in broader contexts, e.g., to the quotient of a complex Banach algebra by a maximal ideal. In the case when A is actually a NormedDivisionRing, one may fill in the argument hA with the lemma isUnit_iff_ne_zero.

Defined in

Mathlib.Analysis.Normed.Algebra.GelfandFormula

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedRingNormedAlgebraCompleteSpace