Comparing Kähler and Weil differentials

Let F / k be an algebraic function field and let x ∈ F be a separating element. The embedding k(X) → F which sends X to x carries the normalized Weil differential dX of k(X) to a nonzero differential of F by cotrace. This differential, written TauCeti.weilDifferentialOfSeparating, is the Weil-theoretic dx.

Assume in addition that k is algebraically closed in F (IsIntegrallyClosedIn k F). Both the Kähler and Weil differential spaces are then one-dimensional over F. Sending the Kähler differential D k F x to this cotrace therefore determines an F-linear equivalence

Ω[F⁄k] ≃ₗ[F] weilDifferentialSpace k F.

For every y ∈ F, the equivalence sends dy to (dy/dx) dx. This is the linear comparison in Stichtenoth, Theorem 4.3.2. Compatibility with local components and residues, and independence from the separating parameter, remain to be proved.

The divisor of dx is explicit: (dx) = -2 (x)_∞ + Diff(F / k(x)) (Stichtenoth, Remark 4.3.7(c)). It is the divisor of a cotrace, Con (η) + Diff(F / k(x)), where the normalized differential η of k(x) has divisor -2 P_∞, and the conorm of P_∞ = (X)_∞ is the pole divisor of x. In particular -2 (x)_∞ + Diff(F / k(x)) is a canonical divisor of F.

Main definitions

• TauCeti.weilDifferentialOfSeparating: the cotrace of the normalized differential of k(X) along the embedding X ↦ x.
• TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating: the comparison equivalence determined by a separating element.

Main results

• TauCeti.weilDifferentialOfSeparating_ne_zero: dx is nonzero.
• TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating_D_self: the comparison sends dx to its Weil counterpart.
• TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating_D: the comparison sends dy to (dy/dx) dx.
• TauCeti.weilDifferentialDivisor_weilDifferentialOfSeparating: (dx) = -2 (x)_∞ + Diff(F / k(x)), and TauCeti.weilDifferentialDivisor_weilDifferentialCotrace_ratFuncWeilDifferential, the same identity for any finite separable extension of k(x).
• TauCeti.divisorClass_neg_two_zsmul_poles_add_different_eq_canonicalClass: -2 (x)_∞ + Diff(F / k(x)) represents the canonical class.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section IV.3, Definition 4.3.1, Theorem 4.3.2 and Remark 4.3.7.

noncomputable def TauCeti.weilDifferentialOfSeparating {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : ↥(weilDifferentialSpace k F)

The Weil differential dx attached to a separating element x: the cotrace to F of the normalized differential dX on the rational function field, along the embedding X ↦ x.

The result belongs to the intrinsic Weil differential space, so the chosen rational-function algebra structure used in its construction is not exposed in the type.

Equations

• TauCeti.weilDifferentialOfSeparating hF hx = (TauCeti.weilDifferentialCotrace k F ⋯ hF) ⟨TauCeti.ratFuncWeilDifferential k, ⋯⟩

theorem TauCeti.weilDifferentialOfSeparating_def {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : have x_1 := ⋯; have x_2 := ⋯; have x_3 := ⋯; weilDifferentialOfSeparating hF hx = (weilDifferentialCotrace k F ⋯ hF) ⟨ratFuncWeilDifferential k, ⋯⟩

The Weil differential attached to x is the cotrace of the normalized differential on k(X) under the rational-function algebra structure induced by X ↦ x.

theorem TauCeti.weilDifferentialOfSeparating_ne_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : weilDifferentialOfSeparating hF hx ≠ 0

The Weil differential dx attached to a separating element is nonzero.

noncomputable def TauCeti.weilDifferentialBasisOfSeparating {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : Module.Basis Unit F ↥(weilDifferentialSpace k F)

The basis of the Weil differential space whose unique vector is the differential dx attached to a separating element.

Equations

• TauCeti.weilDifferentialBasisOfSeparating hF hex hx = FiniteDimensional.basisSingleton Unit ⋯ (TauCeti.weilDifferentialOfSeparating hF hx) ⋯

@[simp]

theorem TauCeti.weilDifferentialBasisOfSeparating_apply {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (i : Unit) : (weilDifferentialBasisOfSeparating hF hex hx) i = weilDifferentialOfSeparating hF hx

noncomputable def TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : Ω[F⁄k] ≃ₗ[F] ↥(weilDifferentialSpace k F)

The Kähler–Weil differential comparison for a separating element (Stichtenoth, Theorem 4.3.2): the F-linear equivalence which sends the Kähler differential dx to the cotrace of the normalized Weil differential dX along k(X) → F, X ↦ x.

Equations

• TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx = (TauCeti.kaehlerBasisOfSeparating hx).equiv (TauCeti.weilDifferentialBasisOfSeparating hF hex hx) (Equiv.refl Unit)

@[simp]

theorem TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating_D_self {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx) ((KaehlerDifferential.D k F) x) = weilDifferentialOfSeparating hF hx

The Kähler–Weil comparison sends the differential of the chosen separating element to its Weil counterpart.

@[simp]

theorem TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating_symm_weilDifferentialOfSeparating {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx).symm (weilDifferentialOfSeparating hF hx) = (KaehlerDifferential.D k F) x

The inverse Kähler–Weil comparison sends the Weil differential attached to the chosen separating element back to its Kähler differential.

@[simp]

theorem TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating_D {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (y : F) : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx) ((KaehlerDifferential.D k F) y) = (derivativeOfSeparating hx) y • weilDifferentialOfSeparating hF hx

Under the Kähler–Weil comparison determined by x, the differential dy is (dy/dx) dx.

The divisor of dx

theorem TauCeti.weilDifferentialCotrace_ratFuncWeilDifferential_ne_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (hF : IsFunctionField k F) : ↑((weilDifferentialCotrace k F ⋯ hF) ⟨ratFuncWeilDifferential k, ⋯⟩) ≠ 0

The cotrace to F of the normalized differential of k(x) is nonzero.

@[simp]

theorem TauCeti.weilDifferentialDivisor_weilDifferentialCotrace_ratFuncWeilDifferential {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : weilDifferentialDivisor hF hex ⋯ ⋯ = -2 • Divisor.poles hF ((Units.map ↑(algebraMap (RatFunc k) F)) (Units.mk0 RatFunc.X ⋯)) + Divisor.different k F ⋯

The divisor of dx (Stichtenoth, Remark 4.3.7(c)): for a finite separable extension F of k(x) with exact constant field k, the cotrace to F of the normalized differential η of k(x) has divisor -2 (x)_∞ + Diff(F / k(x)), where x is the image in F of the variable of k(x).

@[simp]

theorem TauCeti.divisorClass_neg_two_zsmul_poles_add_different_eq_canonicalClass {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : -(2 • (Place.orderSystem hF).divisorClass (Divisor.poles hF ((Units.map ↑(algebraMap (RatFunc k) F)) (Units.mk0 RatFunc.X ⋯)))) + (Place.orderSystem hF).divisorClass (Divisor.different k F ⋯) = canonicalClass hF hex

-2 (x)_∞ + Diff(F / k(x)) is a canonical divisor (Stichtenoth, Remark 4.3.7(c)): for a finite separable extension F of k(x) with exact constant field k, this divisor represents the canonical class of F.

@[simp]

theorem TauCeti.weilDifferentialDivisor_weilDifferentialOfSeparating {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : weilDifferentialDivisor hF hex ⋯ ⋯ = -2 • Divisor.poles hF (Units.mk0 x ⋯) + Divisor.different k F ⋯

The divisor of dx (Stichtenoth, Remark 4.3.7(c)): for a separating element x of F / k with exact constant field k, the Weil differential dx has divisor -2 (x)_∞ + Diff(F / k(x)), the different being taken along the embedding k(X) → F, X ↦ x.