The homogeneous components of an ℕ-graded ring as a polynomial

Let A be a ring graded by 𝒜 : ℕ → σ. Recording the homogeneous components aₙ of a ∈ A as the coefficients of a polynomial gives a ring homomorphism

A →+* A[X], a ↦ ∑ₙ aₙ Xⁿ.

An element a is homogeneous of degree n exactly when it is sent to the monomial a Xⁿ. This turns homogeneity into an equation in a ring, so that it can be transported along constructions which commute with ring homomorphisms. Under it, a family of elements a_d with a_d ∈ 𝒜 (w d) becomes the family a_d X^(w d): the grading is the action of a polynomial variable.

Main definitions

• TauCeti.GradedAlgebra.toPolynomial: the ring homomorphism a ↦ ∑ₙ aₙ Xⁿ.

Main results

• TauCeti.GradedAlgebra.coeff_toPolynomial: the coefficient of Xⁿ is the component of degree n.
• TauCeti.GradedAlgebra.toPolynomial_eq_monomial_iff: a is sent to a Xⁿ exactly when a is homogeneous of degree n.
• RingHom.map_toPolynomial_eq_iff: a ring homomorphism preserves the grading exactly when it intertwines these polynomial-valued maps.
• PowerSeries.map_toPolynomial_eq_mk_iff: a power series has its coefficient of Yⁿ in degree n - 1 exactly when its base change along a ↦ ∑ₙ aₙ Xⁿ is ∑ₙ Xⁿ⁻¹ aₙ Yⁿ.

noncomputable def TauCeti.GradedAlgebra.toPolynomial {A : Type u_1} {σ : Type u_2} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] : A →+* Polynomial A

The ring homomorphism A →+* A[X] sending an element a of an ℕ-graded ring to the polynomial ∑ₙ aₙ Xⁿ whose coefficients are its homogeneous components.

theorem TauCeti.GradedAlgebra.toPolynomial_of_mem {A : Type u_1} {σ : Type u_2} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] {a : A} {n : ℕ} (ha : a ∈ 𝒜 n) : (toPolynomial 𝒜) a = (Polynomial.monomial n) a

A homogeneous element a of degree n is sent to the monomial a Xⁿ.

@[simp]

theorem TauCeti.GradedAlgebra.coeff_toPolynomial {A : Type u_1} {σ : Type u_2} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (a : A) (n : ℕ) : ((toPolynomial 𝒜) a).coeff n = ↑(((DirectSum.decompose 𝒜) a) n)

The coefficient of Xⁿ in the image of a is the homogeneous component of a of degree n.

theorem TauCeti.GradedAlgebra.toPolynomial_eq_monomial_iff {A : Type u_1} {σ : Type u_2} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] {a : A} {n : ℕ} : (toPolynomial 𝒜) a = (Polynomial.monomial n) a ↔ a ∈ 𝒜 n

Homogeneity as an equation: a is sent to the monomial a Xⁿ exactly when it is homogeneous of degree n.

@[simp]

theorem GradedRingHom.map_toPolynomial {A : Type u_1} {B : Type u_2} {σ : Type u_3} {τ : Type u_4} [Semiring A] [Semiring B] [SetLike σ A] [AddSubmonoidClass σ A] [SetLike τ B] [AddSubmonoidClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (a : A) : Polynomial.map (↑f) ((TauCeti.GradedAlgebra.toPolynomial 𝒜) a) = (TauCeti.GradedAlgebra.toPolynomial ℬ) (f a)

A graded ring homomorphism commutes with recording homogeneous components as polynomial coefficients.

theorem RingHom.map_toPolynomial_eq_iff {A : Type u_1} {B : Type u_2} {σ : Type u_3} {τ : Type u_4} [Semiring A] [Semiring B] [SetLike σ A] [AddSubmonoidClass σ A] [SetLike τ B] [AddSubmonoidClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : A →+* B) : (∀ (a : A), Polynomial.map f ((TauCeti.GradedAlgebra.toPolynomial 𝒜) a) = (TauCeti.GradedAlgebra.toPolynomial ℬ) (f a)) ↔ ∀ (n : ℕ), ∀ a ∈ 𝒜 n, f a ∈ ℬ n

A ring homomorphism preserves the grading exactly when it intertwines the universal scalar actions recorded by toPolynomial. The scalar is an indeterminate, not just an element of the coefficient ring.

theorem PowerSeries.map_toPolynomial_eq_mk_iff {A : Type u_1} {σ : Type u_2} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (g : PowerSeries A) : ((map (TauCeti.GradedAlgebra.toPolynomial 𝒜)) g = mk fun (n : ℕ) => Polynomial.X ^ (n - 1) * (coeff n) ((map Polynomial.C) g)) ↔ ∀ (n : ℕ), (coeff n) g ∈ 𝒜 (n - 1)

A power series has its coefficient of Yⁿ in degree n - 1 exactly when its base change along a ↦ ∑ₙ aₙ Xⁿ is the series ∑ₙ Xⁿ⁻¹ aₙ Yⁿ.