Twists on polynomial projective space #
This file constructs the comparison between degree-d homogeneous polynomials and global
sections of O(d) on polynomial Proj. The proof uses the variable basic-open cover, the
constructed chart comparison from TwistChart, and the generic point of the polynomial ring.
The global-section comparison is stated over a field and for a nonempty finite variable type, which is the projective-space range consumed by the Serre-finiteness argument. These hypotheses make the generic-point and denominator-cancellation steps explicit.
The global-section comparison is for a nonnegative twist. The imported algebraic layer owns
variable generation, exact monomial division, the canonical localization fraction, and both Čech
terms: polynomialVariableCechTerm for d : ℕ and polynomialVariableIntCechTerm for d : ℤ.
This file begins where geometry enters by comparing those terms with projective basic opens and
sections. The two algebraic terms are not yet identified for a nonnegative d; the landed Čech
differential still uses the ℕ version.
A homogeneous polynomial of degree d defines the global section represented everywhere
by the fraction p / 1 in the shifted module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The zero homogeneous ideal is the generic point of polynomial projective space.
Equations
- AlgebraicGeometry.Proj.polynomialGenericPoint ι k = { asHomogeneousIdeal := ⊥, isPrime := ⋯, not_irrelevant_le := ⋯ }
Instances For
Restriction of a global natural-twist section to the variable chart D₊(Xᵢ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The homogeneous fraction representing a global section on the variable chart D₊(Xᵢ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The denominator submonoid at the polynomial generic point.
Equations
Instances For
Every variable is invertible at the polynomial generic point.
A variable-chart fraction viewed in the common generic localization.
Equations
Instances For
All variable-chart representatives of a global section have the same generic value.
Passing from a variable localization to the generic localization loses no information.
Restricting the polynomial section to a variable chart recovers the literal fraction
p / 1.
The fractions p / 1 on any two variable charts agree in the generic localization.
The standard variable basic opens cover polynomial projective space.
A global section of a nonnegative twist on polynomial projective space is represented by a single homogeneous polynomial.
Distinct homogeneous polynomials define distinct global sections.
Concrete additive comparison between degree-d homogeneous polynomials and global sections
of the natural-shift model of O(d).
Equations
Instances For
Global sections of the integer-indexed twisting sheaf O(d).
Equations
Instances For
For a nonnegative twist, transport global sections from the natural-shift model to the integer-indexed twisting sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The concrete global-section comparison requested for polynomial projective space:
degree-d homogeneous polynomials are exactly Γ(Proj k[Xᵢ], O(d)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Global sections equipped with the canonical field-module structure transported through the explicit polynomial comparison. This avoids pretending that a separate base-ring action is definitionally present in Mathlib's sheaf-of-modules section type.
Equations
Instances For
The concrete comparison as an isomorphism of k-modules, using the transported action made
explicit by polynomialTwistingGlobalSectionsModule.
Equations
Instances For
Nonnegative twists on polynomial projective space are quasi-coherent.
The variable charts have degree one and cover, which is exactly the hypothesis of
natShift_isQuasicoherent. No comparison on higher-degree charts is needed or available.
Every integer twist of polynomial projective space is quasi-coherent.
The variable charts have degree one and generate, which is exactly the hypothesis
intShift_isQuasicoherent takes. The sign of d never enters. This is the negative-twist
input the Serre-finiteness dévissage needs.
Comparing the algebraic variable Čech diagram with projective basic opens #
The basic open of the product denominator is exactly the finite intersection of the corresponding variable charts.
The algebraic Čech term for O(d) is the sections of O(d) over the corresponding
intersection.
Three comparisons compose, and each is used at exactly the generality it has. The denominator
has degree n + 1, so no degree-one hypothesis can be applied to it directly:
natShiftLinearEquivOfMulMemtrivializesA(d)at the algebraic level. It needsX (x 0)invertible in the localization rather than a member of it, whichX_mul_cechCofactorsupplies —.powers (∏ₐ X_{x a})contains no degree-one element forn ≥ 1.selfBasicOpenSectionAddEquivcompares the structure module with its sections, and is already general in the degree of the denominator.natShiftSectionAddEquivOntrivializes at the sheaf level, over any open below a degree-one chart;basicOpen_denominator_leplaces the intersection below the first variable's chart.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Čech comparison is the canonical homogeneous-fraction section map.
This is what makes the comparison usable rather than merely existent. As defined,
cechTermSectionAddEquiv is a composite of three equivalences, two of which are built from a
choice of trivializing element — the first variable X (x 0) of the index. Nothing about the
statement should depend on that choice, and this says so: the composite is
moduleAwayToSection, which is canonical and refers to no trivialization at all. The two
trivializations cancel, one algebraic and one pointwise on stalks.
The consequence worth having is that moduleAwayToSection is defined pointwise, by enlarging
the denominator submonoid at each point. Any statement about how the comparison interacts with
restriction to a smaller open therefore reduces to a pointwise computation, instead of having to
be pushed through three constructed equivalences. That is the route to the Čech differential.
The Čech comparison intertwines the algebraic face with restriction of sections.
This is the compatibility the Čech differential is transported by: on the algebraic side the
j-th face is polynomialVariableCechFace, on the sheaf side it is restriction from the
(n + 1)-fold intersection to the (n + 2)-fold one, and the comparison carries one to the
other. It reduces to moduleAwayToSection_res_faceMap because
cechTermSectionAddEquiv_toAddMonoidHom already identifies the comparison with the canonical
pointwise map, where restriction only reindexes the point.
The integer-twist Čech comparison: the algebraic term at one variable intersection is the
sections of O(d) there, for a twist of either sign.
Five steps rather than the nonnegative case's three, and the two extra ones are both grading transports rather than geometry:
intShiftZeroLinearEquivOfMulMem— the cofactor trivialization. The Čech denominator has degreen + 1, sof = X (x 0)is only invertible in it, never a member; the cofactor is the product of the remaining variables.linearEquivOfMemIff—A(0)isA, at the localization level.selfBasicOpenSectionAddEquiv— the structure module against its sections.sectionAddEquivOfMemIff—AisA(0), at the section level.intShiftSectionAddEquivOn— the chart trivialization, undone.
Steps 2 and 4 exist because the integer trivializations land at A(0) while the section
comparison is stated against A; they move no data at all.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integer Čech comparison is the canonical homogeneous-fraction section map.
The five-step composite has to be named by change before anything will rewrite: simp will
not unfold it far enough to expose the mk argument, because two of the steps are AddEquiv
transports whose apply lemmas only fire once the argument is already in mk form. Naming the
chain, then rewriting inside-out, reduces the whole statement to a pointwise identity in the
localization at each prime, closed by ring.
The integer Čech comparison intertwines the algebraic face with restriction of sections.
This is cechTermSectionAddEquiv_res_face for a twist of either sign, and it is the same proof:
once intCechTermSectionAddEquiv_toAddMonoidHom has identified the five-step composite with the
canonical fraction-to-section map, the statement is moduleAwayToSection_res_faceMap, which is
generic in the graded module and never mentions the twist. The sign lives entirely in the
intShift bookkeeping that intCechTermSectionAddEquiv already absorbed.
The canonical fraction-to-section map is bijective on every Čech intersection.
The degree-one statement moduleAwayToSection_natShift_degreeOne_bijective does not cover this:
a Čech denominator is a product of n + 1 variables, so it has degree n + 1, and the chart it
cuts out is not a degree-one chart once n ≥ 1.