The genus drop under a constant field extension, place by place

Let F / k be an algebraic function field with exact constant field k, let k' / k be a finite extension and let F' = F · k' be the compositum, with [F' : F] = [k' : k], so that F and k' are linearly disjoint over k and F' = F ⊗_k k'. Suppose k' is the exact constant field of F'. Over an imperfect field k the genus can drop (TauCeti.genus_le_genus_of_constantCompositum_eq_top, TauCeti.GenusDrop.genus_lt_genus). This file locates the drop at finitely many places of F.

For a place P of F / k, the ring 𝒪_P ⊗_k k' is the k'-span 𝒪_P · k' of the valuation ring inside F' (TauCeti.Place.constantSpanIntegers). It is contained in the integral closure 𝒪'_P of 𝒪_P in F' (TauCeti.Place.integralClosureSubmodule), the functions regular at all places of F' over P. Geometrically, 𝒪_P ⊗_k k' is the semilocal ring of the base-changed curve along the fiber over P, which may consist of several points, and 𝒪'_P is its normalization. Their quotient has finite k'-dimension, the singularity degree

δ_P = dim_{k'} (𝒪'_P ⧸ 𝒪_P ⊗_k k')

(TauCeti.Place.singularityDegree), which vanishes at all but finitely many places, and

g(F / k) = g(F' / k') + ∑_P δ_P.

So the genus drops exactly when 𝒪_P ⊗_k k' fails to be integrally closed at some place.

The proof compares Riemann–Roch spaces. For a nonspecial divisor E of large degree, write elements of F' in an F-basis of constants. Clearing the pole allowed by E at a place P gives a k'-linear map from L(Con E) to the quotient 𝒪'_P ⧸ 𝒪_P ⊗_k k'. On finitely many places these maps are jointly surjective, since A_F(E) + F is every repartition of F. Their common kernel contains L(E) · k', of dimension ℓ(E), with equality once every place outside the chosen finite set is regular. Riemann's theorem in F and in F' evaluates ℓ(Con E) - ℓ(E) = g(F / k) - g(F' / k').

This is the δ-invariant formula for the genus change under inseparable base extension. Tate's theorem refines it: for a purely inseparable k' / k of degree p, the drop is divisible by (p - 1) / 2.

When the genus does not drop, every place has δ_P = 0, so the integral-basis argument of the separable case applies at every place: L(Con D) = L(D) · k' and ℓ(Con D) = ℓ(D) for every divisor D of F. With the preservation of degrees, the conorm then carries the canonical class to the canonical class and is injective on divisor classes, as for a separable extension of constants. This applies to the function field of a smooth curve (TauCeti.AlgebraicGeometry.dim_conorm_of_smooth).

Main definitions

The rings 𝒪_P · k' and 𝒪'_P come from TauCeti.FieldTheory.FunctionField.ConstantExtension.IntegralBasis.

• TauCeti.Place.singularityQuotient: the quotient 𝒪'_P ⧸ 𝒪_P · k'.
• TauCeti.Place.singularityDegree: its k'-dimension δ_P.

Main results

• TauCeti.Place.finiteDimensional_singularityQuotient: 𝒪'_P ⧸ 𝒪_P · k' is finite-dimensional.
• TauCeti.Place.singularityDegree_eq_zero_iff: when 𝒪'_P ⧸ 𝒪_P · k' is finite-dimensional, δ_P = 0 exactly when 𝒪_P · k' is integrally closed in F'.
• TauCeti.finite_setOf_singularityDegree_ne_zero: δ_P = 0 at all but finitely many places.
• TauCeti.genus_eq_genus_add_finsum_singularityDegree: g(F / k) = g(F' / k') + ∑_P δ_P.
• TauCeti.genus_eq_genus_iff_forall_constantSpanIntegers_eq: the genus is unchanged exactly when 𝒪_P · k' is integrally closed at every place.
• TauCeti.riemannRochSpace_conorm_eq_span_of_forall_constantSpanIntegers_eq and TauCeti.Divisor.dim_conorm_of_forall_constantSpanIntegers_eq: for a finite constant field extension F' = F · k' with [F' : F] = [k' : k], if 𝒪_P · k' is integrally closed at every place, then L(Con D) = L(D) · k' and ℓ(Con D) = ℓ(D).
• TauCeti.riemannRochSpace_conorm_eq_span_of_genus_eq, TauCeti.Divisor.dim_conorm_of_genus_eq, TauCeti.conormClassGroup_canonicalClass_of_genus_eq and TauCeti.conormClassGroup_injective_of_genus_eq: when the genus does not drop, the conorm preserves Riemann–Roch spaces and the canonical class and is injective on divisor classes (Stichtenoth, Theorem 3.6.3(d)–(f), without separability of k' / k).

References

• J. Tate, Genus change in inseparable extensions of function fields, Proc. Amer. Math. Soc. 3 (1952), 400–406.
• S. Schröer, On genus change in algebraic curves over imperfect fields, Proc. Amer. Math. Soc. 137 (2009), 1239–1243, for the genus drop as a sum of δ-invariants.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.5 and III.6.

@[reducible, inline]

abbrev TauCeti.Place.singularityQuotient {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P : Place k F) [Algebra.IsIntegral k k'] : Type v'

The quotient 𝒪'_P ⧸ 𝒪_P · k', which measures how far 𝒪_P ⊗_k k' is from being integrally closed in F'.

noncomputable def TauCeti.Place.singularityDegree {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P : Place k F) [Algebra.IsIntegral k k'] : ℕ

The singularity degree δ_P = dim_{k'} (𝒪'_P ⧸ 𝒪_P · k') of P in F' = F · k': the total k'-dimensional normalization defect along the fiber over P of the curve of F / k after extending the constants to k'. The fiber may consist of several points, and δ_P sums their contributions. It is finite (TauCeti.Place.finiteDimensional_singularityQuotient), and the genus drops by the sum of the singularity degrees (TauCeti.genus_eq_genus_add_finsum_singularityDegree).

theorem TauCeti.Place.singularityDegree_def {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P : Place k F) [Algebra.IsIntegral k k'] : singularityDegree k' F' P = Module.finrank k' (singularityQuotient k' F' P)

theorem TauCeti.Place.singularityDegree_eq_zero_iff {k : Type u} (k' : Type u') {F : Type v} (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P : Place k F) [Algebra.IsIntegral k k'] [FiniteDimensional k' (singularityQuotient k' F' P)] : singularityDegree k' F' P = 0 ↔ constantSpanIntegers k' F' P = integralClosureSubmodule k' F' P

A place has singularity degree zero exactly when 𝒪_P · k' is integrally closed: when 𝒪'_P ⧸ 𝒪_P · k' is finite-dimensional, δ_P = 0 if and only if 𝒪_P ⊗_k k' is the integral closure of 𝒪_P in F'. The finiteness holds at every place in the setting of the genus drop (TauCeti.Place.finiteDimensional_singularityQuotient).

The local comparison

The genus drop

theorem TauCeti.Place.finiteDimensional_singularityQuotient {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (hex' : IsIntegrallyClosedIn k' F') (hn : Module.finrank F F' = Module.finrank k k') (P : Place k F) : FiniteDimensional k' (singularityQuotient k' F' P)

The singularity quotient is finite-dimensional: 𝒪'_P ⧸ 𝒪_P · k' has finite k'-dimension at every place P of F / k.

theorem TauCeti.finite_setOf_singularityDegree_ne_zero {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (hex' : IsIntegrallyClosedIn k' F') (hn : Module.finrank F F' = Module.finrank k k') : {P : Place k F | Place.singularityDegree k' F' P ≠ 0}.Finite

The singularity degree vanishes at almost every place: only finitely many places P of F / k have 𝒪_P ⊗_k k' not integrally closed in F'.

theorem TauCeti.genus_eq_genus_add_finsum_singularityDegree {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (hex' : IsIntegrallyClosedIn k' F') (hn : Module.finrank F F' = Module.finrank k k') : genus k F = genus k' F' + ∑ᶠ (P : Place k F), Place.singularityDegree k' F' P

The genus drop is the sum of the singularity degrees: if k is the exact constant field of F, k' the exact constant field of F' = F · k' and [F' : F] = [k' : k], then

g(F / k) = g(F' / k') + ∑_P δ_P,

where δ_P = dim_{k'} (𝒪'_P ⧸ 𝒪_P ⊗_k k') vanishes at all but finitely many places.

theorem TauCeti.genus_eq_genus_iff_forall_constantSpanIntegers_eq {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (hex' : IsIntegrallyClosedIn k' F') (hn : Module.finrank F F' = Module.finrank k k') : genus k' F' = genus k F ↔ ∀ (P : Place k F), Place.constantSpanIntegers k' F' P = Place.integralClosureSubmodule k' F' P

The genus is unchanged exactly when no place becomes singular: g(F' / k') = g(F / k) if and only if 𝒪_P ⊗_k k' is integrally closed in F' at every place P of F / k.

Constant field extensions without genus drop

theorem TauCeti.riemannRochSpace_conorm_eq_span_of_forall_constantSpanIntegers_eq {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] [FiniteDimensional F F'] (h : constantCompositum F k' F' = ⊤) (hn : Module.finrank F F' = Module.finrank k k') (hF' : IsFunctionField k' F') (hreg : ∀ (P : Place k F), Place.constantSpanIntegers k' F' P = Place.integralClosureSubmodule k' F' P) (D : Divisor k F) : riemannRochSpace ((Divisor.conorm k' F') D) = Submodule.span k' (⇑(algebraMap F F') '' ↑(riemannRochSpace D))

L(Con D) when no place becomes singular: for a finite constant field extension F' = F · k' with [F' : F] = [k' : k], if 𝒪_P ⊗_k k' is integrally closed in F' at every place P of F / k, then for every divisor D of F / k the Riemann–Roch space L(Con D) is the k'-span of the image of L(D). Neither separability of k' / k nor exactness of the constants is assumed.

theorem TauCeti.Divisor.dim_conorm_of_forall_constantSpanIntegers_eq {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] [FiniteDimensional F F'] (h : constantCompositum F k' F' = ⊤) (hn : Module.finrank F F' = Module.finrank k k') (hF : IsFunctionField k F) (hreg : ∀ (P : Place k F), Place.constantSpanIntegers k' F' P = Place.integralClosureSubmodule k' F' P) (D : Divisor k F) : ((conorm k' F') D).dim = D.dim

ℓ(Con D) = ℓ(D) when no place becomes singular: for a finite constant field extension F' = F · k' with [F' : F] = [k' : k], if 𝒪_P ⊗_k k' is integrally closed in F' at every place P of F / k, then the conorm of every divisor D of F / k has the dimension of D. Neither separability of k' / k nor exactness of the constants is assumed.

theorem TauCeti.riemannRochSpace_conorm_eq_span_of_genus_eq {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] [FiniteDimensional F F'] (h : constantCompositum F k' F' = ⊤) (hn : Module.finrank F F' = Module.finrank k k') (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') (hg : genus k' F' = genus k F) (D : Divisor k F) : riemannRochSpace ((Divisor.conorm k' F') D) = Submodule.span k' (⇑(algebraMap F F') '' ↑(riemannRochSpace D))

L(Con D) when the genus does not drop: if k is the exact constant field of F, k' that of F' = F · k', [F' : F] = [k' : k] and g(F' / k') = g(F / k), then for every divisor D of F / k the Riemann–Roch space L(Con D) is the k'-span of the image of L(D) (Stichtenoth, Theorem 3.6.3(d), without separability of k' / k).

theorem TauCeti.Divisor.dim_conorm_of_genus_eq {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] [FiniteDimensional F F'] (h : constantCompositum F k' F' = ⊤) (hn : Module.finrank F F' = Module.finrank k k') (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') (hg : genus k' F' = genus k F) (D : Divisor k F) : ((conorm k' F') D).dim = D.dim

ℓ(Con D) = ℓ(D) when the genus does not drop: under a finite constant field extension F' = F · k' with exact constants on both sides, [F' : F] = [k' : k] and g(F' / k') = g(F / k), the conorm of every divisor D of F / k has the dimension of D.

theorem TauCeti.conormClassGroup_canonicalClass_of_genus_eq {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] [FiniteDimensional F F'] (h : constantCompositum F k' F' = ⊤) (hn : Module.finrank F F' = Module.finrank k k') (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') (hg : genus k' F' = genus k F) : (Divisor.conormClassGroup k' F' hF ⋯) (canonicalClass hF hex) = canonicalClass ⋯ hex'

The conorm of the canonical class is the canonical class when the genus does not drop (Stichtenoth, Theorem 3.6.3(e), without separability of k' / k): under a finite constant field extension F' = F · k' with exact constants on both sides, [F' : F] = [k' : k] and g(F' / k') = g(F / k), the conorm on divisor classes sends the canonical class of F / k to the canonical class of F' / k'.

theorem TauCeti.conormClassGroup_injective_of_genus_eq {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] [FiniteDimensional F F'] (h : constantCompositum F k' F' = ⊤) (hn : Module.finrank F F' = Module.finrank k k') (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') (hg : genus k' F' = genus k F) : Function.Injective ⇑(Divisor.conormClassGroup k' F' hF ⋯)

The conorm is injective on divisor classes when the genus does not drop (Stichtenoth, Theorem 3.6.3(f), without separability of k' / k): under a finite constant field extension F' = F · k' with exact constants on both sides, [F' : F] = [k' : k] and g(F' / k') = g(F / k), a divisor of F / k whose conorm is principal is itself principal.