Homogeneous cyclic decomposition of graded k[X]-modules

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 completes the structure theorem for such modules: M is the internal direct sum of cyclic submodules k[X] ∙ t generated by homogeneous elements t, each of which is either free (an X-tower) or isomorphic to k[X] ⧸ (X ^ m) for some m ≠ 0. The free summands come from TauCeti.InternalGrading.exists_linearIndependent_isCompl_torsion; the new input is the decomposition of the torsion submodule.

The torsion summands are split off one at a time. Let L be a homogeneous submodule killed by X ^ m, and t ∈ L a homogeneous element of degree p with X ^ (m - 1) • t ≠ 0. Choose a k-linear functional φ that sees only the homogeneous component of degree q = p - (m - 1) * d and takes the value 1 on X ^ (m - 1) • t. Since the elements X ^ l • t lie in the distinct degrees p - l * d, the functional φ vanishes on all of them except X ^ (m - 1) • t. The elements y ∈ L with φ (a • y) = 0 for every polynomial a then form a homogeneous complement of k[X] ∙ t in L. Repeating this inside the complement builds a strictly increasing chain of submodules of M, which stops because M is Noetherian.

Main results

• TauCeti.InternalGrading.exists_disjoint_span_singleton_sup_eq: a cyclic submodule generated by a homogeneous element of maximal order has a homogeneous complement.
• TauCeti.InternalGrading.exists_iSupIndep_iSup_span_singleton_eq_of_le_torsion: a homogeneous torsion submodule is an independent sum of finitely many cyclic submodules k[X] ∙ t with homogeneous t and annihilator (X ^ m), m ≠ 0.
• TauCeti.InternalGrading.exists_isInternal_span_singleton: the structure theorem; M is the internal direct sum of homogeneous free cyclic submodules and finitely many homogeneous cyclic submodules with annihilators (X ^ m), m ≠ 0.

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_disjoint_span_singleton_sup_eq {k : Type u_1} {M : Type u} [Field k] [AddCommGroup 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)) {L : Submodule (Polynomial k) M} (hL : DirectSum.SetLike.IsHomogeneous (G.piece ℤ) L) {m : ℕ} (hLm : ∀ y ∈ L, Polynomial.X ^ m • y = 0) {p : ℤ} {t : M} (htL : t ∈ L) (htp : t ∈ G.piece ℤ p) (ht : Polynomial.X ^ (m - 1) • t ≠ 0) : ∃ (K : Submodule (Polynomial k) M), DirectSum.SetLike.IsHomogeneous (G.piece ℤ) K ∧ Disjoint (Polynomial k ∙ t) K ∧ Polynomial k ∙ t ⊔ K = L

Splitting off a cyclic summand of maximal order. Let X lower degree by d ≠ 0, let L be a homogeneous k[X]-submodule killed by X ^ m, and let t ∈ L be homogeneous with X ^ (m - 1) • t ≠ 0. Then the cyclic submodule k[X] ∙ t has a homogeneous complement in L.

theorem TauCeti.InternalGrading.exists_iSupIndep_iSup_span_singleton_eq_of_le_torsion {k : Type u_1} {M : Type u} [Field k] [AddCommGroup M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] {G : InternalGrading k M ℤ} {d : ℕ} [Module.Finite (Polynomial 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) (hL : DirectSum.SetLike.IsHomogeneous (G.piece ℤ) L) (hLT : L ≤ Submodule.torsion (Polynomial k) M) : ∃ (ι : Type u) (_ : Finite ι) (t : ι → M) (deg : ι → ℤ) (m : ι → ℕ), (∀ (i : ι), t i ∈ G.piece ℤ (deg i)) ∧ (∀ (i : ι), m i ≠ 0) ∧ (∀ (i : ι), Ideal.torsionOf (Polynomial k) M (t i) = Ideal.span {Polynomial.X ^ m i}) ∧ (iSupIndep fun (i : ι) => Polynomial k ∙ t i) ∧ ⨆ (i : ι), Polynomial k ∙ t i = L

The torsion part of the structure theorem. Let X lower degree by d ≠ 0 in a finitely generated graded k[X]-module over a field. Then every homogeneous k[X]-submodule L contained in the torsion submodule is the independent sum of finitely many cyclic submodules k[X] ∙ t i, where each t i is homogeneous with annihilator (X ^ m i) for some m i ≠ 0. Thus each summand is isomorphic to k[X] ⧸ (X ^ m i) (Ideal.quotTorsionOfEquivSpanSingleton).

theorem TauCeti.InternalGrading.exists_isInternal_span_singleton {k : Type u_1} {M : Type u} [Field k] [AddCommGroup M] [Module k M] [Module (Polynomial k) M] [IsScalarTower k (Polynomial k) M] {G : InternalGrading k M ℤ} {d : ℕ} [Module.Finite (Polynomial k) M] (hd : d ≠ 0) (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece ℤ p → Polynomial.X • x ∈ G.piece ℤ (p - ↑d)) : ∃ (ι : Type u) (κ : Type u) (_ : Finite ι) (_ : Finite κ) (t : ι ⊕ κ → M) (deg : ι ⊕ κ → ℤ) (m : κ → ℕ), (∀ (i : ι ⊕ κ), t i ∈ G.piece ℤ (deg i)) ∧ (∀ (i : ι), Ideal.torsionOf (Polynomial k) M (t (Sum.inl i)) = ⊥) ∧ (∀ (j : κ), m j ≠ 0) ∧ (∀ (j : κ), Ideal.torsionOf (Polynomial k) M (t (Sum.inr j)) = Ideal.span {Polynomial.X ^ m j}) ∧ DirectSum.IsInternal fun (i : ι ⊕ κ) => Polynomial k ∙ t i

The structure theorem for finitely generated graded k[X]-modules. Let X lower degree by d ≠ 0 in a finitely generated graded k[X]-module M over a field. Then M is the internal direct sum of cyclic submodules k[X] ∙ t i generated by homogeneous elements t i, indexed by the disjoint union of two finite types: for i in the first, t i has zero annihilator, so k[X] ∙ t i is a free X-tower; for j in the second, t j has annihilator (X ^ m j) with m j ≠ 0, so k[X] ∙ t j ≅ k[X] ⧸ (X ^ m j).