Repartitions and scheme-theoretic principal parts

Let X be an integral Noetherian separated scheme over a field k. Assume that X → Spec(k) satisfies the existence part of the valuative criterion, every point has coheight at most one, the local rings at codimension-one points are discrete valuation rings, and the resulting codimension-one points are identified with the normalized places of its function field. A repartition of k(X) / k determines a finitely supported family of principal parts: at a point x, take the class of its entry at the corresponding place in k(X) / 𝒪_X(D)_x.

This file constructs that map and proves that it is surjective, with kernel the repartitions bounded by the function-field divisor corresponding to D. Thus global principal parts are the quotient of the repartition space by one step of its divisor filtration. This is the local comparison needed to identify first cohomology of 𝒪_X(D) with a repartition cokernel.

Main declarations

• SchemeWeilDivisor.repartitionToPrincipalParts: the linear map from repartitions to global principal parts;
• SchemeWeilDivisor.ker_repartitionToPrincipalParts: its kernel is the divisor filtration;
• SchemeWeilDivisor.repartitionToPrincipalParts_surjective: every finitely supported family of principal parts is represented by a repartition;
• SchemeWeilDivisor.adeleFiltrationQuotientEquivPrincipalParts: global principal parts are the quotient of the repartition space by the divisor filtration.

References

• J.-P. Serre, Algebraic Groups and Class Fields, Chapter II, Section 5.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.5.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.mem_stalkSubmodule_iff_valuation_le_exp {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [AlgebraicGeometry.IsLocallyNoetherian X] (D : SchemeWeilDivisor X) (x : CodimensionOnePoint X) (f : ↑X.functionField) : f ∈ D.stalkSubmodule x ↔ (X.toPlace ↑x).valuation f ≤ WithZero.exp (WeilDivisor.coeff D x)

Membership in the stalk of 𝒪_X(D) at x is the valuation bound imposed by D(x).

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionToPrincipalParts {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : ↥(repartitionSpace k ↑X.functionField) →ₗ[k] ↑(D.principalParts.presheaf.obj (Opposite.op ⊤))

A repartition determines a global family of principal parts by taking, at each codimension-one point, the class of its entry at the corresponding place.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionToPrincipalParts_apply {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) (a : ↥(repartitionSpace k ↑X.functionField)) (x : { x : CodimensionOnePoint X // ↑x ∈ ⊤ }) : ((D.principalPartsSectionsEquiv ⊤) ((repartitionToPrincipalParts hex hdim D) a)) x = Submodule.Quotient.mk (↑a (X.toPlace ↑↑x))

The principal part of a repartition at x is the class of its entry at the place attached to x.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ker_repartitionToPrincipalParts {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : (repartitionToPrincipalParts hex hdim D).ker = (adeleFiltration ((equivFunctionFieldDivisor hex hdim) D)).submoduleOf (repartitionSpace k ↑X.functionField)

The kernel of the repartition-to-principal-parts map is the step of the repartition filtration bounded by the corresponding function-field divisor.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.repartitionToPrincipalParts_surjective {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : Function.Surjective ⇑(repartitionToPrincipalParts hex hdim D)

Every global family of principal parts is represented by a repartition.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.adeleFiltrationQuotientEquivPrincipalParts {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : (↥(repartitionSpace k ↑X.functionField) ⧸ (adeleFiltration ((equivFunctionFieldDivisor hex hdim) D)).submoduleOf (repartitionSpace k ↑X.functionField)) ≃ₗ[k] ↑(D.principalParts.presheaf.obj (Opposite.op ⊤))

Global principal parts as a repartition quotient. The quotient of the repartition space by the repartitions bounded by D is linearly equivalent to the global principal parts of D.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.adeleFiltrationQuotientEquivPrincipalParts_mk {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) (a : ↥(repartitionSpace k ↑X.functionField)) : (adeleFiltrationQuotientEquivPrincipalParts hex hdim D) (Submodule.Quotient.mk a) = (repartitionToPrincipalParts hex hdim D) a

The repartition-quotient equivalence sends the class of a repartition to its family of principal parts.