Homogeneous torsion in graded polynomial modules

Suppose M is internally integer graded over a domain k, is torsion-free over k, and multiplication by X strictly lowers degree. Then its k[X]-torsion submodule is precisely its X-power torsion submodule, even for elements with several homogeneous components. This torsion submodule is homogeneous, so it and its quotient inherit gradings through InternalGrading.submodule and InternalGrading.quotient, after restricting scalars to k. Over a field, finite generation gives a single power of X annihilating the entire torsion submodule; the ambient module need not be torsion.

The primary-torsion equality supplies the hypothesis on the torsion submodule for Mathlib's Module.torsion_by_prime_power_decomposition. The torsion submodule also admits a homogeneous polynomial-linear complement. This file does not construct homogeneous cyclic generators or a bigraded decomposition. Examples use the existing negative-degree polynomial grading and its induced quotient grading on k[X] / (X²).

Main results

• InternalGrading.torsion_eq_torsion'_powers_X: polynomial torsion is X-power torsion.
• InternalGrading.isHomogeneous_torsion: every component of a torsion element is torsion.
• InternalGrading.torsion_eq_torsionBy_X_pow: for a finitely generated module over a field, its torsion submodule is the kernel of a single power of X.
• InternalGrading.exists_isCompl_torsion_of_X_smul_mem_piece: torsion has a homogeneous polynomial-linear complement.

theorem TauCeti.InternalGrading.torsion_eq_torsion'_powers_X {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)) : Submodule.torsion (Polynomial k) M = Submodule.torsion' (Polynomial k) M ↥(Submonoid.powers Polynomial.X)

If X strictly lowers degree in a module torsion-free over its coefficient domain, the polynomial torsion submodule equals the submodule of elements killed by powers of X. No homogeneity assumption on the elements is needed.

theorem TauCeti.InternalGrading.isHomogeneous_torsion {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)) : DirectSum.SetLike.IsHomogeneous G.piece (Submodule.torsion (Polynomial k) M)

The torsion submodule of a graded polynomial module is homogeneous if X strictly lowers degree and the module is torsion-free over its coefficient domain. In particular its scalar restriction is a valid input to the existing submodule and quotient grading constructors.

theorem TauCeti.InternalGrading.torsion_eq_torsionBy_X_pow {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] [Module.Finite (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)) : ∃ (N : ℕ), Submodule.torsion (Polynomial k) M = Submodule.torsionBy (Polynomial k) M (Polynomial.X ^ N)

Over a field, the torsion submodule of a finitely generated graded polynomial module is annihilated by one power of X, and equals the kernel of that power. The module itself need not be torsion. The exponent may be zero when the torsion submodule is zero.

theorem TauCeti.InternalGrading.exists_isCompl_torsion_of_X_smul_mem_piece {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] [Module.Finite (Polynomial k) M] {d : ℕ} (G : InternalGrading k M) (hd : d ≠ 0) (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece p → Polynomial.X • x ∈ G.piece (p - ↑d)) : ∃ (L : Submodule (Polynomial k) M), IsCompl (Submodule.torsion (Polynomial k) M) L ∧ DirectSum.SetLike.IsHomogeneous G.piece L

A finitely generated polynomial module over a field admits a homogeneous complement to its torsion submodule when X strictly lowers degree. The complement is not canonical; no homogeneous basis is assumed or asserted.