Regular Kähler differentials at places

At a place P whose residue field is separable over k, a separating uniformizer t identifies the image of Ω[𝒪_P⁄k] → Ω[F⁄k] with 𝒪_P dt, because differentiation with respect to t preserves 𝒪_P. In particular, regularity can be checked on the coefficient in the basis dt, without assuming that the map from local differentials is injective.

The trace residue pairing against 𝒪_P detects integrality of that coefficient. Since the Kähler–Weil comparison is independent of the separating element over any exact constant field, local components of Weil differentials are trace residues, so this lattice is exactly the annihilator of 𝒪_P under the local component. For nonzero differentials it is therefore exactly the nonnegative-order lattice of Weil differentials. Over a perfect constant field every residue field is separable and every prime element is separating, so this holds at places of every degree. This is the local comparison needed to identify the differential sheaf on a smooth curve with a canonical divisor sheaf.

Without perfectness the comparison still holds at every smooth place, that is, wherever Ω[𝒪_P⁄k] is free of rank one over 𝒪_P, even when the residue field is inseparable over k. There Ω[𝒪_P⁄k] is generated by a single differential dz with z ∈ 𝒪_P, so differentiation by z preserves 𝒪_P, and 𝒪_P is formally unramified over the valuation ring of k(z). The different exponent of P over k(z) therefore vanishes, so dz has order zero at P, and both lattices are 𝒪_P dz.

At rational places the trace residue is the residue, and the comparison is also stated through the residue of Kähler differentials.

Main results

• TauCeti.Place.mem_range_map_iff_coord_mem_integers_of_derivativeOfSeparating_mem: the coefficient criterion whenever differentiation by a separating element regular at P preserves the valuation ring.

• TauCeti.Place.mem_range_map_iff_coord_mem_integers: a differential comes from 𝒪_P exactly when its coefficient in dt is integral.

• TauCeti.Place.coord_mem_integers_iff_forall_traceResidue_coord_smul_eq_zero: that coefficient is integral exactly when the trace residues of u ω / dt vanish for all integral u.

• TauCeti.Place.mem_range_map_iff_weilDifferentialOrder_nonneg: over a perfect exact constant field, a nonzero Weil differential has nonnegative order at a place of any degree exactly when the corresponding Kähler differential comes from the valuation ring.

• TauCeti.Place.mem_range_map_iff_weilDifferentialOrder_nonneg_of_finrank_eq_one: the same comparison over any exact constant field with a separating element, at a place where Ω[𝒪_P⁄k] is free of rank one, with TauCeti.Place.mem_range_map_iff_weilDifferentialOrder_nonneg_of_span_D_eq_top its form for a given generator dz.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Sections I.7 and IV.2–3, and Remark 4.3.7(d).
• R. Hartshorne, Algebraic Geometry, II, Section 8, and IV, Section 1.

The Kähler–Weil comparison and its residue formula are those of kaehlerDifferentialEquivWeilDifferentialOfSeparating, repartitionDualComponent_kaehlerDifferentialEquivWeilDifferentialOfSeparating and Place.traceResidue_coord_smul_eq_repartitionDualComponent.

theorem TauCeti.Place.mem_range_map_iff_coord_mem_integers_of_derivativeOfSeparating_mem {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (htP : t ∈ P.integers) (hD : ∀ z ∈ P.integers, (derivativeOfSeparating htr) z ∈ P.integers) (ω : Ω[F⁄k]) : ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ ((kaehlerBasisOfSeparating htr).coord ()) ω ∈ P.integers

If differentiation by a separating element t regular at P preserves the valuation ring of P, then a Kähler differential comes from that valuation ring exactly when its coefficient in the basis dt is integral there.

theorem TauCeti.Place.mem_range_map_iff_coord_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] [Algebra.IsSeparable k P.ResidueField] (ω : Ω[F⁄k]) : ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ ((kaehlerBasisOfSeparating htr).coord ()) ω ∈ P.integers

A Kähler differential of F comes from the valuation ring of a place with separable residue field exactly when its coefficient in the basis given by a separating uniformizer is integral there.

theorem TauCeti.Place.coord_mem_integers_iff_forall_traceResidue_coord_smul_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] [FiniteDimensional k P.ResidueField] [Algebra.IsSeparable k P.ResidueField] (ω : Ω[F⁄k]) : ((kaehlerBasisOfSeparating htr).coord ()) ω ∈ P.integers ↔ ∀ u ∈ P.integers, (P.traceResidue ht) (((kaehlerBasisOfSeparating htr).coord ()) (u • ω)) = 0

At a place with separable residue field, the trace residue pairing against integral functions detects whether the coefficient of a Kähler differential in a separating-uniformizer basis is integral.

theorem TauCeti.Place.coord_mem_integers_iff_forall_kaehlerResidue_smul_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (ω : Ω[F⁄k]) : ((kaehlerBasisOfSeparating htr).coord ()) ω ∈ P.integers ↔ ∀ u ∈ P.integers, (P.kaehlerResidue hP ht htr) (u • ω) = 0

The residue pairing against integral functions detects whether the coefficient of a rational differential in a separating-uniformizer basis is integral.

theorem TauCeti.Place.mem_range_map_iff_forall_repartitionDualComponent_eq_zero_of_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (ω : Ω[F⁄k]) : ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ ∀ u ∈ P.integers, (repartitionDualComponent (↑((kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx) ω)) P) u = 0

Under the Kähler–Weil comparison, the image of local Kähler differentials at a rational place is precisely the annihilator of its valuation ring for the local component.

theorem TauCeti.Place.mem_range_map_iff_weilDifferentialOrder_nonneg_of_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (ω : ↥(weilDifferentialSpace k F)) (hω : ↑ω ≠ 0) : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx).symm ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ 0 ≤ weilDifferentialOrder hF hex ⋯ hω P

Given a separating uniformizer at a rational place, a nonzero Weil differential has nonnegative order exactly when its corresponding Kähler differential comes from the valuation ring. The constant field need not be perfect.

theorem TauCeti.Place.mem_range_map_iff_weilDifferentialOrder_nonneg_of_span_D_eq_top {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 : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] {z : F} (hzP : z ∈ P.integers) (hΩ : ↥P.integers ∙ (KaehlerDifferential.D k ↥P.integers) ⟨z, hzP⟩ = ⊤) (ω : ↥(weilDifferentialSpace k F)) (hω : ↑ω ≠ 0) : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx).symm ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ 0 ≤ weilDifferentialOrder hF hex ⋯ hω P

Regular differentials at a place where one differential generates: let F / k have exact constant field and a separating element, and let P be a place at which Ω[𝒪_P⁄k] is generated by the differential d z of some z ∈ 𝒪_P. Then a nonzero Weil differential has nonnegative order at P exactly when the corresponding Kähler differential comes from 𝒪_P. The constant field need not be perfect, and the residue field of P need not be separable.

theorem TauCeti.Place.mem_range_map_iff_weilDifferentialOrder_nonneg_of_finrank_eq_one {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 : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] [Module.Free ↥P.integers Ω[↥P.integers⁄k]] (hP : Module.finrank ↥P.integers Ω[↥P.integers⁄k] = 1) (ω : ↥(weilDifferentialSpace k F)) (hω : ↑ω ≠ 0) : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx).symm ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ 0 ≤ weilDifferentialOrder hF hex ⋯ hω P

Regular differentials at a smooth place: let F / k have exact constant field and a separating element, and let P be a place at which Ω[𝒪_P⁄k] is free of rank one over 𝒪_P. Then a nonzero Weil differential has nonnegative order at P exactly when the corresponding Kähler differential comes from 𝒪_P. The constant field need not be perfect, and the residue field of P need not be separable.

theorem TauCeti.Place.mem_range_map_iff_forall_kaehlerResidueOfPerfectField_smul_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (P : Place k F) (hP : P.degree = 1) (hF : IsFunctionField k F) (ω : Ω[F⁄k]) : ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ ∀ u ∈ P.integers, (P.kaehlerResidueOfPerfectField hP hF) (u • ω) = 0

Over a perfect field, a Kähler differential comes from the valuation ring of a rational place exactly when its residue pairing with every integral function vanishes. No uniformizer is part of the statement.

theorem TauCeti.Place.mem_range_map_iff_forall_repartitionDualComponent_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (P : Place k F) (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (ω : Ω[F⁄k]) : ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ ∀ u ∈ P.integers, (repartitionDualComponent (↑((kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx) ω)) P) u = 0

Over a perfect exact constant field, the image of local Kähler differentials at a place of any degree is the annihilator of its valuation ring for the local component of the Kähler–Weil comparison, without choosing a uniformizer.

theorem TauCeti.Place.mem_range_map_iff_weilDifferentialOrder_nonneg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (P : Place k F) (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] (ω : ↥(weilDifferentialSpace k F)) (hω : ↑ω ≠ 0) : (kaehlerDifferentialEquivWeilDifferentialOfSeparating hF hex hx).symm ω ∈ (KaehlerDifferential.map k k (↥P.integers) F).range ↔ 0 ≤ weilDifferentialOrder hF hex ⋯ hω P

Over a perfect exact constant field, a nonzero Weil differential has nonnegative order at a place of any degree exactly when its corresponding Kähler differential comes from that place's valuation ring. No uniformizer is part of the statement.