Graded modules over a polynomial ring

This file records the basic behavior of the action of k[X] on an internally ℤ-graded module on which X lowers degree by a fixed d, and equips k[X] itself with the internal grading that places X ^ n in degree -n.

Main definitions

• TauCeti.Polynomial.negDegreeGrading: the grading of k[X] placing X ^ n in degree -n.

Main results

• TauCeti.InternalGrading.X_pow_smul_mem_piece: if X lowers degree by d, then X ^ n lowers degree by n * d.
• TauCeti.InternalGrading.bddAbove_setOf_piece_ne_bot: a finitely generated graded k[X]-module on which X lowers degree has no nonzero homogeneous elements above some degree.
• TauCeti.InternalGrading.coe_decompose_smul_of_mem: when X lowers degree by a nonzero d, the homogeneous components of a • x, for x homogeneous, are the terms a.coeff n • X ^ n • x.
• TauCeti.InternalGrading.coe_decompose_smul_of_support_le: at an upper bound for the support, polynomial multiplication acts on the component by the constant coefficient.
• TauCeti.InternalGrading.smul_injective_of_coeff_zero_ne_zero: a polynomial with nonzero constant coefficient acts injectively when the coefficients form a domain and the module is torsion-free over them.
• TauCeti.Polynomial.mem_negDegreeGrading_piece: membership in a homogeneous piece is characterized coefficientwise.
• TauCeti.Polynomial.X_smul_mem_negDegreeGrading_piece: multiplication by X lowers degree by one.
• TauCeti.Polynomial.X_pow_mem_negDegreeGrading_piece: X ^ n has degree -n.

theorem TauCeti.InternalGrading.X_pow_smul_mem_piece {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] {G : InternalGrading k M} {d : ℕ} (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p - ↑d)) (n : ℕ) {p : ℤ} {x : M} (hx : x ∈ G.piece p) : Polynomial.X ^ n • x ∈ G.piece (p - ↑n * ↑d)

If X lowers degree by d, then X ^ n lowers degree by n * d.

theorem TauCeti.InternalGrading.bddAbove_setOf_piece_ne_bot {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] {G : InternalGrading k M} {d : ℕ} [Module.Finite (Polynomial k) M] (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p - ↑d)) : BddAbove {p : ℤ | G.piece p ≠ ⊥}

A finitely generated graded k[X]-module on which X lowers degree has no nonzero homogeneous elements above some degree: every element is a k[X]-combination of the finitely many homogeneous components of a finite generating set, and multiplication by a polynomial never raises degree.

theorem TauCeti.InternalGrading.coe_decompose_smul_of_mem {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] {G : InternalGrading k M} {d : ℕ} (hd : d ≠ 0) (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p - ↑d)) {p : ℤ} {x : M} (hx : x ∈ G.piece p) (a : Polynomial k) (n : ℕ) : ↑(((DirectSum.decompose G.piece) (a • x)) (p - ↑n * ↑d)) = a.coeff n • Polynomial.X ^ n • x

If X lowers degree by d ≠ 0, the terms a.coeff n • X ^ n • x of a • x, for x homogeneous of degree p, lie in the pairwise distinct degrees p - n * d; so the component of a • x in degree p - n * d is the n-th of them.

theorem TauCeti.InternalGrading.coe_decompose_smul_of_support_le {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] {G : InternalGrading k M} {d : ℕ} (hd : d ≠ 0) (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p - ↑d)) {p : ℤ} {x : M} (hx : ∀ (q : ℤ), p < q → ↑(((DirectSum.decompose G.piece) x) q) = 0) (a : Polynomial k) : ↑(((DirectSum.decompose G.piece) (a • x)) p) = a.coeff 0 • ↑(((DirectSum.decompose G.piece) x) p)

At an upper bound for the degrees of the nonzero components of x, polynomial multiplication acts on the component by its constant coefficient, provided X strictly lowers degree.

theorem TauCeti.InternalGrading.smul_injective_of_coeff_zero_ne_zero {k : Type u_1} {M : Type u_2} [CommRing k] [IsDomain k] [AddCommGroup M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] [Module.IsTorsionFree k M] {G : InternalGrading k M} {d : ℕ} (hd : d ≠ 0) (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p - ↑d)) {a : Polynomial k} (ha : a.coeff 0 ≠ 0) : Function.Injective fun (x : M) => a • x

A polynomial with nonzero constant coefficient acts injectively on a module graded over a coefficient domain, if the module is torsion-free over the coefficients and X strictly lowers degree. Polynomial torsion in the module is permitted.

noncomputable def TauCeti.Polynomial.negDegreeGrading (k : Type u_1) [CommSemiring k] : InternalGrading k (Polynomial k)

The grading of the polynomial ring k[X] placing the monomial X ^ n in degree -n, so that multiplication by X lowers degree by one.

Equations

• TauCeti.Polynomial.negDegreeGrading k = { piece := AddMonoidAlgebra.gradeBy k ⇑(-Nat.castAddMonoidHom ℤ), isInternal := ⋯ }.map (Polynomial.toFinsuppIsoLinear k).symm

@[simp]

theorem TauCeti.Polynomial.mem_negDegreeGrading_piece {k : Type u_1} [CommSemiring k] {p : ℤ} {x : Polynomial k} : x ∈ (negDegreeGrading k).piece p ↔ ∀ (n : ℕ), x.coeff n ≠ 0 → -↑n = p

A polynomial has degree p in negDegreeGrading exactly when each of its monomials X ^ n has -n = p.

theorem TauCeti.Polynomial.X_smul_mem_negDegreeGrading_piece {k : Type u_1} [CommSemiring k] {p : ℤ} {x : Polynomial k} (hx : x ∈ (negDegreeGrading k).piece p) : Polynomial.X • x ∈ (negDegreeGrading k).piece (p - 1)

Multiplication by X lowers the degree of negDegreeGrading by one.

theorem TauCeti.Polynomial.X_pow_mem_negDegreeGrading_piece {k : Type u_1} [CommSemiring k] (n : ℕ) : Polynomial.X ^ n ∈ (negDegreeGrading k).piece (-↑n)

The monomial X ^ n has degree -n in negDegreeGrading.