Homogeneous bases of the free part of a graded k[X]-module

Let k be a field and M a finitely generated k[X]-module with an internal ℤ-grading on which X lowers degree by a fixed nonzero d. This file shows that the free part of M is graded free: every homogeneous k[X]-submodule meeting the torsion submodule trivially has a k[X]-basis of homogeneous elements. Together with the homogeneous complement to torsion of TauCeti.Algebra.Module.GradedModule.Torsion, this gives the "tower" half of the structure theorem for finitely generated graded k[X]-modules: M is the direct sum of its torsion submodule and a free module on homogeneous generators, one X-tower per generator. The decomposition of the torsion submodule into homogeneous cyclic summands, which completes the structure theorem, is in TauCeti.Algebra.Module.GradedModule.CyclicDecomposition.

The basis is assembled degree by degree. In degree p, the degree-p part of the submodule contains X times its degree-(p + d) part, and a k-basis of a complement is chosen. Since degrees are bounded above, a form of graded Nakayama shows that these elements span. Since X is a nonzerodivisor on the submodule, a relation among them could be divided by X indefinitely, so they are linearly independent.

Main results

• TauCeti.InternalGrading.exists_linearIndependent_span_eq_of_disjoint_torsion: a homogeneous submodule meeting torsion trivially is spanned by a linearly independent homogeneous family.
• TauCeti.InternalGrading.exists_homogeneous_basis: a torsion-free module has a homogeneous basis.
• TauCeti.InternalGrading.exists_linearIndependent_isCompl_torsion: the torsion submodule has a complement with a homogeneous basis.

References

• P. Ozsváth, A. Stipsicz, Z. Szabó, Grid Homology for Knots and Links, AMS Mathematical Surveys and Monographs 208, 2015, Appendix A: the structure of finitely generated graded modules over 𝔽[U].

theorem TauCeti.InternalGrading.exists_linearIndependent_span_eq_of_disjoint_torsion {k : Type u_1} {M : Type u} [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)) (L : Submodule (Polynomial k) M) (hL : DirectSum.SetLike.IsHomogeneous (G.piece ℤ) L) (hLT : Disjoint L (Submodule.torsion (Polynomial k) M)) : ∃ (ι : Type u) (b : ι → M) (deg : ι → ℤ), (∀ (i : ι), b i ∈ G.piece ℤ (deg i)) ∧ LinearIndependent (Polynomial k) b ∧ Submodule.span (Polynomial k) (Set.range b) = L

Homogeneous bases of the free part. Let X lower degree by d ≠ 0 in a finitely generated graded k[X]-module over a field. Then a homogeneous k[X]-submodule L meeting the torsion submodule trivially is the span of a k[X]-linearly independent family of homogeneous elements. That is, L is graded free.

theorem TauCeti.InternalGrading.exists_homogeneous_basis {k : Type u_1} {M : Type u} [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 : ℕ} [Module.IsTorsionFree (Polynomial k) M] (hd : d ≠ 0) (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece ℤ p → Polynomial.X • x ∈ G.piece ℤ (p - ↑d)) : ∃ (ι : Type u) (b : Module.Basis ι (Polynomial k) M) (deg : ι → ℤ), ∀ (i : ι), b i ∈ G.piece ℤ (deg i)

Graded freeness. A finitely generated graded k[X]-module over a field that is torsion-free over k[X], and on which X lowers degree by d ≠ 0, has a k[X]-basis of homogeneous elements.

theorem TauCeti.InternalGrading.exists_linearIndependent_isCompl_torsion {k : Type u_1} {M : Type u} [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)) : ∃ (ι : Type u) (b : ι → M) (deg : ι → ℤ), (∀ (i : ι), b i ∈ G.piece ℤ (deg i)) ∧ LinearIndependent (Polynomial k) b ∧ IsCompl (Submodule.torsion (Polynomial k) M) (Submodule.span (Polynomial k) (Set.range b))

The free part of the structure theorem. In a finitely generated graded k[X]-module over a field on which X lowers degree by d ≠ 0, the torsion submodule has a complement spanned by a k[X]-linearly independent family of homogeneous elements: M is its torsion submodule plus a graded free module, one X-tower for each element of the family.