Twists and twisting sheaves on Proj

For the sign convention fixed in Shift, this file defines

• sheafNatTwist 𝓜 d from the exact natural shift;
• sheafTwist 𝓜 d from the zero-extended integer shift; and
• twistingSheaf 𝒜 d, notation-free 𝒪(d), by applying the construction to the graded ring as a module over itself.

The normalization at zero is an actual isomorphism of sheaves of modules. Natural shifts also carry a strict composition comparison. Mixed integer iteration is not asserted at the graded module level because truncating negative degrees makes that statement false; its sheaf-level comparison belongs with the later quasi-coherence/basic-open equivalence.

noncomputable def AlgebraicGeometry.Proj.sheafNatTwist {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 : ℕ) : (Proj 𝒜).Modules

The associated sheaf of the natural shift M(d), for d : ℕ.

Equations

• AlgebraicGeometry.Proj.sheafNatTwist 𝒜 𝓜 d = AlgebraicGeometry.Proj.associatedSheaf 𝒜 (GradedModule.natShift 𝓜 d)

noncomputable def AlgebraicGeometry.Proj.sheafTwist {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 : ℤ) : (Proj 𝒜).Modules

The associated sheaf of the integer shift M(d), with negative degrees zero-extended.

Equations

• AlgebraicGeometry.Proj.sheafTwist 𝒜 𝓜 d = AlgebraicGeometry.Proj.associatedSheaf 𝒜 (GradedModule.intShift 𝓜 d)

noncomputable def AlgebraicGeometry.Proj.sheafTwistZeroIso {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 𝒜 𝓜] : sheafTwist 𝒜 𝓜 0 ≅ associatedSheaf 𝒜 𝓜

The zero integer twist is canonically isomorphic to the original associated sheaf.

Equations

• AlgebraicGeometry.Proj.sheafTwistZeroIso 𝒜 𝓜 = AlgebraicGeometry.Proj.associatedIsoOfPiecewiseIff 𝒜 (GradedModule.intShift 𝓜 0) 𝓜 ⋯

noncomputable def AlgebraicGeometry.Proj.sheafNatTwistZeroIso {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 𝒜 𝓜] : sheafNatTwist 𝒜 𝓜 0 ≅ associatedSheaf 𝒜 𝓜

Natural shift by zero is canonically the original associated sheaf.

Equations

• AlgebraicGeometry.Proj.sheafNatTwistZeroIso 𝒜 𝓜 = AlgebraicGeometry.Proj.associatedIsoOfPiecewiseIff 𝒜 (GradedModule.natShift 𝓜 0) 𝓜 ⋯

noncomputable def AlgebraicGeometry.Proj.sheafNatTwistAddIso {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 : ℕ) : sheafNatTwist 𝒜 (GradedModule.natShift 𝓜 d) e ≅ sheafNatTwist 𝒜 𝓜 (d + e)

Natural shifts compose according to addition of their indices.

Equations

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

noncomputable def AlgebraicGeometry.Proj.twistingSheaf {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (d : ℤ) : (Proj 𝒜).Modules

The twisting sheaf 𝒪(d) on Proj 𝒜, using the convention A(d)ₙ = Aₙ₊d.

Equations

• AlgebraicGeometry.Proj.twistingSheaf 𝒜 d = AlgebraicGeometry.Proj.sheafTwist 𝒜 𝒜 d

noncomputable def AlgebraicGeometry.Proj.twistingSheafZeroIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] : twistingSheaf 𝒜 0 ≅ associatedSheaf 𝒜 𝒜

The normalization 𝒪(0) ≅ Ã; the identification of Ã with the structure sheaf is kept as the next affine/quasi-coherence comparison rather than hidden in this definition.

Equations

• AlgebraicGeometry.Proj.twistingSheafZeroIso 𝒜 = AlgebraicGeometry.Proj.sheafTwistZeroIso 𝒜 𝒜

noncomputable def AlgebraicGeometry.Proj.twistingSheafOfNatIso {A σA : Type u} [CommRing A] [SetLike σA A] [AddSubgroupClass σA A] (𝒜 : ℕ → σA) [GradedRing 𝒜] (d : ℕ) : twistingSheaf 𝒜 ↑d ≅ sheafNatTwist 𝒜 𝒜 d

A nonnegative integer twist agrees with the corresponding strict natural twist.

Equations

• AlgebraicGeometry.Proj.twistingSheafOfNatIso 𝒜 d = AlgebraicGeometry.Proj.associatedIsoOfPiecewiseIff 𝒜 (GradedModule.intShift 𝒜 ↑d) (GradedModule.natShift 𝒜 d) ⋯