Irreducible positive-dimensional vanishing #
Assembly of the irreducible positive-dimensional case of Hartshorne III.2.7. Given the
induction hypothesis VanishingIH on spaces of strictly smaller Krull dimension, this
file proves vanishing for all sheaves on an irreducible Noetherian space X with
dim X > 0.
The key Noetherian-shrinking step exists_section_generating_stalks uses Nat.find to
pick a point x₀ whose image subgroup is generated by a minimal positive integer d,
then propagates divisibility d | d_x to every other point of a sufficiently small
neighbourhood by minimality.
Main definitions #
VanishingIH— the induction hypothesis predicate.
Main results #
sHom_stalk_bijective_at— stalk-bijectivity criterion for the section homomorphism.exists_nonzero_stalk_in_V— a nonzero subsheaf ofzeroOutsideInt Vhas a nonzero stalk at some point ofV.exists_section_generating_stalks,exists_good_section,subsheaf_contains_zeroOutsideInt— the Noetherian-shrinking step.closedComplementVanishing— vanishing for sheaves supported on a closed complement.zeroOutsideInt_vanishing,zeroOutsideInt_cohomology_vanishing— Step 5 vanishing.subsheaf_zeroOutsideInt_vanishing— Step 4 vanishing.epiImage_zeroOutsideInt_vanishing_of_locallySurjective— Steps 3C + 4 + LES combined.irreducible_pos_vanishing— the headline assembly.
The stalk map of sHom s at x ∈ U is bijective when every stalk element of R at x
is an integer multiple of germ(s, x), and R embeds into zeroOutsideInt V
(providing torsion-freeness needed for injectivity).
A nonzero subsheaf of zeroOutsideInt V has a nonzero stalk at some point of V.
At each point x ∈ V, the image of the stalk of R under i is a subgroup of
stalk(zeroOutsideInt V, x) ≅ ULift ℤ. Transporting to ℤ and applying
Int.subgroup_cyclic, if this image is nonzero, it has a positive generator d_x.
The "index" d_x measures how deeply
R sits inside zeroOutsideInt V at x.
This lemma produces V' ≤ V, V' ≠ ⊥, and s ∈ R(V') such that for all x ∈ V':
(1) germ(s, x) ≠ 0
(2) every stalk element of R at x is an integer multiple of germ(s, x).
This is the hard "Noetherian shrinking" step of Hartshorne III.2.7, Step 4.
Core construction for Step 4: find V' ≤ V, V' ≠ ⊥, and a section s ∈ R(V') such that
sHom s : zeroOutsideInt V' ⟶ R is a stalk-isomorphism on V'.
Uses: minimum-index point, generator section, locally constant germ shrinking.
Structure lemma (Hartshorne Step 4 core): a nonzero subsheaf of zeroOutsideInt V
contains zeroOutsideInt V' for some nonempty open V' ⊆ V, with the inclusion
being a stalk-isomorphism on V'. This follows from: stalks of Z_V are ℤ or 0,
stalks of R are d_x·ℤ ⊆ ℤ, and after shrinking to an open where the multiplicity
d_x is constant and minimal, R restricts to d·Z_{V'} ≅ Z_{V'}.
Step 4/5 vanishing assembly #
The induction hypothesis for Grothendieck vanishing: vanishing holds for all sheaf-valued presheaves on all spaces of strictly smaller Krull dimension than X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Vanishing for a sheaf supported on the complement of an open V, via the
closed-immersion SES on Y = Vᶜ. This is the support-vanishing input used by the
Step 5 irreducible-space assembly immediately below.
Step 5 (Hartshorne III.2.7): given vanishing of the cokernel of
openHom(V ≤ ⊤) at degree m, deduce vanishing of zeroOutsideInt V at
degree m + 1. Uses the SES 0 → zeroOutsideInt V → zeroOutsideInt ⊤ → cokernel → 0
where zeroOutsideInt ⊤ = Z_X (constant sheaf, flasque on irreducible spaces).
Step 5 (Hartshorne III.2.7): zeroOutsideInt V has vanishing cohomology in every
degree m > dim X on an irreducible Noetherian space.
Proof: write m = m' + 1, apply zeroOutsideInt_vanishing (SES + flasque), then prove
cokernel vanishing at m' via the closed-immersion middle-term API, which transports
cohomology along the PushforwardHIso closed-inclusion comparison.
Step 4 (Hartshorne III.2.7): any subsheaf of zeroOutsideInt V has vanishing
cohomology in degree m > dim X. Uses subsheaf_contains_zeroOutsideInt to find
V' ⊆ V with Z_{V'} ↪ R (stalk-iso on V'). The cokernel is supported on (V')^c
(dim < dim X), so vanishes by the IH. Middle-term LES gives H^m(R) = 0.
Steps 3C + 4 + LES (Hartshorne III.2.7): any locally surjective image of
zeroOutsideInt V has vanishing cohomology in degree m > dim X. Uses third-term LES with
zeroOutsideInt_cohomology_vanishing (Step 5) and
subsheaf_zeroOutsideInt_vanishing (Step 4).
Irreducible positive-dimensional vanishing (Hartshorne III.2.7, irreducible case). Uses the closed immersion step and induction on a proper closed subset.