English
For a morphism of rings R → S and A an algebra over both, the preimage of the spectrum of a ∈ A under the algebra map algebraMap(R,S) equals the spectrum of a considered as an element of R-algebra A.
Русский
Для морфизма колец R → S и алгебры A над ними, предобраз спектра элемента a ∈ A через алгебраическую карту algebraMap(R,S) равен спектру того же элемента a, рассматриваемого как элемент над R.
LaTeX
$$$\operatorname{preimage}(\operatorname{algebraMap}(R,S), \sigma_S(a)) = \sigma_R(a)$$$
Lean4
@[simp]
theorem preimage_algebraMap (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} : algebraMap R S ⁻¹' spectrum S a = spectrum R a :=
Set.ext fun _ => spectrum.algebraMap_mem_iff _
