English
If A is the localization of R at M, then A[X] is the localization of R[X] at M.map Polynomial.C.
Русский
Если $A$ — локализация $R$ по $M$, то $A[X]$ есть локализация $R[X]$ по $M.map\\,C$.
LaTeX
$$$IsLocalization\\ S A[X] \\quad \\text{with } A = \\text{Localization at } M$$$
Lean4
/-- If `A` is the localization of `R` at a submonoid `S`, then `A[X]` is the localization of
`R[X]` at `S.map Polynomial.C`.
See also `MvPolynomial.isLocalization` for the multivariate case. -/
theorem isLocalization {R} [CommSemiring R] (S : Submonoid R) (A) [CommSemiring A] [Algebra R A] [IsLocalization S A] :
letI := (mapRingHom (algebraMap R A)).toAlgebra
IsLocalization (S.map C) A[X] :=
letI := (mapRingHom (algebraMap R A)).toAlgebra
have : IsScalarTower R R[X] A[X] := .of_algebraMap_eq fun _ ↦ (map_C _).symm
isLocalizedModule_iff_isLocalization.mp <|
(isLocalizedModule_iff_isBaseChange S A _).mpr <|
.of_equiv (polyEquivTensor' R A).symm.toLinearEquiv fun _ ↦ by simp
