Serre finiteness for projective varieties #
A projective variety over k has finite-dimensional coherent cohomology in every degree, and
its FiniteDimensionalCohomology package is a theorem: step 3 of #332, closing it for every
variety with a projective presentation into a projective space with at least two coordinates.
The transport, and why it has to be linear #
The closed-immersion comparison identifies Hⁱ(X, F) with Hⁱ(Pⁿ, ι_* F) as abelian groups.
An additive isomorphism onto a finite-dimensional k-space bounds nothing over an infinite field,
so the identification has to be shown k-linear before finiteness can cross it. The base field
acts on both sides through global functions, and the two actions match because ι is a morphism
over Spec k: the global function a scalar becomes on X is the pullback of the one it becomes on
Pⁿ (baseFieldToGlobalSections_comp), and pushforward carries multiplication by the pulled-back
function to multiplication by the original (pushforward_varietyScalarAction). The comparison is
natural in the sheaf (coherentHPushforwardAddEquiv_naturality, from extAdjunctionMap_comp_mk₀
and associativity of Ext), so it commutes with the scalar endomorphisms, which is linearity.
The HasExt witness #
coherentH names its groups at HasExt.standard, in universe u + 1;
cohCohomologyPushforwardAddEquiv lets instance search find the Grothendieck-category witness in
universe u, so it compares different groups. coherentHPushforwardAddEquiv is the same
comparison instantiated at the standard witness (cohomologyPushforwardAddEquivAt), which is what
lets it be stated against coherentH at all.
Two coordinates #
The projective-space theorem takes Nontrivial ι: on P⁰, a point, a negative twist is the
structure sheaf and its degree-zero cohomology is k, not 0, so the dévissage's degree-zero
step needs a different argument there. A presentation into P⁰ or into the empty P⁻¹ describes
a point or the empty scheme, whose cohomology is the affine case; it is excluded here by the
Nontrivial P.index hypothesis rather than treated.
Two spellings of the structure morphism #
ProjectivePresentation states its compatibility against AlgebraicGeometry.projectiveSpaceToSpec,
built from homogeneousZeroRingEquiv; the Over instance on Pⁿ uses
Proj.projectiveSpaceToSpec, built from the algebra map. projectiveSpaceToSpec_eq says they are
the same morphism, because both ring maps send r to the constant polynomial r.
A scalar becomes, on X, the pullback of the global function it becomes on Y, for
g : X ⟶ Y over Spec k.
Pushforward carries the scalar action to the scalar action. Over an open U of Y, both
sides multiply a section of F over g⁻¹ U by the restriction of the same global function of
X; the pushforward's module structure is restriction of scalars along g, which is what turns
the function of Y into that function of X.
Pushforward carries the coherent scalar action to the coherent scalar action.
Hⁱ(X, F) ≃+ Hⁱ(Y, g_* F) for a closed immersion g, at the HasExt witness coherentH
uses. The same comparison as cohCohomologyPushforwardAddEquiv, instantiated at
HasExt.standard rather than at the witness instance search finds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The closed-immersion comparison is natural in the coherent sheaf: the abstract naturality
cohomologyPushforwardAddEquivAt_naturality, read through toSheaf, which commutes with
pushforward on the nose.
The closed-immersion comparison is base-field linear. Naturality against the scalar endomorphism, followed by the identification of its pushforward with the scalar endomorphism of the pushforward.
Hⁱ(X, F) ≃ₗ[k] Hⁱ(Y, g_* F) for a closed immersion g over Spec k.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Finite-dimensionality descends along a closed immersion over Spec k.
The two structure morphisms of polynomial projective space agree. homogeneousZeroRingEquiv
and the algebra map both send r to the constant polynomial r.
Serre finiteness for a projective variety: every coherent sheaf on X has
finite-dimensional cohomology in every degree, given a presentation into a projective space with
at least two coordinates.
The finite-dimensional cohomology package of a projective variety, proved from a presentation rather than supplied.
Equations
- P.finiteDimensionalCohomology = { toLinearCohomology := AlgebraicGeometry.Cohomology.canonicalLinearCohomology X, finite := ⋯ }
Instances For
The finite cohomology package of a projective variety: Serre finiteness with the finite-affine-cover vanishing bound.