Homogeneous elements as sections of the twist, and multiplication F ⟶ F(n) #
#585 asks that fⁿ · s extend to a global section of F(n), for F quasi-coherent on
Proj 𝒜 and s a section over a degree-one chart. That statement cannot be written against the
tree as it stands: multiplying a section of an arbitrary F by a homogeneous element needs a map
F ⟶ F(n), and no such map exists. #584 supplied the twist itself; this file supplies the
multiplication into it.
The observation that makes it short #
A degree-n element m of 𝓜 is a global section of M(n)~, not merely a section over a
basic open. The fraction is m / 1: a local fraction asks for numerator and denominator in the
same degree, 1 has degree 0, and mem_intShift_zero_of_mem says a degree-n element of 𝓜
lies in degree 0 of the shifted grading. Nothing is inverted, so the same fraction is valid at
every point of every open and restriction does not move it — which is why sectionsOfMem's
compatibility is rfl, and why no basicOpen_one transport is needed anywhere.
From there to an arbitrary F #
unitToTwist is that compatible family read through SheafOfModules.unitHomEquiv — a global
section is a map out of the unit. twistBy then tensors it with F and cancels the unit:
F ≅ F ⊗ 𝟙 --(𝟙 ⊗ ·fⁿ)--> F ⊗ O(n) = F(n)
F is an arbitrary module sheaf. It is not assumed to be an associated sheaf, which is the
point: #584's comparison stops at associated sheaves, and #585 may not inherit that limit —
its acceptance criteria forbid exactly that hypothesis. Nothing here needs the comparison.
The original #570 issue sketch proposed using these maps to build Γ_*(F) as a graded module,
with the A-action supplied by twist multiplication. That route is now historical: the completed
proof takes the direct chart-generation route instead. GlobalGeneration.lean consumes these maps
alongside the uniform extension theorem to obtain free I ↠ F ⊗ O(N), and TwistInverse.lean
then untwists it to the finite coproduct epimorphism. No graded Serre correspondence is asserted
here.
Why unitToTwist_app_one is not decoration #
unitHomEquiv.symm is an equivalence's inverse, so the morphism it produces is opaque at every use
site: a wrong sectionsOfMem would typecheck and nothing downstream would notice. That lemma pins
the content — 1 ↦ m / 1 — and is the only thing standing between this API and a map that asserts
nothing.
Its 1 is ascribed at the ring, (1 : ringCatSheaf.obj.obj (op U)), rather than written bare. The
unit sheaf's sections are the ring's sections by a def that does not unfold at reducible
transparency, so OfNat is not found on the bare numeral. references/instance-transparency.md
is the general case; Mathlib's own unitHomEquiv_apply_coe ascribes it for the same reason.
Scope #
The maps, and what they do to 1. The extension theorem of #585 is not here — it needs the
degree-one chart cover, quasi-coherence to make each chart a module, and an affine clearing lemma
for the denominator. With this API its statement elaborates, which is what it was blocked on; it is
proved in Proj/Modules/Glue.lean as exists_globalSection_twistBy.
A degree-n element of 𝓜 sits in degree 0 of the shifted grading.
Which is what makes it a global section of M(n)~ rather than one over a basic open: the
fraction m / 1 needs its numerator one degree-step below its denominator's degree, and 1 has
degree 0.
A degree-n element of 𝓜 is the section m / 1 of M(n)~, over any open.
Nothing is inverted, so the same fraction is valid at every point of every open, and restriction between opens does not move it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two spellings of the same element give the same section.
g ^ N and g ^ (1 * N) are equal but not syntactically so, and a twist produced at degree
e * N with e = 1 carries the second spelling while the generator lemmas carry the first.
The section m / 1 restricts to the section m / 1: nothing is inverted, so the same
fraction is valid at every point of every open.
The compatible family the fractions m / 1 form, which is what a map out of the unit
consumes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiplication by a degree-n element of 𝒜, as a map out of the structure sheaf.
#584 gave the twist; this gives the sections of it that a homogeneous element supplies, which
is what #585 multiplies by.
Equations
- AlgebraicGeometry.Proj.unitToTwist 𝒜 𝓜 n hm = (have this := AlgebraicGeometry.Proj.sheafTwist 𝒜 𝓜 ↑n; this).unitHomEquiv.symm (AlgebraicGeometry.Proj.sectionsOfMem 𝒜 𝓜 n hm)
Instances For
What unitToTwist does: it sends 1 to m / 1.
Without this the map is opaque — unitHomEquiv.symm is an equivalence's inverse, so nothing about
the resulting morphism is visible at a use site, and a wrong sectionsOfMem would go unnoticed.
Multiplication by a degree-n element of 𝒜, on an arbitrary module sheaf: F ⟶ F(n).
F is not assumed to be an associated sheaf, which is the whole point — #585 multiplies a
section of an arbitrary quasi-coherent F, and until this map exists the statement cannot even be
written. It is the map out of the unit, tensored with F and read through the right unitor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiplying by two spellings of the same element is the same map.