Shifts of naturally graded modules

An ℕ-graded ring can support module twists conventionally indexed by ℤ. This file keeps that boundary visible without assuming a geometric realization.

• natShift 𝓜 d has degree-n piece 𝓜 (n + d) and composes strictly.
• intShift 𝓜 d uses the same formula with n + d : ℤ, extending 𝓜 by the zero subgroup in negative degrees. It is a one-step shift of the original natural grading. Iterated mixed integer shifts are deliberately not identified at the graded-module level: truncation at degree zero makes that false before passing to associated sheaves.

Our sign convention is therefore M(d)ₙ = Mₙ₊d.

Natural shifts

def GradedModule.natShift {σM : Type u} (𝓜 : ℕ → σM) (d : ℕ) : ℕ → σM

The natural shift with convention M(d)ₙ = Mₙ₊d.

Equations

• GradedModule.natShift 𝓜 d n = 𝓜 (n + d)

instance GradedModule.natShiftGradedSMul {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [SetLike σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (d : ℕ) : SetLike.GradedSMul 𝒜 (natShift 𝓜 d)

@[simp]

theorem GradedModule.natShift_apply {σM : Type u} (𝓜 : ℕ → σM) (d n : ℕ) : natShift 𝓜 d n = 𝓜 (n + d)

@[simp]

theorem GradedModule.natShift_zero {σM : Type u} (𝓜 : ℕ → σM) : natShift 𝓜 0 = 𝓜

@[simp]

theorem GradedModule.natShift_add {σM : Type u} (𝓜 : ℕ → σM) (d e : ℕ) : natShift (natShift 𝓜 d) e = natShift 𝓜 (d + e)

Integer shifts by zero extension

def GradedModule.intShiftPiece {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d : ℤ) (n : ℕ) : AddSubgroup M

The degree-n subgroup of the integer shift. A nonzero element belongs precisely when it lies in a natural graded piece whose integer degree equals n + d; zero is retained when that integer is negative.

Equations

• GradedModule.intShiftPiece 𝓜 d n = { carrier := {m : M | m = 0 ∨ ∃ (k : ℕ), ↑k = ↑n + d ∧ m ∈ 𝓜 k}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def GradedModule.intShift {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d : ℤ) : ℕ → AddSubgroup M

The integer shift of a naturally graded module, using zero in negative degrees.

Equations

• GradedModule.intShift 𝓜 d n = GradedModule.intShiftPiece 𝓜 d n

@[simp]

theorem GradedModule.mem_intShiftPiece {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) {d : ℤ} {n : ℕ} {m : M} : m ∈ intShiftPiece 𝓜 d n ↔ m = 0 ∨ ∃ (k : ℕ), ↑k = ↑n + d ∧ m ∈ 𝓜 k

theorem GradedModule.intShiftPiece_eq_bot_of_neg {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d : ℤ) (n : ℕ) (hn : ↑n + d < 0) : intShiftPiece 𝓜 d n = ⊥

A shifted graded piece below degree zero is trivial.

intShift is ℕ-indexed and intShiftPiece 𝓜 d n asks for an element of degree n + d. When that integer is negative, no natural degree witnesses membership, so only zero remains.

instance GradedModule.intShiftGradedSMul {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (d : ℤ) : SetLike.GradedSMul 𝒜 (intShift 𝓜 d)

@[simp]

theorem GradedModule.intShift_apply {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d : ℤ) (n : ℕ) : intShift 𝓜 d n = intShiftPiece 𝓜 d n

theorem GradedModule.mem_intShift_zero_iff {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (n : ℕ) (m : M) : m ∈ intShift 𝓜 0 n ↔ m ∈ 𝓜 n

At shift zero the integer-shifted pieces are the original pieces, expressed as an equality of their carriers.

theorem GradedModule.mem_intShift_ofNat_iff {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d n : ℕ) (m : M) : m ∈ intShift 𝓜 (↑d) n ↔ m ∈ natShift 𝓜 d n

A nonnegative integer shift agrees with the corresponding natural shift, at the level of membership in each graded piece.

theorem GradedModule.mem_natShift_add_iff {M σM : Type u} [SetLike σM M] (𝓜 : ℕ → σM) (d e n : ℕ) (m : M) : m ∈ natShift (natShift 𝓜 d) e n ↔ m ∈ natShift 𝓜 (d + e) n

Strict composition for nonnegative shifts, phrased as membership so it applies uniformly even when the subobject types differ.

theorem GradedModule.mem_intShift_add_iff_of_nonneg {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d e : ℤ) (n : ℕ) (hne : 0 ≤ ↑n + e) (m : M) : m ∈ intShift (intShift 𝓜 d) e n ↔ m ∈ intShift 𝓜 (d + e) n

Integer shifts compose only where the intermediate degree exists, and hne is exactly that condition.

The unrestricted statement — intShift (intShift 𝓜 d) e = intShift 𝓜 (d + e) — is false, and the hypothesis here is where it fails rather than a convenience. Shifting by a negative e first asks for a graded piece in degree n + e; when that integer is negative the zero extension supplies 0 and the information is gone, while the single shift by d + e may still land in a genuine piece. Concretely, with d = 10, e = -5 and n = 0, the left side is {0} because no natural number has integer value -5, and the right side is 𝓜 5.

This is a fact about the algebraic model, not about the sheaf. associatedSheaf only ever reads these pieces through homogeneous localizations, where the missing degrees are inverted back in, so the sheaf-level composition O(d)(e) ≅ O(d + e) is not obstructed by this — but it cannot be obtained by transporting an algebraic identity, and has to be proved on the sheaf side. Recorded here because that is the trap this lemma exists to mark.

theorem GradedModule.eq_zero_of_mem_intShift_intShift_of_neg {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d e : ℤ) (n : ℕ) (hne : ↑n + e < 0) {m : M} (hm : m ∈ intShift (intShift 𝓜 d) e n) : m = 0

Below the intermediate degree the double shift is zero. This is the failure mem_intShift_add_iff_of_nonneg's hypothesis avoids, as a theorem rather than a remark: an inner shift by e asks for degree n + e, and no natural number has a negative integer value, so nothing but zero survives.

Together with membership in the single shift — for instance any nonzero element of 𝓜 (n + d + e) when that degree is a natural number — this exhibits the two sides as different subgroups, which is why no unrestricted composition lemma appears above.

theorem GradedModule.smul_mem_intShift {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (d : ℤ) (i j : ℕ) {a : A} {m : M} (ha : a ∈ intShift 𝒜 d i) (hm : m ∈ 𝓜 j) : a • m ∈ intShift 𝓜 d (i + j)

Degree bookkeeping for the twisted multiplication.

A ring element of the degree-d shift scales a module element of degree j into the degree-d shift of the module. This is what makes A(d) ⊗ M → M(d) land where it should, and it is the SetLike.GradedSMul analogue of the fact that 𝒜 i · 𝓜 j ⊆ 𝓜 (i + j).

The composition, at the localization

mem_intShift_add_iff_of_nonneg and eq_zero_of_mem_intShift_intShift_of_neg together say the double shift and the single shift are genuinely different graded submodule families, and record that the sheaf-level composition O(d)(e) ≅ O(d + e) therefore cannot be transported from an algebraic identity. This section supplies the algebraic half of the replacement: at a localization whose denominators contain a homogeneous element of positive degree, the two families have the same degree-zero part, because the degrees the double shift truncates are inverted back in.

That is exactly the reading Shift's note above predicted. What remains for the sheaf statement is to carry this from one localization to the sections of the associated sheaf, and it is not here.

theorem GradedModule.mem_intShift_add_of_mem_intShift_intShift {M σM : Type u} [AddCommGroup M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) (d e : ℤ) (n : ℕ) {m : M} (hm : m ∈ intShift (intShift 𝓜 d) e n) : m ∈ intShift 𝓜 (d + e) n

The double shift always lands in the single shift.

Only the converse needs the degree bound of mem_intShift_add_iff_of_nonneg; this direction is unconditional, so it is the one that gives a graded map without hypotheses.

theorem GradedModule.isDegreeZero_intShift_intShift_iff {A M σA σM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike σA A] [AddSubgroupClass σA A] [SetLike σM M] [AddSubgroupClass σM M] (𝒜 : ℕ → σA) (𝓜 : ℕ → σM) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (S : Submonoid A) {m : ℕ} (hm : 0 < m) {t : A} (ht : t ∈ 𝒜 m) (htS : t ∈ S) (d e : ℤ) (z : LocalizedModule S M) : IsDegreeZero 𝒜 (intShift (intShift 𝓜 d) e) S z ↔ IsDegreeZero 𝒜 (intShift 𝓜 (d + e)) S z

The double shift and the single shift have the same degree-zero localization, once the denominators contain a homogeneous element t of positive degree.

One direction is mem_intShift_add_of_mem_intShift_intShift applied to the numerator; the other is where the content is. A fraction certified only for intShift 𝓜 (d + e) is rewritten by multiplying numerator and denominator by a power of t, which raises its degree without changing the element, until the degree clears the bound mem_intShift_add_iff_of_nonneg asks for. This is the precise sense in which the truncated degrees are "inverted back in": they are never needed at a degree the localization cannot reach.