English
If S is the localization of R away from r, we obtain a natural presentation of S as an R-algebra with a single generator X and the relation r·X − 1 = 0.
Русский
Если S является локализацией R отпалённой от r, то получаем естественную презентацию S как R-алгебры с одним генератором X и отношением r·X − 1 = 0.
LaTeX
$$$\\mathrm{localizationAway}\\\\ S\\\\ r:\\; \\mathrm{Presentation}\\\\ R\\\\ S\\\\ units \\\\rightarrow (C r \\cdot X() - 1)$$$
Lean4
theorem _root_.Algebra.Generators.ker_localizationAway :
(Generators.localizationAway S r).ker = Ideal.span {C r * X () - 1} :=
by
have :
aeval (S₁ := S) (Generators.localizationAway S r).val =
(mvPolynomialQuotientEquiv S r).toAlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1})) :=
by
ext x
simp only [aeval_X, Generators.localizationAway_val, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe,
Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply]
rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]
rw [Generators.ker_eq_ker_aeval_val, this, AlgEquiv.toAlgHom_eq_coe, ← RingHom.ker_coe_toRingHom,
AlgHom.comp_toRingHom, ← RingHom.comap_ker]
simp only [AlgEquiv.toAlgHom_toRingHom]
change Ideal.comap _ (RingHom.ker (mvPolynomialQuotientEquiv S r)) = Ideal.span {C r * X () - 1}
simp [RingHom.ker_equiv, ← RingHom.ker_eq_comap_bot]
