Trivializing a graded-module twist after degree-one localization

If f is homogeneous of degree one, multiplication by f ^ d trivializes the natural shift A(d) after localizing away from f. This file constructs that statement at the exact degree-zero-localization level used by the associated-sheaf construction.

The sign convention is DerivedAlgGeo's convention A(d)ₙ = Aₙ₊d: a fraction in the shifted degree-zero localization has ordinary graded degree d. Multiplying it by f⁻ᵈ produces a degree-zero fraction, and multiplication by fᵈ is the inverse operation.

noncomputable def GradedModule.DegreeZeroLocalization.natShiftToSelfLinearMap {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) (Submonoid.powers f)) →ₗ[HomogeneousLocalization 𝒜 (Submonoid.powers f)] ↥(DegreeZeroLocalization 𝒜 𝒜 (Submonoid.powers f))

Divide an A(d) fraction by f ^ d, obtaining an ordinary degree-zero fraction.

Equations

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

noncomputable def GradedModule.DegreeZeroLocalization.selfToNatShiftLinearMap {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : ↥(DegreeZeroLocalization 𝒜 𝒜 (Submonoid.powers f)) →ₗ[HomogeneousLocalization 𝒜 (Submonoid.powers f)] ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) (Submonoid.powers f))

Multiply an ordinary degree-zero fraction by f ^ d, obtaining a fraction in A(d).

Equations

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

noncomputable def GradedModule.DegreeZeroLocalization.natShiftSelfLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) (Submonoid.powers f)) ≃ₗ[HomogeneousLocalization 𝒜 (Submonoid.powers f)] ↥(DegreeZeroLocalization 𝒜 𝒜 (Submonoid.powers f))

On a degree-one chart, the degree-zero localization of A(d) is canonically the chart ring as a module over itself.

Equations

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

@[simp]

theorem GradedModule.DegreeZeroLocalization.natShiftSelfLinearEquiv_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) (c : NumDenSameDeg 𝒜 (natShift 𝒜 d) (Submonoid.powers f)) : (natShiftSelfLinearEquiv 𝒜 hf d) (mk c) = mk { deg := c.deg + d, num := c.num, den := ⟨↑c.den * f ^ d, ⋯⟩, den_mem := ⋯ }

@[simp]

theorem GradedModule.DegreeZeroLocalization.natShiftSelfLinearEquiv_symm_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) (c : NumDenSameDeg 𝒜 𝒜 (Submonoid.powers f)) : (natShiftSelfLinearEquiv 𝒜 hf d).symm (mk c) = mk { deg := c.deg, num := ⟨↑c.num * f ^ d, ⋯⟩, den := c.den, den_mem := ⋯ }

noncomputable def GradedModule.DegreeZeroLocalization.natShiftAwayLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) : ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) (Submonoid.powers f)) ≃ₗ[HomogeneousLocalization 𝒜 (Submonoid.powers f)] HomogeneousLocalization 𝒜 (Submonoid.powers f)

The chart trivialization with Mathlib's homogeneous-localization ring as target.

Equations

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

Trivialization in any localization containing the degree-one element

theorem GradedModule.DegreeZeroLocalization.transitionScalar_mul {A : Type u} [CommRing A] {f : A} {S : Submonoid A} (n : ℕ) {g g' : A} (hgS : g ∈ S) (hg'S : g' ∈ S) : Localization.mk (g' ^ n) (GradedModule.DegreeZeroLocalization.twistPowerOfMem✝ n hgS) * Localization.mk (f ^ n) (GradedModule.DegreeZeroLocalization.twistPowerOfMem✝ n hg'S) = Localization.mk (f ^ n) (GradedModule.DegreeZeroLocalization.twistPowerOfMem✝ n hgS)

The transition cocycle: (g'/g)ⁿ · (f/g')ⁿ = (f/g)ⁿ.

Composing the transition from the g'-chart to the g-chart with the scalar that the g'-chart clears gives exactly the scalar the g-chart clears.

This is why the per-chart extensions of #585 agree where two charts meet: over D₊(g), s is cleared by (f/g)ⁿ, and over D₊(g') by (f/g')ⁿ; this identity says that carrying the second across by the transition lands on the first, with no correction factor.

Cancellation of g'ⁿ, and nothing else — note f never has to be a unit, it appears only in numerators.

noncomputable def GradedModule.DegreeZeroLocalization.natShiftToSelfLinearMapOfMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} (hfS : f ∈ S) : ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) S) →ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 𝒜 S)

Divide an A(d) fraction by f ^ d, given that f itself lies in S.

Membership is genuinely the hypothesis consumed, not merely invertibility of f in Localization S: the graded representative below keeps every denominator inside S by multiplying c.den by f ^ d, which needs f ^ d ∈ S. When f is only invertible — the Čech-intersection case, where the denominator submonoid contains no degree-one element at all — use natShiftLinearEquivOfMulMem, which asks instead for a homogeneous cofactor h with f * h ∈ S; taking h = 1 recovers the membership hypothesis.

Equations

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

noncomputable def GradedModule.DegreeZeroLocalization.selfToNatShiftLinearMapOfMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} : ↥(DegreeZeroLocalization 𝒜 𝒜 S) →ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) S)

Multiply an ordinary degree-zero fraction by f ^ d in any localization containing f.

Equations

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

Trivializing when f is only invertible, not a member

natShiftToSelfLinearMapOfMem asks for f ∈ S, but its own statement only needs f to be invertible in Localization S. The gap is not academic: on a Čech intersection the denominator submonoid is .powers (∏ₐ gₐ), which for more than one factor contains no degree-one element at all, while every gₐ is invertible there.

The hypothesis below records invertibility in the form the graded bookkeeping can use: a homogeneous cofactor h with f * h ∈ S. Division by f ^ d is then performed as multiplication by h ^ d / (f * h) ^ d, which is the same element of the localization but keeps every denominator literally inside S. Taking h = 1 recovers the membership hypothesis.

noncomputable def GradedModule.DegreeZeroLocalization.natShiftToSelfLinearMapOfMulMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} {h : A} {e : ℕ} (h_deg : h ∈ 𝒜 e) (hfh : f * h ∈ S) : ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) S) →ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 𝒜 S)

Divide an A(d) fraction by f ^ d whenever a homogeneous cofactor carries f into the denominator submonoid.

Equations

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

noncomputable def GradedModule.DegreeZeroLocalization.natShiftLinearEquivOfMulMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} {h : A} {e : ℕ} (h_deg : h ∈ 𝒜 e) (hfh : f * h ∈ S) : ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) S) ≃ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 𝒜 S)

Multiplication and division by f ^ d are inverse whenever a homogeneous cofactor carries f into the denominator submonoid. This is the form the Čech intersections need: there f is one variable and the cofactor is the product of the others.

Equations

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

noncomputable def GradedModule.DegreeZeroLocalization.natShiftLinearEquivOfMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} (hfS : f ∈ S) : ↥(DegreeZeroLocalization 𝒜 (natShift 𝒜 d) S) ≃ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 𝒜 S)

Multiplication and division by f ^ d give inverse degree-zero localization maps whenever f belongs to the denominator submonoid.

Equations

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

@[simp]

theorem GradedModule.DegreeZeroLocalization.natShiftLinearEquivOfMem_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} (hfS : f ∈ S) (c : NumDenSameDeg 𝒜 (natShift 𝒜 d) S) : (natShiftLinearEquivOfMem 𝒜 hf d hfS) (mk c) = mk { deg := c.deg + d, num := c.num, den := ⟨↑c.den * f ^ d, ⋯⟩, den_mem := ⋯ }

@[simp]

theorem GradedModule.DegreeZeroLocalization.natShiftLinearEquivOfMem_symm_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} (hfS : f ∈ S) (c : NumDenSameDeg 𝒜 𝒜 S) : (natShiftLinearEquivOfMem 𝒜 hf d hfS).symm (mk c) = mk { deg := c.deg, num := ⟨↑c.num * f ^ d, ⋯⟩, den := c.den, den_mem := ⋯ }

@[simp]

theorem GradedModule.DegreeZeroLocalization.natShiftLinearEquivOfMulMem_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℕ) {S : Submonoid A} {h : A} {e : ℕ} (h_deg : h ∈ 𝒜 e) (hfh : f * h ∈ S) (c : NumDenSameDeg 𝒜 (natShift 𝒜 d) S) : (natShiftLinearEquivOfMulMem 𝒜 hf d h_deg hfh) (mk c) = mk { deg := c.deg + d * (1 + e), num := ⟨↑c.num * h ^ d, ⋯⟩, den := ⟨↑c.den * (f * h) ^ d, ⋯⟩, den_mem := ⋯ }

Value of the cofactor trivialization on a homogeneous fraction.

The OfMem sibling above divides by f ^ d; here f need only be invertible, so the fraction is multiplied by the cofactor power h ^ d and the denominator picks up (f * h) ^ d instead. This is the computation rule the Čech comparison needs, where f is one variable and h is the product of the others.

Integer twists

intShift 𝒜 d is the zero-extended integer shift: its degree-n piece asks for an element of 𝒜 k with (k : ℤ) = n + d, and retains 0 when that integer is negative.

Lowering the twist by e while raising the fraction's degree by e leaves that integer condition identical — ((n + e : ℕ) : ℤ) + (d - e) = (n : ℤ) + d. So multiplying the denominator by f ^ e transports the whole disjunctive membership verbatim, and in particular the zero branch needs no separate treatment. That is what makes the integer case no harder than the natural one here, and it is the step a negative twist is built from: taking d = 0 sends A to A(-e).

theorem GradedModule.DegreeZeroLocalization.mem_intShift_sub_natCast_add {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) (d : ℤ) (e n : ℕ) (a : A) : a ∈ intShift 𝒜 (d - ↑e) (n + e) ↔ a ∈ intShift 𝒜 d n

The integer-shift membership condition depends only on the integer n + d, so raising the degree by e and lowering the twist by e is the same condition.

noncomputable def GradedModule.DegreeZeroLocalization.intShiftLowerLinearMap {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d : ℤ) (e : ℕ) (hfS : f ∈ S) : ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 d) S) →ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 (d - ↑e)) S)

Divide an A(d) fraction by f ^ e, lowering the integer twist to d - e.

Only membership of f in the denominator submonoid is used, exactly as in the nonnegative case; the twist d is unconstrained in sign.

Equations

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

theorem GradedModule.DegreeZeroLocalization.mul_pow_mem_intShift {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) (e n : ℕ) (a : A) (ha : a ∈ intShift 𝒜 (d - ↑e) n) : a * f ^ e ∈ intShift 𝒜 d n

Multiplying the numerator by f ^ e raises an integer twist back by e.

noncomputable def GradedModule.DegreeZeroLocalization.intShiftRaiseLinearMap {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d : ℤ) (e : ℕ) : ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 (d - ↑e)) S) →ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 d) S)

Multiply an A(d - e) fraction by f ^ e, raising the integer twist back to d.

Equations

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

noncomputable def GradedModule.DegreeZeroLocalization.intShiftLowerLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d : ℤ) (e : ℕ) (hfS : f ∈ S) : ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 d) S) ≃ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 (d - ↑e)) S)

Multiplication and division by f ^ e identify an integer twist with its lowering by e.

Taking d = 0 gives A ≃ A(-e) over any localization containing f, which is the negative twist the Serre-finiteness dévissage needs. The sign of d plays no role.

Equations

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

@[simp]

theorem GradedModule.DegreeZeroLocalization.intShiftLowerLinearEquiv_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d : ℤ) (e : ℕ) (hfS : f ∈ S) (c : NumDenSameDeg 𝒜 (intShift 𝒜 d) S) : (intShiftLowerLinearEquiv 𝒜 hf d e hfS) (mk c) = mk { deg := c.deg + e, num := ⟨↑c.num, ⋯⟩, den := ⟨↑c.den * f ^ e, ⋯⟩, den_mem := ⋯ }

Reaching twist zero

intShiftLowerLinearEquiv computes its target as d - e, which is awkward to aim at a prescribed twist: hitting A(0) from A(d) would need d - e to be definitionally zero. The hypothesis-carrying form below takes the target twist as a parameter instead, so a caller supplies the arithmetic as a proof rather than fighting a transport.

noncomputable def GradedModule.DegreeZeroLocalization.intShiftShiftLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d d' : ℤ) (e : ℕ) (hdd' : d' = d - ↑e) (hfS : f ∈ S) : ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 d) S) ≃ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 d') S)

intShiftLowerLinearEquiv with the target twist named rather than computed.

Equations

• GradedModule.DegreeZeroLocalization.intShiftShiftLinearEquiv 𝒜 hf d d' e hdd' hfS = ⋯ ▸ GradedModule.DegreeZeroLocalization.intShiftLowerLinearEquiv 𝒜 hf d e hfS

Trivializing an integer twist, without a sign split in the term

Writing the trivialization as if 0 ≤ d then … else … type-checks, but it makes every downstream computation branch: a locally fractional section carries an explicit degree/numerator/denominator certificate, so a caller needs a formula for the image of mk c, and a definition by cases yields one formula per branch forever after.

There is a single formula covering both signs. Multiplying by

f ^ (-d).toNat / f ^ d.toNat

divides by f ^ d when d ≥ 0 and multiplies by f ^ (-d) when d < 0, because exactly one of d.toNat and (-d).toNat is nonzero. The sign of d then appears only inside the degree bookkeeping, discharged by omega, and never in the term.

theorem GradedModule.DegreeZeroLocalization.mul_pow_toNat_mem_intShift_zero {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) (n : ℕ) (a : A) (ha : a ∈ intShift 𝒜 d n) : a * f ^ (-d).toNat ∈ intShift 𝒜 0 (n + d.toNat)

The numerator of the trivialized fraction lies in the degree the denominator does.

noncomputable def GradedModule.DegreeZeroLocalization.intShiftZeroLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d : ℤ) (hfS : f ∈ S) : ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 d) S) ≃ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 0) S)

Every integer twist is trivial on a localization containing a degree-one element.

One formula covers both signs; see the section comment.

Equations

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

@[simp]

theorem GradedModule.DegreeZeroLocalization.intShiftZeroLinearEquiv_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d : ℤ) (hfS : f ∈ S) (c : NumDenSameDeg 𝒜 (intShift 𝒜 d) S) : (intShiftZeroLinearEquiv 𝒜 hf d hfS) (mk c) = mk { deg := c.deg + d.toNat, num := ⟨↑c.num * f ^ (-d).toNat, ⋯⟩, den := ⟨↑c.den * f ^ d.toNat, ⋯⟩, den_mem := ⋯ }

The trivialization in explicit fractions, in one formula for both signs.

This is what makes the uniform definition worth having: a locally fractional section carries a degree/numerator/denominator certificate, and rebuilding it downstream needs exactly this rule — once, not once per sign.

theorem GradedModule.DegreeZeroLocalization.intShiftZeroLinearEquiv_transition {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) {g : A} (hg : g ∈ 𝒜 1) (hfS : f ∈ S) (hgS : g ∈ S) (n : ℕ) (z : ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 ↑n) S)) : ↑((intShiftZeroLinearEquiv 𝒜 hf (↑n) hfS) z) = Localization.mk (g ^ n) (GradedModule.DegreeZeroLocalization.twistPowerOfMem✝ n hfS) • ↑((intShiftZeroLinearEquiv 𝒜 hg (↑n) hgS) z)

The two degree-one trivializations of an integer twist differ by gⁿ / fⁿ.

intShiftZeroLinearEquiv is multiplication by intTwistScalar, which at a nonnegative twist n is 1 / fⁿ. So trivializing at f and trivializing at g differ by the unit gⁿ / fⁿ, and the identity reduces to a cancellation in Localization S.

This is the transition function of O(n) between two degree-one charts, and it is what an overlap comparison consumes: on D₊(f) ⊓ D₊(g) a section trivialized one way is gⁿ/fⁿ times the same section trivialized the other way.

Stated on the underlying LocalizedModule, which drops the degree bookkeeping entirely — both sides are scalar multiples of the same z, so no NumDenSameDeg appears and no degree has to be matched.

theorem GradedModule.DegreeZeroLocalization.mul_pow_toNat_mem_intShift {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} (hf : f ∈ 𝒜 1) (d : ℤ) (n : ℕ) (a : A) (ha : a ∈ intShift 𝒜 0 n) : a * f ^ d.toNat ∈ intShift 𝒜 d (n + (-d).toNat)

The numerator of the inverse trivialization lies in the twist it should.

@[simp]

theorem GradedModule.DegreeZeroLocalization.intShiftZeroLinearEquiv_symm_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} (hf : f ∈ 𝒜 1) (d : ℤ) (hfS : f ∈ S) (c : NumDenSameDeg 𝒜 (intShift 𝒜 0) S) : (intShiftZeroLinearEquiv 𝒜 hf d hfS).symm (mk c) = mk { deg := c.deg + (-d).toNat, num := ⟨↑c.num * f ^ d.toNat, ⋯⟩, den := ⟨↑c.den * f ^ (-d).toNat, ⋯⟩, den_mem := ⋯ }

The inverse trivialization in explicit fractions, again in one formula for both signs.

The cofactor form, for Čech intersections

intShiftZeroLinearEquiv asks for f ∈ S. A Čech intersection cannot supply that: the denominator there is ∏ₐ X_{x a}, homogeneous of degree n + 1, so for n ≥ 1 its powers submonoid contains no degree-one element at all. What is available is a homogeneous cofactor h with f * h ∈ S — the product of the remaining variables.

The scalar is parameterized by its two exponents rather than by d directly. That is not cosmetic: writing the inverse as the -d instance of the same definition puts (- -d).toNat in the term, which is only propositionally d.toNat, and every subsequent change fails on it. Naming the exponents makes the forward and inverse scalars the same definition with the pair swapped, and their product telescopes to (f * h) ^ (a + b) over itself.

theorem GradedModule.DegreeZeroLocalization.mul_pow_mul_pow_mem_intShift_zero {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f h : A} {e : ℕ} (hf : f ∈ 𝒜 1) (h_deg : h ∈ 𝒜 e) (a b : ℕ) (d : ℤ) (hd : d = ↑a - ↑b) (n : ℕ) (x : A) (hx : x ∈ intShift 𝒜 d n) : x * h ^ a * f ^ b ∈ intShift 𝒜 0 (n + a * (1 + e))

Degrees for the cofactor trivialization: multiplying by h ^ a * f ^ b carries the twist (a : ℤ) - b to the twist zero.

theorem GradedModule.DegreeZeroLocalization.mul_pow_mul_pow_mem_intShift {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f h : A} {e : ℕ} (hf : f ∈ 𝒜 1) (h_deg : h ∈ 𝒜 e) (a b : ℕ) (d : ℤ) (hd : d = ↑a - ↑b) (n : ℕ) (x : A) (hx : x ∈ intShift 𝒜 0 n) : x * h ^ b * f ^ a ∈ intShift 𝒜 d (n + b * (1 + e))

The same, in the direction that produces the twist rather than removing it.

noncomputable def GradedModule.DegreeZeroLocalization.intShiftZeroLinearEquivOfMulMem {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} {h : A} {e : ℕ} (hf : f ∈ 𝒜 1) (h_deg : h ∈ 𝒜 e) (a b : ℕ) (d : ℤ) (hd : d = ↑a - ↑b) (hfh : f * h ∈ S) : ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 d) S) ≃ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (intShift 𝒜 0) S)

Trivializing an integer twist when f is only invertible in S, via a homogeneous cofactor.

This is the form the Čech intersections need: there f is one variable of the index and h is the product of the others. The twist is given as (a : ℤ) - b so that the caller chooses the exponents; a = d.toNat, b = (-d).toNat recovers an arbitrary d.

Equations

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

@[simp]

theorem GradedModule.DegreeZeroLocalization.intShiftZeroLinearEquivOfMulMem_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} {h : A} {e : ℕ} (hf : f ∈ 𝒜 1) (h_deg : h ∈ 𝒜 e) (a b : ℕ) (d : ℤ) (hd : d = ↑a - ↑b) (hfh : f * h ∈ S) (c : NumDenSameDeg 𝒜 (intShift 𝒜 d) S) : (intShiftZeroLinearEquivOfMulMem 𝒜 hf h_deg a b d hd hfh) (mk c) = mk { deg := c.deg + a * (1 + e), num := ⟨↑c.num * h ^ a * f ^ b, ⋯⟩, den := ⟨↑c.den * (f * h) ^ a, ⋯⟩, den_mem := ⋯ }

The cofactor trivialization in explicit fractions.

The same trivialization for a graded module

Everything above is stated for 𝒜 as a module over itself, which is all the twisting sheaf needs and all that TwistChart.lean and Finiteness.lean ever ask for. The tensor comparison F ⊗ O(d) ≅ F(d) of #584 needs it for an arbitrary graded module, and nothing in the construction resists: intTwistScalar lives in Localization S and acts on LocalizedModule S M exactly as it acts on LocalizedModule S A.

Only two things are genuinely new. The degree bookkeeping is SetLike.GradedSMul.smul_mem where the ring case used SetLike.mul_mem_graded; and map_smul' has to name the algebraMap into Localization S, because the HomogeneousLocalization 𝒜 S-action is Module.compHom along it and the two actions commute only after that is made visible.

The numerator here is f ^ (-d).toNat • m rather than m * f ^ (-d).toNat, which is the order LocalizedModule.mk_smul_mk produces, so the numerator needs no mul_comm fix-up — only the denominator does.

theorem GradedModule.DegreeZeroLocalization.pow_smul_mem_intShift_zero {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (hf : f ∈ 𝒜 1) (d : ℤ) (n : ℕ) (m : M) (hm : m ∈ intShift 𝓜 d n) : f ^ (-d).toNat • m ∈ intShift 𝓜 0 (n + d.toNat)

The numerator of the trivialized fraction lies in the degree the denominator does.

theorem GradedModule.DegreeZeroLocalization.pow_smul_mem_intShift {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (hf : f ∈ 𝒜 1) (d : ℤ) (n : ℕ) (m : M) (hm : m ∈ intShift 𝓜 0 n) : f ^ d.toNat • m ∈ intShift 𝓜 d (n + (-d).toNat)

The numerator of the inverse trivialization lies in the twist it should.

noncomputable def GradedModule.DegreeZeroLocalization.intShiftZeroModuleLinearEquiv {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (hf : f ∈ 𝒜 1) (d : ℤ) (hfS : f ∈ S) : ↥(DegreeZeroLocalization 𝒜 (intShift 𝓜 d) S) ≃ₗ[HomogeneousLocalization 𝒜 S] ↥(DegreeZeroLocalization 𝒜 (intShift 𝓜 0) S)

Every integer twist of a graded module is trivial on a localization containing a degree-one element.

Equations

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

@[simp]

theorem GradedModule.DegreeZeroLocalization.intShiftZeroModuleLinearEquiv_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (hf : f ∈ 𝒜 1) (d : ℤ) (hfS : f ∈ S) (c : NumDenSameDeg 𝒜 (intShift 𝓜 d) S) : (intShiftZeroModuleLinearEquiv 𝒜 𝓜 hf d hfS) (mk c) = mk { deg := c.deg + d.toNat, num := ⟨f ^ (-d).toNat • ↑c.num, ⋯⟩, den := ⟨↑c.den * f ^ d.toNat, ⋯⟩, den_mem := ⋯ }

The trivialization in explicit fractions, in one formula for both signs.

The module analogue of intShiftZeroLinearEquiv_apply_mk, and needed for the same reason: a locally fractional section carries a degree/numerator/denominator certificate, and rebuilding it downstream needs exactly this rule.

@[simp]

theorem GradedModule.DegreeZeroLocalization.intShiftZeroModuleLinearEquiv_symm_apply_mk {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {S : Submonoid A} {M σM : Type u} [AddCommGroup M] [Module A M] [SetLike σM M] [AddSubgroupClass σM M] (𝓜 : ℕ → σM) [SetLike.GradedSMul 𝒜 𝓜] (hf : f ∈ 𝒜 1) (d : ℤ) (hfS : f ∈ S) (c : NumDenSameDeg 𝒜 (intShift 𝓜 0) S) : (intShiftZeroModuleLinearEquiv 𝒜 𝓜 hf d hfS).symm (mk c) = mk { deg := c.deg + (-d).toNat, num := ⟨f ^ d.toNat • ↑c.num, ⋯⟩, den := ⟨↑c.den * f ^ (-d).toNat, ⋯⟩, den_mem := ⋯ }

The inverse trivialization in explicit fractions, again in one formula for both signs.