Nonnegative twists on degree-one Proj charts

Multiplication and division by a degree-one homogeneous element f identify A(d) with A over D₊(f). This file lifts the localization equivalence to the locally fractional sheaves and then identifies the canonical map

(A(d)₍f₎)₀ ⟶ Γ(D₊(f), A(d)̃)

as an equivalence. Thus the degree-one charts used by polynomial projective space no longer require a BasicOpenSectionData certificate.

noncomputable def AlgebraicGeometry.Proj.natShiftFiberLinearEquivOfMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {x : ProjectiveSpectrum 𝒜} (hx : x ∈ ProjectiveSpectrum.basicOpen 𝒜 f) : ↥(Fiber 𝒜 (GradedModule.natShift 𝒜 d) x) ≃ₗ[HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl] ↥(Fiber 𝒜 𝒜 x)

The pointwise trivialization of A(d) at a point lying in D₊(f).

The membership proof is taken directly rather than through a bundled element of the chart, so that one equivalence serves every open contained in D₊(f).

Equations

• AlgebraicGeometry.Proj.natShiftFiberLinearEquivOfMem 𝒜 hf d hx = GradedModule.DegreeZeroLocalization.natShiftLinearEquivOfMem 𝒜 hf d hx

noncomputable def AlgebraicGeometry.Proj.natShiftFiberLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) (x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)) : ↥(Fiber 𝒜 (GradedModule.natShift 𝒜 d) ↑x) ≃ₗ[HomogeneousLocalization 𝒜 (↑x).asHomogeneousIdeal.toIdeal.primeCompl] ↥(Fiber 𝒜 𝒜 ↑x)

The pointwise trivialization of A(d) at a point of D₊(f).

Equations

• AlgebraicGeometry.Proj.natShiftFiberLinearEquiv 𝒜 hf d x = AlgebraicGeometry.Proj.natShiftFiberLinearEquivOfMem 𝒜 hf d ⋯

Integer twists, pointwise

The trivialization of an integer twist is the same construction, with the sign of d decided once inside DegreeZeroLocalization.intShiftZeroLinearEquiv. It lands at A(0) rather than at A; the identification of A(0) with A is the separate zero-normalization already available as sheafTwistZeroIso at the sheaf level.

noncomputable def AlgebraicGeometry.Proj.intShiftFiberLinearEquivOfMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {x : ProjectiveSpectrum 𝒜} (hx : x ∈ ProjectiveSpectrum.basicOpen 𝒜 f) : ↥(Fiber 𝒜 (GradedModule.intShift 𝒜 d) x) ≃ₗ[HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl] ↥(Fiber 𝒜 (GradedModule.intShift 𝒜 0) x)

The pointwise trivialization of A(d) at a point lying in D₊(f), for an integer twist.

Equations

• AlgebraicGeometry.Proj.intShiftFiberLinearEquivOfMem 𝒜 hf d hx = GradedModule.DegreeZeroLocalization.intShiftZeroLinearEquiv 𝒜 hf d hx

noncomputable def AlgebraicGeometry.Proj.intShiftFiberLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) (x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)) : ↥(Fiber 𝒜 (GradedModule.intShift 𝒜 d) ↑x) ≃ₗ[HomogeneousLocalization 𝒜 (↑x).asHomogeneousIdeal.toIdeal.primeCompl] ↥(Fiber 𝒜 (GradedModule.intShift 𝒜 0) ↑x)

The pointwise trivialization of A(d) at a point of D₊(f), for an integer twist.

Equations

• AlgebraicGeometry.Proj.intShiftFiberLinearEquiv 𝒜 hf d x = AlgebraicGeometry.Proj.intShiftFiberLinearEquivOfMem 𝒜 hf d ⋯

Integer twists, on sections

The same construction as the nonnegative case, pointwise, with the certificate rebuilt by the single computation rules intShiftZeroLinearEquiv_apply_mk and its symm sibling. Because those rules are uniform in the sign of d, nothing here splits on it.

noncomputable def AlgebraicGeometry.Proj.intShiftSectionToZeroOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 d)).obj.obj (Opposite.op U)) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 0)).obj.obj (Opposite.op U)

Trivialize a locally fractional section of A(d)̃, over any open contained in D₊(f).

Equations

• AlgebraicGeometry.Proj.intShiftSectionToZeroOn 𝒜 hf d hU s = ⟨fun (x : ↥(Opposite.unop (Opposite.op U))) => (AlgebraicGeometry.Proj.intShiftFiberLinearEquivOfMem 𝒜 hf d ⋯) (↑s x), ⋯⟩

noncomputable def AlgebraicGeometry.Proj.intShiftSectionFromZeroOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 0)).obj.obj (Opposite.op U)) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 d)).obj.obj (Opposite.op U)

The inverse trivialization on sections, over any open contained in D₊(f).

Equations

• AlgebraicGeometry.Proj.intShiftSectionFromZeroOn 𝒜 hf d hU s = ⟨fun (x : ↥(Opposite.unop (Opposite.op U))) => (AlgebraicGeometry.Proj.intShiftFiberLinearEquivOfMem 𝒜 hf d ⋯).symm (↑s x), ⋯⟩

@[simp]

theorem AlgebraicGeometry.Proj.intShiftSectionToZeroOn_apply {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 d)).obj.obj (Opposite.op U)) (x : ↥U) : ↑(intShiftSectionToZeroOn 𝒜 hf d hU s) x = (intShiftFiberLinearEquivOfMem 𝒜 hf d ⋯) (↑s x)

@[simp]

theorem AlgebraicGeometry.Proj.intShiftSectionFromZeroOn_apply {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 0)).obj.obj (Opposite.op U)) (x : ↥U) : ↑(intShiftSectionFromZeroOn 𝒜 hf d hU s) x = (intShiftFiberLinearEquivOfMem 𝒜 hf d ⋯).symm (↑s x)

theorem AlgebraicGeometry.Proj.intShiftFiberLinearEquivOfMem_symm_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {x : ProjectiveSpectrum 𝒜} (hx : x ∈ ProjectiveSpectrum.basicOpen 𝒜 f) (c : GradedModule.NumDenSameDeg 𝒜 (GradedModule.intShift 𝒜 0) x.asHomogeneousIdeal.toIdeal.primeCompl) : (intShiftFiberLinearEquivOfMem 𝒜 hf d hx).symm (GradedModule.DegreeZeroLocalization.mk c) = GradedModule.DegreeZeroLocalization.mk { deg := c.deg + (-d).toNat, num := ⟨↑c.num * f ^ d.toNat, ⋯⟩, den := ⟨↑c.den * f ^ (-d).toNat, ⋯⟩, den_mem := ⋯ }

The pointwise inverse trivialization on a homogeneous fraction.

noncomputable def AlgebraicGeometry.Proj.intShiftSectionAddEquivOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 d)).obj.obj (Opposite.op U) ≃+ (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 0)).obj.obj (Opposite.op U)

Over any open contained in D₊(f), an integer twist is trivial on sections.

Equations

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

noncomputable def AlgebraicGeometry.Proj.intShiftSectionLinearEquivOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 d)).obj.obj (Opposite.op U) ≃ₗ[↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U))] (associatedSheafInType 𝒜 (GradedModule.intShift 𝒜 0)).obj.obj (Opposite.op U)

The integer chart trivialization is linear over the structure-sheaf sections.

Equations

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

noncomputable def AlgebraicGeometry.Proj.natShiftSectionToSelfOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op U)) : (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op U)

Divide a locally fractional section of A(d)̃ by f ^ d, over any open contained in D₊(f).

The trivialization is pointwise, so nothing in the construction refers to the chart itself: only membership in D₊(f) is used, and hU supplies exactly that.

Equations

• AlgebraicGeometry.Proj.natShiftSectionToSelfOn 𝒜 hf d hU s = ⟨fun (x : ↥(Opposite.unop (Opposite.op U))) => (AlgebraicGeometry.Proj.natShiftFiberLinearEquivOfMem 𝒜 hf d ⋯) (↑s x), ⋯⟩

noncomputable def AlgebraicGeometry.Proj.natShiftSectionFromSelfOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op U)) : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op U)

Multiply a locally fractional section of Ã by f ^ d, over any open contained in D₊(f).

Equations

• AlgebraicGeometry.Proj.natShiftSectionFromSelfOn 𝒜 hf d hU s = ⟨fun (x : ↥(Opposite.unop (Opposite.op U))) => (AlgebraicGeometry.Proj.natShiftFiberLinearEquivOfMem 𝒜 hf d ⋯).symm (↑s x), ⋯⟩

noncomputable def AlgebraicGeometry.Proj.natShiftSectionToSelf {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) (s : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))) : (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))

Divide a locally fractional section of A(d)̃ by f ^ d.

Equations

• AlgebraicGeometry.Proj.natShiftSectionToSelf 𝒜 hf d s = AlgebraicGeometry.Proj.natShiftSectionToSelfOn 𝒜 hf d ⋯ s

noncomputable def AlgebraicGeometry.Proj.natShiftSectionFromSelf {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) (s : (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))) : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))

Multiply a locally fractional section of Ã by f ^ d.

Equations

• AlgebraicGeometry.Proj.natShiftSectionFromSelf 𝒜 hf d s = AlgebraicGeometry.Proj.natShiftSectionFromSelfOn 𝒜 hf d ⋯ s

theorem AlgebraicGeometry.Proj.natShiftSectionToSelfOn_map {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {U U' : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (hU' : U' ≤ U) (s : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op U)) : (CategoryTheory.ConcreteCategory.hom ((associatedSheafInType 𝒜 𝒜).obj.map (CategoryTheory.homOfLE hU').op)) (natShiftSectionToSelfOn 𝒜 hf d hU s) = natShiftSectionToSelfOn 𝒜 hf d ⋯ ((CategoryTheory.ConcreteCategory.hom ((associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.map (CategoryTheory.homOfLE hU').op)) s)

Dividing by f ^ d commutes with restriction to a smaller open.

This is what makes the pointwise trivialization a map of presheaves rather than a family of unrelated maps: restriction in M̃ is precomposition of the underlying function, and the trivialization is applied pointwise, so the two operations do not interact.

theorem AlgebraicGeometry.Proj.natShiftSectionFromSelfOn_map {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {U U' : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (hU' : U' ≤ U) (s : (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op U)) : (CategoryTheory.ConcreteCategory.hom ((associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.map (CategoryTheory.homOfLE hU').op)) (natShiftSectionFromSelfOn 𝒜 hf d hU s) = natShiftSectionFromSelfOn 𝒜 hf d ⋯ ((CategoryTheory.ConcreteCategory.hom ((associatedSheafInType 𝒜 𝒜).obj.map (CategoryTheory.homOfLE hU').op)) s)

Multiplying by f ^ d commutes with restriction to a smaller open.

@[simp]

theorem AlgebraicGeometry.Proj.natShiftSectionFromSelfOn_apply {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op U)) (x : ↥U) : ↑(natShiftSectionFromSelfOn 𝒜 hf d hU s) x = (natShiftFiberLinearEquivOfMem 𝒜 hf d ⋯).symm (↑s x)

Pointwise value of the chart trivialization on sections.

Stated here, in the generic grading, rather than unfolded at each use. A caller working over a concrete grading — the polynomial one, say — has types large enough that asking change to see through natShiftSectionFromSelfOn exhausts the isDefEq budget, while rewriting with this costs nothing.

@[simp]

theorem AlgebraicGeometry.Proj.natShiftFiberLinearEquivOfMem_symm_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {x : ProjectiveSpectrum 𝒜} (hx : x ∈ ProjectiveSpectrum.basicOpen 𝒜 f) (c : GradedModule.NumDenSameDeg 𝒜 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl) : (natShiftFiberLinearEquivOfMem 𝒜 hf d hx).symm (GradedModule.DegreeZeroLocalization.mk c) = GradedModule.DegreeZeroLocalization.mk { deg := c.deg, num := ⟨↑c.num * f ^ d, ⋯⟩, den := c.den, den_mem := ⋯ }

Value of the inverse pointwise trivialization on a homogeneous fraction.

natShiftFiberLinearEquivOfMem is natShiftLinearEquivOfMem at the prime complement, so this is that lemma transported; it exists so callers can rewrite without unfolding the fiber abbreviation.

noncomputable def AlgebraicGeometry.Proj.natShiftSectionAddEquivOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op U) ≃+ (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op U)

Over any open contained in D₊(f), a nonnegative twist is additively equivalent to the structure module when f has degree one.

Equations

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

noncomputable def AlgebraicGeometry.Proj.natShiftSectionLinearEquivOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op U) ≃ₗ[↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U))] (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op U)

Over any open contained in D₊(f), the chart trivialization is linear over the structure-sheaf sections of that open.

Equations

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

theorem AlgebraicGeometry.Proj.natShiftSectionFromSelfOn_selfBasicOpenSectionAddEquiv_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f g : A} (hf : f ∈ 𝒜 1) {m : ℕ} (hg : g ∈ 𝒜 m) (hm : 0 < m) (d : ℕ) (hle : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (c : GradedModule.NumDenSameDeg 𝒜 𝒜 (Submonoid.powers g)) : natShiftSectionFromSelfOn 𝒜 hf d hle ((selfBasicOpenSectionAddEquiv 𝒜 hg hm) (GradedModule.DegreeZeroLocalization.mk c)) = (moduleAwayToSection 𝒜 (GradedModule.natShift 𝒜 d) g) (GradedModule.DegreeZeroLocalization.mk { deg := c.deg, num := ⟨↑c.num * f ^ d, ⋯⟩, den := c.den, den_mem := ⋯ })

Untwisting a canonical structure-module section is the canonical twisted section.

This is the pointwise heart of every "the constructed comparison is the canonical one" argument for a nonnegative twist, isolated in the generic grading on purpose. Stated here the types stay small and the proof is a chain of rewrites; instantiated at a concrete grading — the polynomial one, where a Čech denominator is a product of variables — the same reasoning done inline exhausts the isDefEq budget. Callers should rewrite with this rather than unfold.

g cuts out the open and needs positive degree; f is the degree-one element doing the trivializing, and only has to be invertible there, which hle records.

noncomputable def AlgebraicGeometry.Proj.natShiftSectionAddEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f)) ≃+ (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))

Over D₊(f), a nonnegative twist is additively equivalent to the structure module when f has degree one.

Equations

• AlgebraicGeometry.Proj.natShiftSectionAddEquiv 𝒜 hf d = AlgebraicGeometry.Proj.natShiftSectionAddEquivOn 𝒜 hf d ⋯

noncomputable def AlgebraicGeometry.Proj.natShiftSectionLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f)) ≃ₗ[↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f)))] (associatedSheafInType 𝒜 𝒜).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))

The chart trivialization is linear over the structure-sheaf sections on D₊(f).

Equations

• AlgebraicGeometry.Proj.natShiftSectionLinearEquiv 𝒜 hf d = AlgebraicGeometry.Proj.natShiftSectionLinearEquivOn 𝒜 hf d ⋯

The canonical basic-open map

noncomputable def AlgebraicGeometry.Proj.natShiftBasicOpenSectionAddEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : ↥(GradedModule.DegreeZeroLocalization 𝒜 (GradedModule.natShift 𝒜 d) (Submonoid.powers f)) ≃+ (associatedSheafInType 𝒜 (GradedModule.natShift 𝒜 d)).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))

The algebraic chart trivialization, the structure-module comparison, and the sheaf chart trivialization combine to identify the localized shift with its sections on D₊(f).

Equations

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

theorem AlgebraicGeometry.Proj.natShiftBasicOpenSectionAddEquiv_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) (c : GradedModule.NumDenSameDeg 𝒜 (GradedModule.natShift 𝒜 d) (Submonoid.powers f)) : (natShiftBasicOpenSectionAddEquiv 𝒜 hf d) (GradedModule.DegreeZeroLocalization.mk c) = (moduleAwayToSection 𝒜 (GradedModule.natShift 𝒜 d) f) (GradedModule.DegreeZeroLocalization.mk c)

The chart equivalence above is the canonical homogeneous-fraction section map.

theorem AlgebraicGeometry.Proj.natShiftBasicOpenSectionAddEquiv_toAddMonoidHom {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : (natShiftBasicOpenSectionAddEquiv 𝒜 hf d).toAddMonoidHom = moduleAwayToSection 𝒜 (GradedModule.natShift 𝒜 d) f

As an additive map, the constructed chart equivalence is exactly the canonical map from homogeneous fractions to locally fractional sections.

theorem AlgebraicGeometry.Proj.moduleAwayToSection_natShift_degreeOne_bijective {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : Function.Bijective ⇑(moduleAwayToSection 𝒜 (GradedModule.natShift 𝒜 d) f)

For a nonnegative twist, the canonical basic-open section map is bijective on every degree-one chart.

The same trivialization, for a graded module

TwistLocalization.lean's GradedModule section trivializes an integer twist of an arbitrary graded module on any localization containing a degree-one element. The fiber at a point of D₊(f) is such a localization, so the pointwise statement costs nothing beyond naming it — exactly as intShiftFiberLinearEquivOfMem costs nothing over intShiftZeroLinearEquiv.

Everything above this section is 𝒜 as a module over itself, which is all the twisting sheaf needs. #584's tensor comparison F ⊗ O(d) ≅ F(d) needs the module case, and this is the fiber half of it. The section and .over halves are not here.

noncomputable def AlgebraicGeometry.Proj.intShiftModuleFiberLinearEquivOfMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {x : ProjectiveSpectrum 𝒜} (hx : x ∈ ProjectiveSpectrum.basicOpen 𝒜 f) : ↥(Fiber 𝒜 (GradedModule.intShift 𝓜 d) x) ≃ₗ[HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl] ↥(Fiber 𝒜 (GradedModule.intShift 𝓜 0) x)

The pointwise trivialization of M(d) at a point lying in D₊(f), for an integer twist.

Equations

• AlgebraicGeometry.Proj.intShiftModuleFiberLinearEquivOfMem 𝒜 𝓜 hf d hx = GradedModule.DegreeZeroLocalization.intShiftZeroModuleLinearEquiv 𝒜 𝓜 hf d hx

noncomputable def AlgebraicGeometry.Proj.intShiftModuleFiberLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) (x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)) : ↥(Fiber 𝒜 (GradedModule.intShift 𝓜 d) ↑x) ≃ₗ[HomogeneousLocalization 𝒜 (↑x).asHomogeneousIdeal.toIdeal.primeCompl] ↥(Fiber 𝒜 (GradedModule.intShift 𝓜 0) ↑x)

The pointwise trivialization of M(d) at a point of D₊(f), for an integer twist.

Equations

• AlgebraicGeometry.Proj.intShiftModuleFiberLinearEquiv 𝒜 𝓜 hf d x = AlgebraicGeometry.Proj.intShiftModuleFiberLinearEquivOfMem 𝒜 𝓜 hf d ⋯

The same, on sections

The section-level port of the fiber trivialization above. The shape is intShiftSectionToZeroOn's exactly: apply the fiber equivalence pointwise, then rebuild the local-fraction certificate with the _apply_mk rule. The numerator becomes f ^ k • r rather than r * f ^ k, which is the order LocalizedModule.mk_smul_mk produces; the denominator is unchanged, because it lives in 𝒜 either way.

noncomputable def AlgebraicGeometry.Proj.intShiftModuleSectionToZeroOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 d)).obj.obj (Opposite.op U)) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 0)).obj.obj (Opposite.op U)

Divide a locally fractional section of M(d)~ by f ^ d, over any open inside D₊(f).

Equations

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

noncomputable def AlgebraicGeometry.Proj.intShiftModuleSectionFromZeroOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) (s : (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 0)).obj.obj (Opposite.op U)) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 d)).obj.obj (Opposite.op U)

The inverse trivialization on sections, over any open contained in D₊(f).

Equations

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

noncomputable def AlgebraicGeometry.Proj.intShiftModuleSectionAddEquivOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 d)).obj.obj (Opposite.op U) ≃+ (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 0)).obj.obj (Opposite.op U)

Over any open contained in D₊(f), an integer twist of a module is trivial on sections.

Equations

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

noncomputable def AlgebraicGeometry.Proj.intShiftModuleSectionLinearEquivOn {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} (hU : U ≤ ProjectiveSpectrum.basicOpen 𝒜 f) : (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 d)).obj.obj (Opposite.op U) ≃ₗ[↑((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U))] (associatedSheafInType 𝒜 (GradedModule.intShift 𝓜 0)).obj.obj (Opposite.op U)

The module chart trivialization is linear over the structure-sheaf sections.

Equations

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