spectrum_eq_preimage_range — Mathlib

English

Another formulation: spectrum 𝕜 f equals the preimage under the algebra map of the range of f, for f: X → R with appropriate structure.

Русский

Ещё одно формулирование: спектр 𝕜 f равен предобразу под алгебраическим отображением диапазона f.

LaTeX

$$$\mathrm{spectrum}_{\mathbb{K}}(f) = (\mathrm{algebraMap}_{\mathbb{K}, R})^{-1}(\mathrm{range}(f)).$$$

Lean4

theorem spectrum_eq_preimage_range (f : C(X, R)) : spectrum 𝕜 f = algebraMap _ _ ⁻¹' Set.range f :=
  by
  ext x
  simp only [spectrum.mem_iff, isUnit_iff_forall_ne_zero, not_forall, sub_apply, Classical.not_not, Set.mem_range,
    sub_eq_zero, @eq_comm _ (x • 1 : R) _, Set.mem_preimage, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply]

Похожие утверждения