The chain rule, independence of the Kähler–Weil comparison, and the residue theorem

Let F / k be an algebraic function field with exact constants, and let x and y be separating elements. The Weil differentials dx and dy (TauCeti.weilDifferentialOfSeparating) are the cotraces of the canonical differential of the rational function field along X ↦ x and X ↦ y. They satisfy the chain rule

dy = (dy/dx) · dx,

where dy/dx is the derivative of Kähler differentials (TauCeti.derivativeOfSeparating). This is Stichtenoth's Theorem 4.3.2(a), δ(y) = (dy/dx) · δ(x). Stichtenoth assumes a perfect constant field; here the chain rule holds over every exact constant field.

The proof compares one local component. At a rational place P where x - a and y - b are both prime elements, the local components are residues (TauCeti.repartitionDualComponent_weilDifferentialOfSeparating): (dy)_P (u) = res_{P,y-b} (u) and (dx)_P (u) = res_{P,x-a} (u). The transformation formula (TauCeti.Place.residue_eq_residue_mul_derivativeOfSeparating) rewrites the first as res_{P,x-a} (u · dy/dx), which is the local component of (dy/dx) · dx. Over an exact constant field one local component determines a Weil differential (TauCeti.repartitionDualComponent_inj).

F need not have such a rational place, but it has infinitely many places whose residue field is separable over k (TauCeti.Place.infinite_setOf_isSeparable_residueField), even over an imperfect field. At all but finitely many of them, x and y are units and some q(x) and r(y) are prime elements (TauCeti.Place.finite_setOf_forall_irreducible_ord_aeval_ne_one), where q and r are separable since the values of x and y are (TauCeti.Place.separable_of_ord_aeval_pos). A finite separable constant field extension makes the places above such a place rational (TauCeti.Place.exists_constantCompositum_eq_top_and_forall_degree_eq_one), without ramification, so there x - a and y - b are prime elements, and the chain rule holds after extending the constants. The cotrace to the extension is injective and carries dx and dy to their counterparts (TauCeti.weilDifferentialCotrace_weilDifferentialOfSeparating), while the algebra map carries dy/dx to its counterpart (TauCeti.derivativeOfSeparating_algebraMap), so the chain rule descends.

Consequently the Kähler–Weil comparison TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating does not depend on the separating element used to build it, and the local components of the Weil differential attached to a Kähler differential ω are its residues. At a place P with separable residue field and a separating prime element t, writing u ω = z dt, the local component at u is the trace residue Tr_{F_P/k} res_{P,t} (z), the form of Stichtenoth's Theorem 4.3.2(d) for places of arbitrary degree (Remark 4.3.7(d)). At rational places it reads ω_P (u) = res_P (u ω). Over a perfect constant field every residue field is separable and every prime element separating.

These are the trace-residue formulas for Weil differentials of TauCeti.FieldTheory.FunctionField.Differential.TraceResidue read through the comparison, which preserves coordinates (TauCeti.coord_kaehlerDifferentialEquivWeilDifferentialOfSeparating). The residue theorem with trace residues for Weil differentials (TauCeti.finsum_traceResidue_coord_eq_zero) thereby becomes the residue theorem for Kähler differentials over a perfect field: the trace residues of ω at all places sum to zero (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)). Over an algebraically closed field every place is rational and this is ∑_P res_P (ω) = 0.

Main results

• TauCeti.weilDifferentialOfSeparating_eq_derivativeOfSeparating_smul_of_ord_eq_one: dy = (dy/dx) · dx, given a rational place at which x - a and y - b are prime elements.
• TauCeti.weilDifferentialOfSeparating_eq_derivativeOfSeparating_smul: the chain rule dy = (dy/dx) · dx over any exact constant field.
• TauCeti.Place.ord_derivativeOfSeparating_eq_sub: ord_P (dy/dx) = v_P(dy) - v_P(dx) at every place.
• TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating_eq: the Kähler–Weil comparison is independent of the separating element.
• TauCeti.Place.traceResidue_coord_smul_eq_repartitionDualComponent: local components are trace residues at a place of any degree with separable residue field.
• TauCeti.repartitionDualComponent_kaehlerDifferentialEquivWeilDifferentialOfSeparating: local components are residues, ω_P (u) = res_P (u ω), at rational places.
• TauCeti.Place.kaehlerResidueOfPerfectField_smul_eq_repartitionDualComponent: the same over a perfect field, with the uniformizer-free residue.
• TauCeti.Place.kaehlerResidue_eq_traceResidue_coord and TauCeti.Place.kaehlerResidueOfPerfectField_eq_traceResidue_coord: at a rational place the residue of a Kähler differential is its trace residue.
• TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero: the residue theorem over a perfect field, ∑_P Tr_{F_P/k} res_{P,t_P} (ω / dt_P) = 0 for prime elements t_P, a sum with finitely many nonzero terms (TauCeti.finite_support_traceResidue_kaehlerBasisOfSeparating_coord).
• TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero: the residue theorem ∑_P res_P (ω) = 0 over an algebraically closed field, a sum with finitely many nonzero terms (TauCeti.finite_support_kaehlerResidueOfPerfectField).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 4.3.2, Corollary 4.3.3 and Remark 4.3.7.

theorem TauCeti.weilDifferentialOfSeparating_eq_derivativeOfSeparating_smul_of_ord_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x y : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (hy : Transcendental k y) [Algebra.IsSeparable (↥k⟮y⟯) F] {P : Place k F} (hP : P.degree = 1) {a b : k} (hxa : P.ord (x - (algebraMap k F) a) = 1) (hyb : P.ord (y - (algebraMap k F) b) = 1) : weilDifferentialOfSeparating hF hy = (derivativeOfSeparating hx) y • weilDifferentialOfSeparating hF hx

The chain rule for Weil differentials, at a common rational place (Stichtenoth, Theorem 4.3.2(a)): if x - a and y - b are prime elements at the same rational place, then the Weil differentials of the separating elements x and y satisfy dy = (dy/dx) · dx.

theorem TauCeti.weilDifferentialOfSeparating_eq_derivativeOfSeparating_smul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x y : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (hy : Transcendental k y) [Algebra.IsSeparable (↥k⟮y⟯) F] : weilDifferentialOfSeparating hF hy = (derivativeOfSeparating hx) y • weilDifferentialOfSeparating hF hx

The chain rule for Weil differentials (Stichtenoth, Theorem 4.3.2(a)): over any exact constant field, the Weil differentials of any two separating elements x and y satisfy dy = (dy/dx) · dx. Stichtenoth assumes k perfect; here k is arbitrary, and F need not have any rational place.

theorem TauCeti.Place.ord_derivativeOfSeparating_eq_sub {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x y : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (hy : Transcendental k y) [Algebra.IsSeparable (↥k⟮y⟯) F] : P.ord ((derivativeOfSeparating hx) y) = weilDifferentialOrder hF hex ⋯ ⋯ P - weilDifferentialOrder hF hex ⋯ ⋯ P

The order of a derivative is a difference of orders of differentials: over an exact constant field, for separating elements x and y and any place P, ord_P (dy/dx) = v_P(dy) - v_P(dx). This is the chain rule dy = (dy/dx) · dx read at P.

theorem TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x y : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (hy : Transcendental k y) [Algebra.IsSeparable (↥k⟮y⟯) F] : kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx = kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hy

The Kähler–Weil comparison does not depend on the separating element (Stichtenoth, Theorem 4.3.2): over any exact constant field, the comparisons built from any two separating elements are equal.

Local components are residues

theorem TauCeti.Place.traceResidue_coord_smul_eq_repartitionDualComponent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] {P : Place k F} [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (ω : Ω[F⁄k]) (u : F) : (P.traceResidue ht) (((kaehlerBasisOfSeparating htr).coord ()) (u • ω)) = (repartitionDualComponent (↑((kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx) ω)) P) u

Local components are trace residues (Stichtenoth, Theorem 4.3.2(d) and Remark 4.3.7(d)): over an exact constant field, let P be a place of any degree whose residue field is separable over k, and t a separating prime element of P. For a Kähler differential ω, the trace residue Tr_{F_P/k} res_{P,t} (u ω / dt) is the local component at P, evaluated at u, of the Weil differential attached to ω by the Kähler–Weil comparison, built from any separating element x. No further condition on the constant field is needed.

theorem TauCeti.Place.kaehlerResidue_eq_traceResidue_coord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} (hP : P.degree = 1) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (ω : Ω[F⁄k]) : (P.kaehlerResidue hP ht htr) ω = (P.traceResidue ht) (((kaehlerBasisOfSeparating htr).coord ()) ω)

At a rational place, the residue res_P (ω) of a Kähler differential computed with a separating prime element t is the trace residue Tr_{F_P/k} res_{P,t} (ω / dt), the trace from F_P = k being the identity.

theorem TauCeti.repartitionDualComponent_kaehlerDifferentialEquivWeilDifferentialOfSeparating {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] {P : Place k F} (hP : P.degree = 1) {t : F} (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (ω : Ω[F⁄k]) (u : F) : (repartitionDualComponent (↑((kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx) ω)) P) u = (P.kaehlerResidue hP ht htr) (u • ω)

Local components are residues (Stichtenoth, Theorem 4.3.2(d)): over an exact constant field, let ω be a Kähler differential and P a rational place with a separating prime element t. The local component at P of the Weil differential attached to ω by the Kähler–Weil comparison is u ↦ res_P (u ω). Over a perfect constant field every prime element is separating, and the residue does not depend on it (TauCeti.Place.kaehlerResidueOfPerfectField_smul_eq_repartitionDualComponent).

theorem TauCeti.Place.kaehlerResidueOfPerfectField_eq_traceResidue_coord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) {P : Place k F} (hP : P.degree = 1) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (ω : Ω[F⁄k]) : (P.kaehlerResidueOfPerfectField hP hF) ω = (P.traceResidue ht) (((kaehlerBasisOfSeparating htr).coord ()) ω)

Over a perfect field, the residue res_P (ω) of a Kähler differential at a rational place P is the trace residue Tr_{F_P/k} res_{P,t} (ω / dt) for every prime element t of P.

theorem TauCeti.Place.kaehlerResidueOfPerfectField_smul_eq_repartitionDualComponent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] {P : Place k F} (hP : P.degree = 1) (ω : Ω[F⁄k]) (u : F) : (P.kaehlerResidueOfPerfectField hP hF) (u • ω) = (repartitionDualComponent (↑((kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx) ω)) P) u

Local components are residues, over a perfect field (Stichtenoth, Theorem 4.3.2(d)): over a perfect exact constant field, the residue res_P (u ω) of a Kähler differential at a rational place P is the local component at P of the Weil differential attached to ω, evaluated at u. Every prime element of P is separating here, so no uniformizer is needed.

theorem TauCeti.finite_support_traceResidue_kaehlerBasisOfSeparating_coord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) [∀ (P : Place k F), Algebra.IsSeparable k P.ResidueField] (t : Place k F → F) (ht : ∀ (P : Place k F), P.ord (t P) = 1) [∀ (P : Place k F), Algebra.IsSeparable (↥k⟮t P⟯) F] (ω : Ω[F⁄k]) : have htr := ⋯; (Function.support fun (P : Place k F) => (P.traceResidue ⋯) (((kaehlerBasisOfSeparating ⋯).coord ()) ω)).Finite

The trace residues Tr_{F_P/k} res_{P,t_P} (ω / dt_P) of a Kähler differential, computed with a prime element t_P at each place P, vanish at all but finitely many places. The separability of each residue field over k (TauCeti.Place.isSeparable_residueField_of_perfectField) and of F over each k(t_P) (TauCeti.Place.transcendental_and_isSeparable_adjoin_of_ord_eq_one) holds automatically over a perfect field; it is assumed only so that the trace residues and the coordinates in dt_P can be stated. This is TauCeti.finite_support_traceResidue_coord for the Weil differential attached to ω, on the constant repartition 1.

theorem TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) [∀ (P : Place k F), Algebra.IsSeparable k P.ResidueField] (t : Place k F → F) (ht : ∀ (P : Place k F), P.ord (t P) = 1) [∀ (P : Place k F), Algebra.IsSeparable (↥k⟮t P⟯) F] (ω : Ω[F⁄k]) : have htr := ⋯; ∑ᶠ (P : Place k F), (P.traceResidue ⋯) (((kaehlerBasisOfSeparating ⋯).coord ()) ω) = 0

The residue theorem for trace residues (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)): over an exact constant field, choose a prime element t_P at each place P, with the residue fields and F / k(t_P) separable (automatic over a perfect field). Then the trace residues of a Kähler differential ω sum to zero, ∑_P Tr_{F_P/k} res_{P,t_P} (ω / dt_P) = 0, a sum with finitely many nonzero terms (TauCeti.finite_support_traceResidue_kaehlerBasisOfSeparating_coord). This is the residue theorem for Weil differentials TauCeti.finsum_traceResidue_coord_eq_zero at u = 1, applied to the Weil differential attached to ω. Unlike TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero, places of every degree contribute, so this applies over finite fields.

theorem TauCeti.finite_support_kaehlerResidueOfPerfectField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [IsAlgClosed k] (hF : IsFunctionField k F) (ω : Ω[F⁄k]) : (Function.support fun (P : Place k F) => (P.kaehlerResidueOfPerfectField ⋯ hF) ω).Finite

Over an algebraically closed field, a Kähler differential has nonzero residue at only finitely many places.

theorem TauCeti.finsum_kaehlerResidueOfPerfectField_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [IsAlgClosed k] (hF : IsFunctionField k F) (ω : Ω[F⁄k]) : ∑ᶠ (P : Place k F), (P.kaehlerResidueOfPerfectField ⋯ hF) ω = 0

The residue theorem (Stichtenoth, Corollary 4.3.3): over an algebraically closed field, the residues of a Kähler differential ω at the places of F sum to zero, ∑_P res_P (ω) = 0. Every place is rational here, and only finitely many residues are nonzero (TauCeti.finite_support_kaehlerResidueOfPerfectField).

Over a field that is not algebraically closed the rational places do not suffice: over ℚ, the differential 2x / (x² - 2) dx of ℚ(x) has residue zero at every rational place x = a and residue -2 at infinity; the missing residue sits at the place of x² - 2, which is not rational (see TauCeti.finsum_residue_adicOfIrreducible_X_sub_C). Over a perfect field the trace residues at the places of every degree sum to zero (TauCeti.finsum_traceResidue_kaehlerBasisOfSeparating_coord_eq_zero).