The standard grading on a multivariate polynomial ring

Besides naming the grading, this file records that the polynomial variables generate the ring over its degree-zero homogeneous submodule. Projective-space files consume that algebraic generation theorem when proving cover and finite-type statements.

@[reducible, inline]

abbrev MvPolynomial.polynomialGrading (ι R : Type u) [CommRing R] : ℕ → Submodule R (MvPolynomial ι R)

The standard total-degree grading on a multivariate polynomial ring.

Equations

• MvPolynomial.polynomialGrading ι R = MvPolynomial.homogeneousSubmodule ι R

theorem MvPolynomial.polynomialVariable_adjoin_eq_top (ι k : Type u) [Field k] : Algebra.adjoin (↥(polynomialGrading ι k 0)) (Set.range fun (i : ι) => X i) = ⊤

The variables generate a polynomial ring over its degree-zero homogeneous submodule.