English
Let R → S be a morphism of commutative semirings with A a ring, and compatible algebra structures so that R → S → A is a scalar tower. For any a ∈ A, the image of r under algebraMap(R,S) lies in the spectrum of a over S if and only if r lies in the spectrum of a over R.
Русский
Пусть R → S – морфизм коммутативных полускол, A – кольцо, и существуют подходящие структуры алгебры так, что образчик R в S и далее в A образуют стековую структура. Для любого a ∈ A выполняется: algebraMap(R,S)(r) ∈ спектр_S(a) ⇔ r ∈ спектр_R(a).
LaTeX
$$$\operatorname{algebraMap} R S\; r \in \sigma_S(a) \iff r \in \sigma_R(a)$$$
Lean4
@[simp]
theorem algebraMap_mem_iff (S : Type*) {R A : Type*} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S]
[Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} :
algebraMap R S r ∈ spectrum S a ↔ r ∈ spectrum R a := by
simp only [spectrum.mem_iff, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
