Maximal non-torsion degree of a graded k[X]-module

Let M be a ℤ-graded module over a polynomial ring k[X] in which X lowers degree by a fixed d. The degrees of the homogeneous elements of M that are not torsion form a set G.nonTorsionDegrees. Its supremum G.supNonTorsionDegree is attained, and hence is its maximal non-torsion degree, when M is finitely generated and not torsion (for instance, it is s for M the tower k[X] shifted so that 1 sits in degree s, direct sum a torsion module). This is the algebraic invariant through which the concordance invariant τ of a knot is defined: τ(K) is minus the maximal Alexander grading of a homogeneous non-torsion element of the unblocked grid homology GH⁻(K), a finitely generated graded module over 𝔽[U] on which U lowers the Alexander grading by one.

The file shows that the invariant is well behaved without appeal to the structure theorem for graded k[X]-modules:

• when the coefficients k form a domain over which M is torsion-free and X lowers degree by a nonzero d, a homogeneous element is torsion exactly when a power of X kills it (InternalGrading.mem_torsion_iff_exists_X_pow_smul_eq_zero), because the terms c • X ^ n • x of a • x lie in pairwise distinct degrees; so G.nonTorsionDegrees are the degrees of the homogeneous elements no power of X kills (InternalGrading.mem_nonTorsionDegrees_iff_forall_X_pow_smul_ne_zero);
• in a finitely generated graded k[X]-module on which X lowers degree, the non-torsion degrees are bounded above (InternalGrading.bddAbove_nonTorsionDegrees), so the supremum is attained as soon as M is not torsion (InternalGrading.isGreatest_supNonTorsionDegree);
• a homogeneous map of degree δ that reflects torsion raises the invariant by at least δ, as long as the source has a homogeneous non-torsion element and the non-torsion degrees of the target are bounded above (InternalGrading.supNonTorsionDegree_add_le). This applies in particular when the map has a left inverse up to multiplication by a nonzerodivisor such as a power of X (TauCeti.Submodule.comap_torsion_le_of_comp_eq_smul), the shape of the bounds on τ coming from crossing changes and cobordisms; a graded isomorphism preserves the invariant (InternalGrading.supNonTorsionDegree_eq_of_linearEquiv).

Finally, the polynomial ring itself, graded by minus the exponent, has the invariant 0 (Polynomial.supNonTorsionDegree_negDegreeGrading).

Main definitions

• TauCeti.InternalGrading.nonTorsionDegrees: the degrees of homogeneous non-torsion elements.
• TauCeti.InternalGrading.supNonTorsionDegree: their supremum.

References

• P. Ozsváth, A. Stipsicz, Z. Szabó, Grid Homology for Knots and Links, AMS Mathematical Surveys and Monographs 208, 2015, Chapter 6: the definition of τ as minus the maximal Alexander grading of a homogeneous non-torsion element of GH⁻, and the crossing-change maps whose composites are multiplication by U, from which the unknotting-number bound on τ follows.

def TauCeti.InternalGrading.nonTorsionDegrees {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] (G : InternalGrading k M) : Set ℤ

The degrees in which a graded k[X]-module has a homogeneous element that is not torsion.

Equations

• G.nonTorsionDegrees = {p : ℤ | ∃ x ∈ G.piece p, x ∉ Submodule.torsion (Polynomial k) M}

noncomputable def TauCeti.InternalGrading.supNonTorsionDegree {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] (G : InternalGrading k M) : ℤ

The supremum of the degrees in which a graded k[X]-module has a homogeneous non-torsion element. When that set is nonempty and bounded above, this is its maximal element; those conditions hold for a finitely generated module that is not torsion and on which X lowers degree (InternalGrading.isGreatest_supNonTorsionDegree).

Equations

• G.supNonTorsionDegree = sSup G.nonTorsionDegrees

theorem TauCeti.InternalGrading.supNonTorsionDegree_def {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] (G : InternalGrading k M) : G.supNonTorsionDegree = sSup G.nonTorsionDegrees

The supremal non-torsion degree is the supremum of the degrees of homogeneous non-torsion elements.

@[simp]

theorem TauCeti.InternalGrading.mem_nonTorsionDegrees {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] {G : InternalGrading k M} {p : ℤ} : p ∈ G.nonTorsionDegrees ↔ ∃ x ∈ G.piece p, x ∉ Submodule.torsion (Polynomial k) M

Membership in G.nonTorsionDegrees.

@[simp]

theorem TauCeti.InternalGrading.nonTorsionDegrees_shift {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] (G : InternalGrading k M) (c : ℤ) : (G.shift c).nonTorsionDegrees = ⇑(OrderIso.addRight (-c)) '' G.nonTorsionDegrees

Shifting a grading by c subtracts c from every non-torsion degree.

@[simp]

theorem TauCeti.InternalGrading.supNonTorsionDegree_shift {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] (G : InternalGrading k M) (c : ℤ) (hne : G.nonTorsionDegrees.Nonempty) (hbdd : BddAbove G.nonTorsionDegrees) : (G.shift c).supNonTorsionDegree = G.supNonTorsionDegree - c

The supremal non-torsion degree decreases by c when the grading is shifted by c.

@[simp]

theorem TauCeti.InternalGrading.nonTorsionDegrees_nonempty_iff {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] (G : InternalGrading k M) : G.nonTorsionDegrees.Nonempty ↔ ¬Module.IsTorsion (Polynomial k) M

A graded k[X]-module has a homogeneous non-torsion element exactly when it is not torsion: if every homogeneous component of x is torsion, then so is their sum x.

theorem TauCeti.InternalGrading.bddAbove_nonTorsionDegrees {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 G.nonTorsionDegrees

In a finitely generated graded k[X]-module on which X lowers degree, the degrees of the homogeneous non-torsion elements are bounded above.

theorem TauCeti.InternalGrading.isGreatest_supNonTorsionDegree {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] {G : InternalGrading k M} (hne : G.nonTorsionDegrees.Nonempty) (hbdd : BddAbove G.nonTorsionDegrees) : IsGreatest G.nonTorsionDegrees G.supNonTorsionDegree

The supremal non-torsion degree is the greatest non-torsion degree when the set of such degrees is nonempty and bounded above.

theorem TauCeti.InternalGrading.le_supNonTorsionDegree {k : Type u_1} {M : Type u_2} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] {G : InternalGrading k M} (hbdd : BddAbove G.nonTorsionDegrees) {p : ℤ} (hp : p ∈ G.nonTorsionDegrees) : p ≤ G.supNonTorsionDegree

Every degree of a homogeneous non-torsion element is at most the maximal non-torsion degree.

theorem TauCeti.InternalGrading.add_mem_nonTorsionDegrees {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] [AddCommMonoid N] [Module k N] [Module (Polynomial k) N] {G : InternalGrading k M} {H : InternalGrading k N} {f : M →ₗ[Polynomial k] N} {δ : ℤ} (hf : LinearMap.IsHomogeneous f G.piece H.piece δ) (hft : Submodule.comap f (Submodule.torsion (Polynomial k) N) ≤ Submodule.torsion (Polynomial k) M) {p : ℤ} (hp : p ∈ G.nonTorsionDegrees) : p + δ ∈ H.nonTorsionDegrees

A homogeneous map of degree δ that reflects torsion carries a homogeneous non-torsion element of degree p to one of degree p + δ.

theorem TauCeti.InternalGrading.supNonTorsionDegree_add_le {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] [AddCommMonoid N] [Module k N] [Module (Polynomial k) N] {G : InternalGrading k M} {H : InternalGrading k N} (hne : G.nonTorsionDegrees.Nonempty) (hbdd : BddAbove H.nonTorsionDegrees) {f : M →ₗ[Polynomial k] N} {δ : ℤ} (hf : LinearMap.IsHomogeneous f G.piece H.piece δ) (hft : Submodule.comap f (Submodule.torsion (Polynomial k) N) ≤ Submodule.torsion (Polynomial k) M) : G.supNonTorsionDegree + δ ≤ H.supNonTorsionDegree

A homogeneous map of degree δ that reflects torsion raises the maximal non-torsion degree by at least δ, provided the source has a homogeneous non-torsion element and the non-torsion degrees of the target are bounded above (for instance by bddAbove_nonTorsionDegrees when the target is finitely generated and X lowers degree on it). By Submodule.comap_torsion_le_of_comp_eq_smul, torsion is reflected as soon as the map has a left inverse up to multiplication by a power of X.

theorem TauCeti.InternalGrading.nonTorsionDegrees_eq_of_linearEquiv {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] [AddCommMonoid N] [Module k N] [Module (Polynomial k) N] {G : InternalGrading k M} {H : InternalGrading k N} (e : M ≃ₗ[Polynomial k] N) (he : LinearMap.IsHomogeneous (↑e) G.piece H.piece 0) : G.nonTorsionDegrees = H.nonTorsionDegrees

A graded isomorphism of graded k[X]-modules identifies their non-torsion-degree sets.

theorem TauCeti.InternalGrading.supNonTorsionDegree_eq_of_linearEquiv {k : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring k] [AddCommMonoid M] [Module k M] [Module (Polynomial k) M] [AddCommMonoid N] [Module k N] [Module (Polynomial k) N] {G : InternalGrading k M} {H : InternalGrading k N} (e : M ≃ₗ[Polynomial k] N) (he : LinearMap.IsHomogeneous (↑e) G.piece H.piece 0) : G.supNonTorsionDegree = H.supNonTorsionDegree

A graded isomorphism of graded k[X]-modules preserves the supremal non-torsion degree.

theorem TauCeti.InternalGrading.mem_torsion_iff_exists_X_pow_smul_eq_zero {k : Type u_1} {M : Type u_2} [CommSemiring k] [IsDomain k] [AddCommMonoid 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)) {p : ℤ} {x : M} (hx : x ∈ G.piece p) : x ∈ Submodule.torsion (Polynomial k) M ↔ ∃ (n : ℕ), Polynomial.X ^ n • x = 0

When the coefficients k form a domain over which M is torsion-free, a homogeneous element of a graded k[X]-module on which X lowers degree by a nonzero d is torsion exactly when some power of X kills it.

theorem TauCeti.InternalGrading.mem_nonTorsionDegrees_iff_forall_X_pow_smul_ne_zero {k : Type u_1} {M : Type u_2} [CommSemiring k] [IsDomain k] [AddCommMonoid 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)) {p : ℤ} : p ∈ G.nonTorsionDegrees ↔ ∃ x ∈ G.piece p, ∀ (n : ℕ), Polynomial.X ^ n • x ≠ 0

When the coefficients k form a domain over which M is torsion-free, the degrees of the homogeneous non-torsion elements are the degrees of the homogeneous elements that no power of X kills.

@[simp]

theorem TauCeti.Polynomial.nonTorsionDegrees_negDegreeGrading {k : Type u_1} [CommSemiring k] [Nontrivial k] : (negDegreeGrading k).nonTorsionDegrees = Set.Iic 0

The degrees of the homogeneous non-torsion elements of k[X], graded by negDegreeGrading, are the nonpositive integers: every nonzero homogeneous element is a nonzero multiple of a monomial X ^ n, of degree -n.

@[simp]

theorem TauCeti.Polynomial.supNonTorsionDegree_negDegreeGrading {k : Type u_1} [CommSemiring k] [Nontrivial k] : (negDegreeGrading k).supNonTorsionDegree = 0

The top of the tower k[X], graded by negDegreeGrading, sits in degree 0.