Divisors on a scheme of dimension at most one and divisors of its function field

Let X be a separated integral scheme over a field k, of dimension at most one. If every codimension-one local ring is a discrete valuation ring and the structure morphism satisfies the existence part of the valuative criterion, codimension-one points of X are equivalent to normalized places of k(X). Reindexing finite formal sums along this equivalence identifies scheme-theoretic Weil divisors with divisors of the function field.

This file records the characteristic properties of that identification. It preserves point divisors, coefficientwise order and effectivity, the residue-degree-weighted degree, and principal divisors. Consequently it also preserves linear equivalence. These comparisons allow the scheme-theoretic divisor and principal-parts constructions to use the function-field divisor API.

On global sections, a section of the divisor sheaf 𝒪_X(D) is a rational function whose order at every codimension-one point x is at least -D(x), which is exactly membership in the Riemann–Roch space L(D) of the corresponding function-field divisor. Hence H⁰(X, 𝒪_X(D)) = L(D).

Main declarations

• SchemeWeilDivisor.equivFunctionFieldDivisor: the additive equivalence between divisors on X and divisors of k(X);
• SchemeWeilDivisor.degree_equivFunctionFieldDivisor: compatibility with divisor degree;
• SchemeWeilDivisor.equivFunctionFieldDivisor_principalDivisor: compatibility with principal divisors;
• SchemeWeilDivisor.linearlyEquivalent_equivFunctionFieldDivisor_iff: compatibility with linear equivalence;
• SchemeWeilDivisor.globalSectionsEquivRiemannRochSpace: Γ(X, 𝒪_X(D)) ≃ L(D);
• SchemeWeilDivisor.finrank_cohomology_zero_sheaf_eq_dim: dim_k H⁰(X, 𝒪_X(D)) = ℓ(D).

References

• R. Hartshorne, Algebraic Geometry, Chapter I, Section 6, and Chapter II, Section 6.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.4.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) : SchemeWeilDivisor X ≃+ Divisor k ↑X.functionField

Reindex scheme-theoretic Weil divisors along the equivalence between codimension-one points and normalized places of the function field.

Equations

• TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor hex hdim = Finsupp.domCongr (TauCeti.AlgebraicGeometry.CodimensionOnePoint.equivPlace hex hdim)

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.coeff_equivFunctionFieldDivisor {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) (P : Place k ↑X.functionField) : WeilDivisor.coeff ((equivFunctionFieldDivisor hex hdim) D) P = WeilDivisor.coeff D ((CodimensionOnePoint.equivPlace hex hdim).symm P)

The coefficient after reindexing is the coefficient at the corresponding codimension-one point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.coeff_equivFunctionFieldDivisor_toPlace {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) (x : CodimensionOnePoint X) : WeilDivisor.coeff ((equivFunctionFieldDivisor hex hdim) D) (X.toPlace ↑x) = WeilDivisor.coeff D x

The coefficient at the place attached to x is the coefficient at x.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.coeff_equivFunctionFieldDivisor_symm {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : Divisor k ↑X.functionField) (x : CodimensionOnePoint X) : WeilDivisor.coeff ((equivFunctionFieldDivisor hex hdim).symm D) x = WeilDivisor.coeff D (X.toPlace ↑x)

Pulling a function-field divisor back to the curve preserves the coefficient at each codimension-one point.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_ofPoint {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (x : CodimensionOnePoint X) : (equivFunctionFieldDivisor hex hdim) (WeilDivisor.ofPoint x) = WeilDivisor.ofPoint (X.toPlace ↑x)

Reindexing sends the prime divisor at a codimension-one point to the divisor of its place.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_symm_ofPoint {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (P : Place k ↑X.functionField) : (equivFunctionFieldDivisor hex hdim).symm (WeilDivisor.ofPoint P) = WeilDivisor.ofPoint ((CodimensionOnePoint.equivPlace hex hdim).symm P)

Pulling back a prime function-field divisor gives the prime divisor at the corresponding codimension-one point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_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)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : (equivFunctionFieldDivisor hex hdim) D = (WeilDivisor.pushforward fun (x : CodimensionOnePoint X) => X.toPlace ↑x) D

The divisor equivalence is the formal pushforward along the point-to-place map.

@[simp]

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

Reindexing along the point-to-place equivalence preserves coefficientwise inequalities.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_symm_le_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) {D E : Divisor k ↑X.functionField} : (equivFunctionFieldDivisor hex hdim).symm D ≤ (equivFunctionFieldDivisor hex hdim).symm E ↔ D ≤ E

Pulling back along the point-to-place equivalence preserves coefficientwise inequalities.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isEffective_equivFunctionFieldDivisor_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) {D : SchemeWeilDivisor X} : WeilDivisor.IsEffective ((equivFunctionFieldDivisor hex hdim) D) ↔ WeilDivisor.IsEffective D

Reindexing along the point-to-place equivalence preserves effectivity.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isEffective_equivFunctionFieldDivisor_symm_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) {D : Divisor k ↑X.functionField} : WeilDivisor.IsEffective ((equivFunctionFieldDivisor hex hdim).symm D) ↔ WeilDivisor.IsEffective D

Pulling a function-field divisor back to the curve preserves effectivity.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.degree_equivFunctionFieldDivisor {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : Divisor.degree ((equivFunctionFieldDivisor hex hdim) D) = (relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D

The function-field degree of a reindexed divisor is its scheme-theoretic relative degree.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_equivFunctionFieldDivisor_symm {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : Divisor k ↑X.functionField) : (relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) ((equivFunctionFieldDivisor hex hdim).symm D) = Divisor.degree D

The scheme-theoretic degree of a pulled-back function-field divisor is its function-field degree.

Global sections and Riemann–Roch spaces

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.nonemptyTopOpensFunctionField {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : Nonempty ↥↑⊤

The top open of an integral scheme is nonempty.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionsEquiv_symm_mem_sections_top_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsLocallyNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) (f : ↑X.functionField) : (Scheme.rationalFunctionsEquiv ⊤).symm f ∈ D.sections ⊤ ↔ f ∈ riemannRochSpace ((equivFunctionFieldDivisor hex hdim) D)

A rational function is a global section of 𝒪_X(D) exactly when it lies in the Riemann–Roch space of the corresponding function-field divisor.

Not @[simp]: the simp lemma SchemeWeilDivisor.mem_sections already rewrites the left-hand side, and k, hex and hdim do not occur in it, so simp could not instantiate them.

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

Global sections of 𝒪_X(D) form the Riemann–Roch space L(D). A global section of the sheaf of a Weil divisor D is a rational function f with ord_x f ≥ -D(x) at every codimension-one point x, and the map to the function field identifies these with the Riemann–Roch space of the function-field divisor corresponding to D.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.coe_globalSectionsEquivRiemannRochSpace_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)] [X.IsSeparated] [AlgebraicGeometry.IsLocallyNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) (s : ↑(D.sheaf.presheaf.obj (Opposite.op ⊤))) : ↑((globalSectionsEquivRiemannRochSpace hex hdim D) s) = (Scheme.rationalFunctionsEquiv ⊤) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app D.sheafι ⊤)) s)

The Riemann–Roch space element attached to a global section of 𝒪_X(D) is its underlying rational function.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_zero_sheaf_eq_dim {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsLocallyNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : Module.finrank k (Scheme.Modules.Cohomology D.sheaf 0) = ((equivFunctionFieldDivisor hex hdim) D).dim

dim_k H⁰(X, 𝒪_X(D)) = ℓ(D): the dimension of the zeroth cohomology of 𝒪_X(D) is the dimension of the Riemann–Roch space of the corresponding function-field divisor.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_principalHom {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : IsFunctionField k ↑X.functionField) : (equivFunctionFieldDivisor hex hdim).toAddMonoidHom.comp (WeilDivisor.OrderSystem.ofScheme X).principalHom = (Place.orderSystem hF).principalHom

The point-to-place divisor equivalence intertwines the two order systems.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_principalDivisor {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : IsFunctionField k ↑X.functionField) (g : Additive (↑X.functionField)ˣ) : (equivFunctionFieldDivisor hex hdim) ((WeilDivisor.OrderSystem.ofScheme X).principalDivisor g) = (Place.orderSystem hF).principalDivisor g

Scheme-theoretic principal divisors become the corresponding place-order principal divisors under the point-to-place equivalence.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_symm_principalDivisor {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : IsFunctionField k ↑X.functionField) (g : Additive (↑X.functionField)ˣ) : (equivFunctionFieldDivisor hex hdim).symm ((Place.orderSystem hF).principalDivisor g) = (WeilDivisor.OrderSystem.ofScheme X).principalDivisor g

Pulling back a place-order principal divisor gives the corresponding scheme-theoretic principal divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_principal {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : IsFunctionField k ↑X.functionField) (z : (↑X.functionField)ˣ) : (equivFunctionFieldDivisor hex hdim) ((WeilDivisor.OrderSystem.ofScheme X).principalDivisor (Additive.ofMul z)) = Divisor.principal hF z

Scheme-theoretic principal divisors become function-field principal divisors under the point-to-place equivalence.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFunctionFieldDivisor_symm_principal {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : IsFunctionField k ↑X.functionField) (z : (↑X.functionField)ˣ) : (equivFunctionFieldDivisor hex hdim).symm (Divisor.principal hF z) = (WeilDivisor.OrderSystem.ofScheme X).principalDivisor (Additive.ofMul z)

Pulling back a function-field principal divisor gives the corresponding scheme-theoretic principal divisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.linearlyEquivalent_equivFunctionFieldDivisor_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] [AlgebraicGeometry.IsNoetherian X] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (hF : IsFunctionField k ↑X.functionField) {D E : SchemeWeilDivisor X} : (Place.orderSystem hF).LinearlyEquivalent ((equivFunctionFieldDivisor hex hdim) D) ((equivFunctionFieldDivisor hex hdim) E) ↔ (WeilDivisor.OrderSystem.ofScheme X).LinearlyEquivalent D E

Linear equivalence of scheme divisors is exactly linear equivalence of the corresponding function-field divisors.