Flasque sheaves of modules and the cohomology of rational functions #
A sheaf of modules on a scheme is flasque when its underlying abelian presheaf is, that is, when
all of its restriction maps are surjective. TauCeti/Topology/Sheaves/Flasque.lean proves that a
flasque abelian sheaf has no higher cohomology; this file transports that statement to the
cohomology Hⁿ(X, M) of TauCeti/AlgebraicGeometry/Cohomology/Basic.lean and applies it to the
sheaf 𝒦_X of rational functions on an irreducible scheme.
The sheaf 𝒦_X is constant with value the function field on nonempty open subsets and zero on
the empty one, so it is flasque. Consequently, for every short exact sequence
0 ⟶ M ⟶ 𝒦_X ⟶ Q ⟶ 0 — for instance M = 𝒪_X(D) with Q = 𝒦_X / 𝒪_X(D) the sheaf of
principal parts — the long exact sequence collapses:
H¹(X, M)is the cokernel ofH⁰(X, 𝒦_X) ⟶ H⁰(X, Q);Hⁿ⁺²(X, M) ≅ Hⁿ⁺¹(X, Q)for everyn.
Once the divisorial sheaf, its principal-parts quotient, and the required short exact sequence are
supplied, this gives the principal-parts description of its cohomology on an integral curve:
vanishing of H²(X, 𝒪_X(D)) reduces to vanishing of H¹ of the sheaf of principal parts, and
H¹(X, 𝒪_X(D)) is the space of principal parts modulo those of global rational functions, which is
where the dimension counts behind Riemann–Roch take place.
Main declarations #
Scheme.Modules.subsingleton_cohomology_succ_of_isFlasqueandScheme.Modules.subsingleton_cohomologyOn_succ_of_isFlasque: a flasque sheaf of modules has vanishing cohomology in every positive degree, overXand over every open subset;- for a short exact sequence
0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0withM₂flasque:Scheme.Modules.cohomologyδ_surjective_of_isFlasque, the connecting mapHⁿ(X, M₃) ⟶ Hⁿ⁺¹(X, M₁)is surjective, andScheme.Modules.cohomologyδ_injective_of_isFlasque, it is injective in positive degrees;Scheme.Modules.cohomologySuccLinearEquivOfIsFlasquepackages the resulting isomorphismHⁿ⁺¹(X, M₃) ≃ₗ Hⁿ⁺²(X, M₁)over the base ring, andScheme.Modules.cohomologyOneLinearEquivOfIsFlasqueidentifiesH¹(X, M₁)with the cokernel ofH⁰(X, M₂) ⟶ H⁰(X, M₃).
No formalization is vendored. The acyclicity of flasque abelian sheaves is
TauCeti.Topology.subsingleton_H_succ_of_isFlasque, and flasqueness is Mathlib's
TopCat.Presheaf.IsFlasque.
References #
- R. Hartshorne, Algebraic Geometry, II, Exercise 1.16(a) (a constant sheaf on an irreducible space is flasque) and III, Proposition 2.5 (flasque sheaves are acyclic).
- J.-P. Serre, Algebraic Groups and Class Fields, Chapter II, §5 (the cohomology of
𝒪_X(D)on a curve through principal parts).
If the middle term of a short exact sequence of sheaves of modules is flasque, then every
connecting map H^{n₀}(X, M₃) ⟶ H^{n₁}(X, M₁) is surjective.
If the middle term of a short exact sequence of sheaves of modules is flasque, then the
connecting map Hⁿ⁺¹(X, M₃) ⟶ Hⁿ⁺²(X, M₁) is injective.
If the middle term of a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of sheaves of modules
on a scheme over R is flasque, the connecting map is an R-linear isomorphism
Hⁿ⁺¹(X, M₃) ≃ Hⁿ⁺²(X, M₁).
Equations
- One or more equations did not get rendered due to their size.
Instances For
If the middle term of a short exact sequence 0 ⟶ M₁ ⟶ M₂ ⟶ M₃ ⟶ 0 of sheaves of modules
on a scheme over R is flasque, the connecting map identifies H¹(X, M₁) with the cokernel of
H⁰(X, M₂) ⟶ H⁰(X, M₃), as R-modules.
Equations
- One or more equations did not get rendered due to their size.