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 MvPolynomial.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.

Equations

• ⋯ = ⋯

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) : MvPolynomial.C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (MvPolynomial.C a) ⟨MvPolynomial.C ↑m, ⋯⟩

noncomputable def IsLocalization.Away.mvPolynomialQuotientEquiv {R : Type u_2} [CommRing R] (S : Type u_3) [CommRing S] [Algebra R S] (r : R) [IsLocalization.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) [IsLocalization.Away r S] (p : MvPolynomial Unit R) : (IsLocalization.Away.mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})) p) = (MvPolynomial.aeval fun (x : Unit) => IsLocalization.Away.invSelf r) p