Weil divisors, the Picard group, and Pic⁰ of the two-chart model

Let F / k be an algebraic function field over an arbitrary field k, and let X_F = TauCeti.AlgebraicGeometry.twoChartModel hF hx be its regular proper curve over k built from an element x ∈ F transcendental over k. Because the codimension-one points of X_F are in canonical bijection with the normalized places of F / k (twoChartModel.equivPlace), reindexing identifies scheme-theoretic Weil divisors on X_F with function-field divisors on F.

This file establishes the complete divisor- and class-group dictionary between X_F and F / k, with no assumption on the constant field k:

• twoChartModel.equivDivisor: the order-preserving additive equivalence SchemeWeilDivisor X_F ≃+ Divisor k F, compatible with coefficients, prime divisors, and effectivity;
• twoChartModel.degree_equivDivisor and twoChartModel.relativeDegree_equivDivisor_symm: the residue-degree-weighted degree on X_F agrees with the place-degree-weighted degree on F;
• twoChartModel.equivDivisor_principal, twoChartModel.equivDivisor_symm_principal, and twoChartModel.linearlyEquivalent_equivDivisor_iff: principal divisors on X_F correspond to principal divisors of F under k(X_F) ≃ₐ[k] F, so linear equivalence is preserved;
• twoChartModel.classGroupEquiv and twoChartModel.picardEquivClassGroup: the induced isomorphisms Cl(X_F) ≃+ Cl(F) and Pic(X_F) ≃+ Cl(F), intertwining the Euler-characteristic degree on Pic(X_F) with Divisor.degreeClass (twoChartModel.degreeClass_picardEquivClassGroup);
• twoChartModel.picZeroEquivDegreeZeroClassGroup: the restricted isomorphism Pic⁰(X_F) ≃+ Cl⁰(F) between the degree-zero Picard group of X_F and the degree-zero divisor class group of F.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section II.6 and Section IV.1.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.4 and Appendix B.

Reindexing Weil divisors along equivPlace

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : SchemeWeilDivisor (twoChartModel hF hx) ≃+ Divisor k F

Weil divisors on the two-chart model are divisors of F / k: reindexing along twoChartModel.equivPlace identifies SchemeWeilDivisor (twoChartModel hF hx) with Divisor k F.

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_eq_domCongr {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : equivDivisor hxt = Finsupp.domCongr (equivPlace hxt)

equivDivisor is reindexing along equivPlace.

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_eq_trans {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : equivDivisor hxt = (SchemeWeilDivisor.equivFunctionFieldDivisor ⋯ ⋯).trans (Finsupp.domCongr (Place.mapEquiv (functionFieldEquiv hxt)))

equivDivisor factors as SchemeWeilDivisor.equivFunctionFieldDivisor followed by divisor transport along functionFieldEquiv.

theorem TauCeti.AlgebraicGeometry.twoChartModel.domCongr_equivOfRingEquiv_equivFunctionFieldDivisor {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : SchemeWeilDivisor (twoChartModel hF hx)) : (Finsupp.domCongr (Place.equivOfRingEquiv (RingEquiv.refl k) (functionFieldEquiv hxt).toRingEquiv ⋯)) ((SchemeWeilDivisor.equivFunctionFieldDivisor ⋯ ⋯) D) = (equivDivisor hxt) D

Transporting SchemeWeilDivisor.equivFunctionFieldDivisor along functionFieldEquiv gives equivDivisor.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.coeff_equivDivisor {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : SchemeWeilDivisor (twoChartModel hF hx)) (P : Place k F) : WeilDivisor.coeff ((equivDivisor hxt) D) P = WeilDivisor.coeff D ((equivPlace hxt).symm P)

The coefficient of equivDivisor hxt D at a place P is the coefficient of D at the corresponding codimension-one point of X_F.

theorem TauCeti.AlgebraicGeometry.twoChartModel.coeff_equivDivisor_equivPlace {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : SchemeWeilDivisor (twoChartModel hF hx)) (p : CodimensionOnePoint (twoChartModel hF hx)) : WeilDivisor.coeff ((equivDivisor hxt) D) ((equivPlace hxt) p) = WeilDivisor.coeff D p

The coefficient of equivDivisor hxt D at the place of p is the coefficient of D at p.

Not @[simp]: coeff_equivDivisor already simplifies the left-hand side.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.coeff_equivDivisor_symm {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : Divisor k F) (p : CodimensionOnePoint (twoChartModel hF hx)) : WeilDivisor.coeff ((equivDivisor hxt).symm D) p = WeilDivisor.coeff D ((equivPlace hxt) p)

Pulling a divisor of F back to X_F reads its coefficient at p at equivPlace hxt p.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_ofPoint {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (p : CodimensionOnePoint (twoChartModel hF hx)) : (equivDivisor hxt) (WeilDivisor.ofPoint p) = WeilDivisor.ofPoint ((equivPlace hxt) p)

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

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_symm_ofPoint {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (P : Place k F) : (equivDivisor hxt).symm (WeilDivisor.ofPoint P) = WeilDivisor.ofPoint ((equivPlace hxt).symm P)

Pulling back a prime divisor of F gives the prime divisor at the corresponding point of X_F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_le_iff {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) {D E : SchemeWeilDivisor (twoChartModel hF hx)} : (equivDivisor hxt) D ≤ (equivDivisor hxt) E ↔ D ≤ E

equivDivisor preserves coefficientwise inequalities.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_symm_le_iff {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) {D E : Divisor k F} : (equivDivisor hxt).symm D ≤ (equivDivisor hxt).symm E ↔ D ≤ E

(equivDivisor hxt).symm preserves coefficientwise inequalities.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_nonneg_iff {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) {D : SchemeWeilDivisor (twoChartModel hF hx)} : 0 ≤ (equivDivisor hxt) D ↔ 0 ≤ D

equivDivisor preserves effective divisors.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_symm_nonneg_iff {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) {D : Divisor k F} : 0 ≤ (equivDivisor hxt).symm D ↔ 0 ≤ D

(equivDivisor hxt).symm preserves effective divisors.

Degrees, principal divisors, and linear equivalence

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.degree_equivDivisor {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : SchemeWeilDivisor (twoChartModel hF hx)) : Divisor.degree ((equivDivisor hxt) D) = (SchemeWeilDivisor.relativeDegree (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k)) D

Degree comparison: the function-field degree of equivDivisor hxt D equals the residue-degree-weighted degree of D on X_F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.relativeDegree_equivDivisor_symm {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : Divisor k F) : (SchemeWeilDivisor.relativeDegree (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k)) ((equivDivisor hxt).symm D) = Divisor.degree D

The scheme-theoretic degree of (equivDivisor hxt).symm D equals the function-field degree of D.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_principal {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (z : (↑(twoChartModel hF hx).functionField)ˣ) : (equivDivisor hxt) ((WeilDivisor.OrderSystem.ofScheme (twoChartModel hF hx)).principalDivisor (Additive.ofMul z)) = Divisor.principal hF ((Units.map (functionFieldEquiv hxt).toRingEquiv.toMulEquiv.toMonoidHom) z)

Principal divisors on X_F become principal divisors of F under equivDivisor and functionFieldEquiv.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivDivisor_symm_principal {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (z : Fˣ) : (equivDivisor hxt).symm (Divisor.principal hF z) = (WeilDivisor.OrderSystem.ofScheme (twoChartModel hF hx)).principalDivisor (Additive.ofMul ((Units.map (functionFieldEquiv hxt).symm.toRingEquiv.toMulEquiv.toMonoidHom) z))

Pulling back the principal divisor of z ∈ Fˣ gives the scheme-theoretic principal divisor of its preimage in k(X_F)ˣ.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.linearlyEquivalent_equivDivisor_iff {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) {D E : SchemeWeilDivisor (twoChartModel hF hx)} : (Place.orderSystem hF).LinearlyEquivalent ((equivDivisor hxt) D) ((equivDivisor hxt) E) ↔ (WeilDivisor.OrderSystem.ofScheme (twoChartModel hF hx)).LinearlyEquivalent D E

Linear equivalence on X_F is linear equivalence in F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.linearlyEquivalent_equivDivisor_symm_iff {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) {D E : Divisor k F} : (WeilDivisor.OrderSystem.ofScheme (twoChartModel hF hx)).LinearlyEquivalent ((equivDivisor hxt).symm D) ((equivDivisor hxt).symm E) ↔ (Place.orderSystem hF).LinearlyEquivalent D E

Pulling back divisors along equivDivisor preserves and reflects linear equivalence.

The divisor class group, the Picard group, and Pic⁰

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.classGroupEquiv {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : (WeilDivisor.OrderSystem.ofScheme (twoChartModel hF hx)).ClassGroup ≃+ (Place.orderSystem hF).ClassGroup

The divisor class group of X_F is the divisor class group of F: Cl(X_F) ≃+ Cl(F).

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.classGroupEquiv_divisorClass {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : SchemeWeilDivisor (twoChartModel hF hx)) : (classGroupEquiv hxt) ((WeilDivisor.OrderSystem.ofScheme (twoChartModel hF hx)).divisorClass D) = (Place.orderSystem hF).divisorClass ((equivDivisor hxt) D)

classGroupEquiv sends [D] on X_F to [equivDivisor hxt D] on F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.classGroupEquiv_symm_divisorClass {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (E : Divisor k F) : (classGroupEquiv hxt).symm ((Place.orderSystem hF).divisorClass E) = (WeilDivisor.OrderSystem.ofScheme (twoChartModel hF hx)).divisorClass ((equivDivisor hxt).symm E)

(classGroupEquiv hxt).symm sends [E] on F to [(equivDivisor hxt).symm E] on X_F.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.picardEquivClassGroup {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : Additive (LineBundleClass (twoChartModel hF hx)) ≃+ (Place.orderSystem hF).ClassGroup

The Picard group of X_F is the divisor class group of F: Pic(X_F) ≃+ Cl(F), sending [𝒪_{X_F}(D)] to [equivDivisor hxt D].

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.picardEquivClassGroup_toLineBundleClass {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (D : SchemeWeilDivisor (twoChartModel hF hx)) : (picardEquivClassGroup hxt) (Additive.ofMul (SchemeWeilDivisor.toLineBundleClass ⋯ D)) = (Place.orderSystem hF).divisorClass ((equivDivisor hxt) D)

picardEquivClassGroup sends the line-bundle class [𝒪_{X_F}(D)] to the divisor class of equivDivisor hxt D.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.picardEquivClassGroup_symm_divisorClass {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (E : Divisor k F) : (picardEquivClassGroup hxt).symm ((Place.orderSystem hF).divisorClass E) = Additive.ofMul (SchemeWeilDivisor.toLineBundleClass ⋯ ((equivDivisor hxt).symm E))

(picardEquivClassGroup hxt).symm sends the divisor class of E in Cl(F) to the line-bundle class [𝒪_{X_F}((equivDivisor hxt).symm E)].

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.degreeClass_picardEquivClassGroup {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (a : Additive (LineBundleClass (twoChartModel hF hx))) : (Divisor.degreeClass hF) ((picardEquivClassGroup hxt) a) = LineBundleClass.eulerDegree k (Additive.toMul a)

Pic(X_F) ≃+ Cl(F) intertwines the Euler-characteristic degree with divisor degree.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.eulerDegree_picardEquivClassGroup_symm {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (c : (Place.orderSystem hF).ClassGroup) : LineBundleClass.eulerDegree k (Additive.toMul ((picardEquivClassGroup hxt).symm c)) = (Divisor.degreeClass hF) c

(picardEquivClassGroup hxt).symm sends a divisor class of degree d to a line-bundle class of Euler-characteristic degree d.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.picZeroEquivDegreeZeroClassGroup {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : ↥(LineBundleClass.picZero k (twoChartModel hF hx)) ≃+ ↥(Divisor.degreeClass hF).ker

Pic⁰ of the two-chart model is the degree-zero divisor class group of F: Pic⁰(X_F) ≃+ Cl⁰(F), obtained by restricting picardEquivClassGroup.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.coe_picZeroEquivDegreeZeroClassGroup_apply {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (a : ↥(LineBundleClass.picZero k (twoChartModel hF hx))) : ↑((picZeroEquivDegreeZeroClassGroup hxt) a) = (picardEquivClassGroup hxt) ↑a

picZeroEquivDegreeZeroClassGroup is the restriction of picardEquivClassGroup.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.coe_picZeroEquivDegreeZeroClassGroup_symm_apply {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (c : ↥(Divisor.degreeClass hF).ker) : ↑((picZeroEquivDegreeZeroClassGroup hxt).symm c) = (picardEquivClassGroup hxt).symm ↑c

(picZeroEquivDegreeZeroClassGroup hxt).symm is the restriction of (picardEquivClassGroup hxt).symm.