First cohomology as principal parts modulo rational functions

For a Weil divisor D on an integral Noetherian scheme, suppose that the codimension-one points are closed and their local rings are discrete valuation rings. The principal-parts resolution

0 ⟶ 𝒪_X(D) ⟶ 𝒦_X ⟶ 𝒦_X / 𝒪_X(D) ⟶ 0

is then short exact, and the rational-function sheaf 𝒦_X is flasque. This file records the resulting concrete description

H¹(X, 𝒪_X(D)) ≃ Γ(X, 𝒦_X / 𝒪_X(D)) / im(Γ(X, 𝒦_X)).

Unlike the general short-exact-sequence result Scheme.Modules.cohomologyOneLinearEquivOfIsFlasque, the source here is expressed directly in global rational functions and global principal parts. This is the form used to pair cohomology classes with rational differentials by summing residues: a functional on principal parts descends to first cohomology precisely when it vanishes on the image of every global rational function.

Main declarations

• SchemeWeilDivisor.globalToPrincipalPartsBaseLinear sends a global rational function to its family of principal parts, as a map linear over the base ring;
• SchemeWeilDivisor.principalPartsBoundary is the connecting map from global principal parts to H¹(X, 𝒪_X(D));
• SchemeWeilDivisor.principalPartsQuotientEquivCohomologyOne is the displayed linear equivalence.

References

• J.-P. Serre, Algebraic Groups and Class Fields, Chapter II, §5.
• R. Hartshorne, Algebraic Geometry, Chapter III, Proposition 2.5 and Section 7.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.globalToPrincipalPartsBaseLinear (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (D : SchemeWeilDivisor X) : ↑((Scheme.rationalFunctions X).presheaf.obj (Opposite.op ⊤)) →ₗ[R] ↑(D.principalParts.presheaf.obj (Opposite.op ⊤))

The map from global rational functions to global principal parts of D, linear over the base ring of the scheme.

It is the degree-zero cohomology map of toPrincipalParts D, transported through the canonical identifications of zeroth cohomology with global sections.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.globalToPrincipalPartsBaseLinear_apply (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (D : SchemeWeilDivisor X) (f : ↑((Scheme.rationalFunctions X).presheaf.obj (Opposite.op ⊤))) : (globalToPrincipalPartsBaseLinear R D) f = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app D.toPrincipalParts ⊤)) f

globalToPrincipalPartsBaseLinear is the global-sections map induced by toPrincipalParts D.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsQuotientEquivCohomologyOne (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hclosed : ∀ (x : CodimensionOnePoint X), IsClosed {↑x}) (D : SchemeWeilDivisor X) : (↑(D.principalParts.presheaf.obj (Opposite.op ⊤)) ⧸ (globalToPrincipalPartsBaseLinear R D).range) ≃ₗ[R] Scheme.Modules.Cohomology D.sheaf 1

First cohomology as principal parts modulo rational functions. The first cohomology of 𝒪_X(D) is linearly equivalent to global principal parts modulo the principal parts of global rational functions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsBoundary (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hclosed : ∀ (x : CodimensionOnePoint X), IsClosed {↑x}) (D : SchemeWeilDivisor X) : ↑(D.principalParts.presheaf.obj (Opposite.op ⊤)) →ₗ[R] Scheme.Modules.Cohomology D.sheaf 1

The connecting map from global principal parts of D to H¹(X, 𝒪_X(D)).

It is surjective because the middle term 𝒦_X of the principal-parts resolution is flasque. Its kernel is the image of globalToPrincipalPartsBaseLinear.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsQuotientEquivCohomologyOne_mk (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hclosed : ∀ (x : CodimensionOnePoint X), IsClosed {↑x}) (D : SchemeWeilDivisor X) (p : ↑(D.principalParts.presheaf.obj (Opposite.op ⊤))) : (principalPartsQuotientEquivCohomologyOne R hclosed D) (Submodule.Quotient.mk p) = (principalPartsBoundary R hclosed D) p

The cohomology class of a family of principal parts is its image under the boundary map.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsBoundary_apply (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hclosed : ∀ (x : CodimensionOnePoint X), IsClosed {↑x}) (D : SchemeWeilDivisor X) (p : ↑(D.principalParts.presheaf.obj (Opposite.op ⊤))) : (principalPartsBoundary R hclosed D) p = (Scheme.Modules.cohomologyδ ⋯ 0 1 ⋯) ((AlgebraicGeometry.Scheme.Modules.cohomologyZeroBaseLinearEquiv R X D.principalParts).symm p)

The principal-parts boundary is the connecting map of the principal-parts short exact sequence, after identifying zeroth cohomology with global sections.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsBoundary_surjective (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hclosed : ∀ (x : CodimensionOnePoint X), IsClosed {↑x}) (D : SchemeWeilDivisor X) : Function.Surjective ⇑(principalPartsBoundary R hclosed D)

Every first-cohomology class of 𝒪_X(D) is represented by a global family of principal parts.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ker_principalPartsBoundary (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hclosed : ∀ (x : CodimensionOnePoint X), IsClosed {↑x}) (D : SchemeWeilDivisor X) : (principalPartsBoundary R hclosed D).ker = (globalToPrincipalPartsBaseLinear R D).range

The kernel of the principal-parts boundary is the image of global rational functions.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsBoundary_eq_zero_iff (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hclosed : ∀ (x : CodimensionOnePoint X), IsClosed {↑x}) (D : SchemeWeilDivisor X) (p : ↑(D.principalParts.presheaf.obj (Opposite.op ⊤))) : (principalPartsBoundary R hclosed D) p = 0 ↔ ∃ (f : ↑((Scheme.rationalFunctions X).presheaf.obj (Opposite.op ⊤))), (globalToPrincipalPartsBaseLinear R D) f = p

A family of global principal parts has zero boundary exactly when it is the family of principal parts of a global rational function.