The base field acting on sections of a twist #
FiniteDimensionalCohomology asks for Module.Finite k, and the k-action it means is
coherentScalarAction: multiplication by the global function a scalar becomes under the
structure morphism. The Čech lane, by contrast, computes in graded localizations, where k acts
through the constants (polynomialToHomogeneousLocalization). Nothing so far says these are the
same action, and #666's finiteness statement is meaningless until they are.
This file closes that gap at the level of sections.
openToLocalization_baseFieldToGlobalSections— the global function a scalar becomes has valuer / 1at every point. This isopenToLocalization_toSpecZero_appTopcomposed with the surjectionk → 𝒜 0, since the structure morphism ofPⁿisProj.toSpecZerofollowed by the spectrum of that surjection.varietyScalarAction_apply_fiber— hence the action on sections of an associated sheaf is plain scalar multiplication in each fiber. The structure-sheaf action on those sections is pointwise by construction (sectionsSubmodule), so this is the previous lemma plusglobalSectionSmul_appand nothing else.
What is still missing #
The comparison intCechTermSectionAddEquiv between a Čech term and these sections is five steps,
and none has been shown k-linear yet. Two of them are already LinearEquivs over
HomogeneousLocalization, two are pointwise linear, and one is a RingEquiv; the content of this
file is what makes each of those statements true rather than merely plausible. Until that is done,
module_finite_linearCoherentH_of_cech cannot be fed and #666 is not closed.
The base field acts through the constants. The global function a scalar becomes on
projective space has value r / 1 at every point, which is exactly the map
polynomialToHomogeneousLocalization that the graded localizations are k-modules by.
This is openToLocalization_toSpecZero_appTop composed with the surjection k → 𝒜 0: the
structure morphism of Pⁿ is Proj.toSpecZero followed by the spectrum of that surjection.
The base-field action on sections is scalar multiplication, fiber by fiber.
varietyScalarAction is multiplication by the global function attached to the scalar, and the
structure-sheaf action on an associated sheaf is pointwise on fibers by construction. Combining
those with the previous lemma leaves plain scalar multiplication in each fiber — which is what
lets the Čech lane's k-action be compared against the one the finiteness interface consumes.
The constant r restricted to any open, at the type the sections module wants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The restriction of the constant r to a chart, at the type the sections module wants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
It agrees with the chart-level constSection.
The sheaf endomorphism is multiplication by the restricted constant, on any open.
The canonical fraction-to-section map is k-linear. It is pointwise mapOfLE, and the
constant r restricted to the chart has value r / 1 at every point, so both sides scale the
same fiber by the same scalar.
The Čech comparison is k-linear.
The five-step composite never has to be taken apart: intCechTermSectionAddEquiv_apply_mk
already identifies it with moduleAwayToSection on every mk, and mk is surjective. So the
linearity of the whole chain is the linearity of one pointwise mapOfLE.
This is what lets a spanning set computed in the graded localizations be read as a spanning set
for the action module_finite_linearCoherentH_of_cech consumes.