The twists compose, on the sheaf side

Shift.lean proves that the graded identity M(d)(e) = M(d + e) is false. intShift zero-extends, so with d = 10, e = -5 and n = 0 the double shift is {0} while the single shift is 𝓜 5; eq_zero_of_mem_intShift_intShift_of_neg is a theorem written for no purpose other than to record that. Its note also says what to do about it:

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.

This file is that proof, and sheafTwistAddIso is the integer analogue of sheafNatTwistAddIso that TwistingSheaf.lean declined to assert for exactly this reason.

The shape of the argument

The comparison is pointwise the identity. Fiber is DegreeZeroLocalization, which is a submodule of LocalizedModule S M, and that ambient does not mention the grading at all — so the two twists are subobjects of one object and degreeZeroSubmodule_intShift_intShift says their carriers coincide. Nothing is transported; only the certificate changes.

What is left is the local-fraction condition, and the two directions are not symmetric:

• forward, nothing moves. The numerator's certificate is rebuilt through mem_intShift_add_of_mem_intShift_intShift, whose hypothesis-free existence is the useful half of mem_intShift_add_iff_of_nonneg;
• backward is where the content is. A fraction certified only for the single shift is rewritten as τ^k · r / τ^k · t, which raises its degree without changing the element until the double shift can certify it, and the neighbourhood shrinks to V ⊓ D₊(τ) so that one τ serves every point of it. The pointwise statement would not suffice: isLocallyFraction demands a single fraction on a whole neighbourhood, and a per-point choice of τ would not give one.

exists_homogeneous_pos_not_mem supplies the τ, and is where the geometry enters: a point of Proj is exactly a relevant prime, so it misses a homogeneous element of positive degree.

Scope

The composition only. Relating it to the tensor product — F ⊗ O(d) ≅ F(d), and hence O(d) ⊗ O(e) ≅ O(d + e) — is a separate comparison and is not here.

theorem AlgebraicGeometry.Proj.exists_homogeneous_pos_not_mem {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (x : ProjectiveSpectrum 𝒜) : ∃ (m : ℕ) (t : A), 0 < m ∧ t ∈ 𝒜 m ∧ t ∉ x.asHomogeneousIdeal

Every point of Proj misses a homogeneous element of positive degree.

theorem AlgebraicGeometry.Proj.mem_primeCompl_of_not_mem {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] {x : ProjectiveSpectrum 𝒜} {t : A} (ht : t ∉ x.asHomogeneousIdeal) : t ∈ x.asHomogeneousIdeal.toIdeal.primeCompl

The point misses t, phrased for the localization's denominators.

theorem AlgebraicGeometry.Proj.degreeZeroSubmodule_intShift_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) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝓜] (x : ProjectiveSpectrum 𝒜) (d e : ℤ) : GradedModule.degreeZeroSubmodule 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e) x.asHomogeneousIdeal.toIdeal.primeCompl = GradedModule.degreeZeroSubmodule 𝒜 (GradedModule.intShift 𝓜 (d + e)) x.asHomogeneousIdeal.toIdeal.primeCompl

The two shifts have the same fiber at every point of Proj.

noncomputable def AlgebraicGeometry.Proj.fiberIntShiftAddEquiv {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 𝒜 𝓜] (x : ProjectiveSpectrum 𝒜) (d e : ℤ) : ↥(Fiber 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e) x) ≃ₗ[HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl] ↥(Fiber 𝒜 (GradedModule.intShift 𝓜 (d + e)) x)

The fiber comparison, as a linear equivalence. It is the identity on carriers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Proj.fiberIntShiftAddEquiv_coe {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 𝒜 𝓜] (x : ProjectiveSpectrum 𝒜) (d e : ℤ) (z : ↥(Fiber 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e) x)) : ↑((fiberIntShiftAddEquiv 𝒜 𝓜 x d e) z) = ↑z

theorem AlgebraicGeometry.Proj.pred_intShift_intShift_of_pred {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 𝒜 𝓜] (d e : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (g : (x : ↥U) → ↥(Fiber 𝒜 (GradedModule.intShift 𝓜 (d + e)) ↑x)) (hg : (isLocallyFraction 𝒜 (GradedModule.intShift 𝓜 (d + e))).pred g) : (isLocallyFraction 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e)).pred fun (x : ↥U) => (fiberIntShiftAddEquiv 𝒜 𝓜 (↑x) d e).symm (g x)

Backward transfer of the local-fraction condition.

The fraction certified for the single shift is rewritten with a power of τ in numerator and denominator, which raises its degree until the double shift can certify it. The neighbourhood shrinks to V ⊓ D₊(τ) so that one τ serves every point of it.

theorem AlgebraicGeometry.Proj.pred_intShift_add_of_pred {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 𝒜 𝓜] (d e : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (f : (x : ↥U) → ↥(Fiber 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e) ↑x)) (hf : (isLocallyFraction 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e)).pred f) : (isLocallyFraction 𝒜 (GradedModule.intShift 𝓜 (d + e))).pred fun (x : ↥U) => (fiberIntShiftAddEquiv 𝒜 𝓜 (↑x) d e) (f x)

Forward transfer of the local-fraction condition.

Nothing moves: the fraction is the same, and only the numerator's membership certificate is rebuilt, through the unconditional inclusion.

noncomputable def AlgebraicGeometry.Proj.sectionAddEquivIntShiftAdd {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 𝒜 𝓜] (d e : ℤ) (U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)) : (associatedSheafInType 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e)).obj.obj (Opposite.op U) ≃+ (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 (d + e))).obj.obj (Opposite.op U)

The two twists have the same sections over every open.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.sectionLinearEquivIntShiftAdd {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 𝒜 𝓜] (d e : ℤ) (U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)) : (associatedSheafInType 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e)).obj.obj (Opposite.op U) ≃ₗ[↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U))] (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 (d + e))).obj.obj (Opposite.op U)

The section comparison is linear over the structure-sheaf sections.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.associatedSheafIntShiftAddIso {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 𝒜 𝓜] (d e : ℤ) : associatedSheaf 𝒜 (GradedModule.intShift (GradedModule.intShift 𝓜 d) e) ≅ associatedSheaf 𝒜 (GradedModule.intShift 𝓜 (d + e))

O(d)(e) ≅ O(d + e), on the sheaf side.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.sheafTwistAddIso {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 𝒜 𝓜] (d e : ℤ) : sheafTwist 𝒜 (GradedModule.intShift 𝓜 d) e ≅ sheafTwist 𝒜 𝓜 (d + e)

The integer twists compose.

The statement TwistingSheaf.lean records as belonging "with the later quasi-coherence/basic-open equivalence", and the integer analogue of sheafNatTwistAddIso. Definitionally this is associatedSheafIntShiftAddIso; it is restated in twist language because that is how callers meet it.

Equations

• AlgebraicGeometry.Proj.sheafTwistAddIso 𝒜 𝓜 d e = AlgebraicGeometry.Proj.associatedSheafIntShiftAddIso 𝒜 𝓜 d e

noncomputable def AlgebraicGeometry.Proj.twistingSheafAddIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] [SetLike.GradedSMul 𝒜 𝒜] (d e : ℤ) : sheafTwist 𝒜 (GradedModule.intShift 𝒜 d) e ≅ twistingSheaf 𝒜 (d + e)

O(d)(e) ≅ O(d + e).

The headline instance of sheafTwistAddIso, at the graded ring as a module over itself.

Equations

• AlgebraicGeometry.Proj.twistingSheafAddIso 𝒜 d e = AlgebraicGeometry.Proj.sheafTwistAddIso 𝒜 𝒜 d e