Localization and multivariate polynomial rings

In this file we show some results connecting multivariate polynomial rings and localization.

Main results

• MvPolynomial.isLocalization: If S is the localization of R at a submonoid M, then MvPolynomial σ S is the localization of MvPolynomial σ R at the image of M in MvPolynomial σ R.

instance MvPolynomial.isLocalization {σ : Type u_1} {R : Type u_2} [CommRing R] (M : Submonoid R) (S : Type u_3) [CommRing S] [Algebra R S] [IsLocalization M S] : IsLocalization (Submonoid.map C M) (MvPolynomial σ S)

If S is the localization of R at a submonoid M, then MvPolynomial σ S is the localization of MvPolynomial σ R at M.map MvPolynomial.C.

See also Polynomial.isLocalization for the univariate case.

theorem MvPolynomial.isLocalization_C_mk' {σ : Type u_1} {R : Type u_2} [CommRing R] (M : Submonoid R) (S : Type u_3) [CommRing S] [Algebra R S] [IsLocalization M S] (a : R) (m : ↥M) : C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (C a) ⟨C ↑m, ⋯⟩

noncomputable def IsLocalization.Away.mvPolynomialQuotientEquiv {R : Type u_2} [CommRing R] (S : Type u_3) [CommRing S] [Algebra R S] (r : R) [Away r S] : (MvPolynomial Unit R ⧸ Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1}) ≃ₐ[R] S

The canonical algebra isomorphism from MvPolynomial Unit R quotiented by C r * X () - 1 to the localization of R away from r.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsLocalization.Away.mvPolynomialQuotientEquiv_apply {R : Type u_2} [CommRing R] (S : Type u_3) [CommRing S] [Algebra R S] (r : R) [Away r S] (p : MvPolynomial Unit R) : (mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})) p) = (MvPolynomial.aeval fun (x : Unit) => invSelf r) p