Constant coefficients in polynomial local rings #
The constant coefficient map from a multivariate polynomial ring over a local ring extends to the localization at the preimage of the coefficient ring's maximal ideal. It detects when a polynomial is outside the square of the maximal ideal of that localization.
Main results #
TauCeti.algebraMap_notMem_maximalIdeal_sq: a polynomial whose constant coefficient is outside the square of the coefficient ring's maximal ideal remains outside the square after localization.
theorem
TauCeti.algebraMap_notMem_maximalIdeal_sq
{R : Type u_1}
{σ : Type u_2}
[CommRing R]
[IsLocalRing R]
{p : MvPolynomial σ R}
(hp : MvPolynomial.constantCoeff p ∉ IsLocalRing.maximalIdeal R ^ 2)
:
A polynomial whose constant coefficient is not in 𝔪_R² does not lie in the square of the
maximal ideal of R[σ]_𝔪: the constant coefficient extends to R[σ]_𝔪 → R, which maps the
maximal ideal into 𝔪_R.