apply_mem_spectrum — Mathlib

English

If f is an algebra equivalence A ≃ₐ[R] B, then spectrum_R(f(a)) = spectrum_R(a) for all a ∈ A.

Русский

Если f — алгебраическое эквивалентность A ≃ₐ[R] B, то спектр сохраняется: spectrum_R(f(a)) = spectrum_R(a).

LaTeX

$$$\operatorname{spectrum}_R(f(a)) = \operatorname{spectrum}_R(a)$$$

Lean4

theorem apply_mem_spectrum [Nontrivial R] (φ : F) (a : A) : φ a ∈ σ a :=
  by
  have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
    simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes, Algebra.algebraMap_self,
      RingHom.id_apply, sub_self]
  simp only [spectrum.mem_iff, ← mem_nonunits_iff, coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]

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