The genus under a constant field extension

Let F' = F · k' be a separable algebraic constant field extension of an algebraic function field F / k with exact constant field k. The genus of F' / k' is the genus of F / k, also when k' / k is infinite, for instance an algebraic closure of a perfect k. Riemann's theorem reads the genus off the multiples l B of the pole divisor B of a transcendental x ∈ F: their degrees l [F : k(x)] and their dimensions do not change in F' (TauCeti.Divisor.dim_nsmul_poles_of_constantCompositum_eq_top), and every divisor of F' is linearly equivalent to one below some l B.

The conorm Con : Div(F) → Div(F') preserves degrees and the dimensions of Riemann–Roch spaces, so it carries the canonical class to the canonical class and is injective on divisor classes, including when the separable algebraic constant extension is infinite.

Exactness of k' in F' is not needed for the degree and genus identities; where the canonical class of F' / k' is spoken of, it follows from exactness of k in F (IsIntegrallyClosedIn.of_constantCompositum_eq_top).

The genus never increases under any algebraic extension of constants, including inseparable and infinite extensions. For a finite extension the conorm comparison also gives [k' : k] (g(F' / k') - 1) ≤ [F' : F] (g(F / k) - 1). Without separability the genus inequality can be strict (TauCeti.GenusDrop.genus_lt_genus).

Main results

• TauCeti.finrank_mul_genus_sub_one_le_of_constantCompositum_eq_top: [k' : k] (g(F' / k') - 1) ≤ [F' : F] (g(F / k) - 1) for any finite k' / k.
• TauCeti.genus_le_genus_of_constantCompositum_eq_top: g(F' / k') ≤ g(F / k) for any algebraic k' / k, finite or not, separable or not.
• TauCeti.Divisor.degree_conorm_of_constantCompositum_eq_top: deg (Con D) = deg D.
• TauCeti.genus_eq_genus_of_constantCompositum_eq_top: g(F' / k') = g(F / k) for a separable algebraic k' / k, finite or not.
• TauCeti.conormClassGroup_canonicalClass_of_forall_dim_conorm_eq and TauCeti.conormClassGroup_injective_of_forall_dim_conorm_eq: a conorm preserving degrees and Riemann–Roch dimensions, along an extension that preserves the genus, carries the canonical class to the canonical class; one preserving degrees and dimensions is injective on divisor classes.
• TauCeti.conormClassGroup_canonicalClass_of_constantCompositum_eq_top: the conorm of the canonical class is the canonical class.
• TauCeti.conormClassGroup_injective_of_constantCompositum_eq_top: the conorm is injective on divisor classes.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6, Theorem 3.6.3(b), (c), (e) and (f).
• J. Tate, Genus change in inseparable extensions of function fields, Proc. Amer. Math. Soc. 3 (1952), 400–406, for the genus change under inseparable constant field extensions.

The genus never increases

theorem TauCeti.finrank_mul_genus_sub_one_le_of_constantCompositum_eq_top {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) (h : constantCompositum F k' F' = ⊤) : ↑(Module.finrank k k') * (↑(genus k' F') - 1) ≤ ↑(Module.finrank F F') * (↑(genus k F) - 1)

The genus cannot grow under a finite constant field extension, in quantitative form: if F' = F · k' for a finite extension k' / k, then

[k' : k] (g(F' / k') - 1) ≤ [F' : F] (g(F / k) - 1).

No separability of k' / k is assumed, nor exactness of k in F or of k' in F'. Since [F' : F] ≤ [k' : k], this gives g(F' / k') ≤ g(F / k) (TauCeti.genus_le_genus_of_constantCompositum_eq_top). For a separable k' / k over an exact constant field the two degrees agree and the genus is unchanged (TauCeti.genus_eq_genus_of_constantCompositum_eq_top); an inseparable k' / k can make it drop (TauCeti.GenusDrop.genus_lt_genus).

theorem TauCeti.genus_le_genus_of_constantCompositum_eq_top {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'] [Algebra.IsAlgebraic k k'] (hF : IsFunctionField k F) (h : constantCompositum F k' F' = ⊤) : genus k' F' ≤ genus k F

The genus never increases under an algebraic constant field extension: if F' = F · k' for an algebraic extension k' / k, finite or not, then g(F' / k') ≤ g(F / k). No separability or exactness hypothesis is needed. The inequality is strict for some inseparable extensions (TauCeti.GenusDrop.genus_lt_genus), and an equality for separable ones over an exact constant field (TauCeti.genus_eq_genus_of_constantCompositum_eq_top). For an algebraic closure k' of k, it bounds the genus of F · k' / k' by that of F / k.

The genus under separable algebraic constant field extensions

theorem TauCeti.genus_eq_genus_of_constantCompositum_eq_top {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'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) : genus k' F' = genus k F

The genus is unchanged by a separable algebraic constant field extension (Stichtenoth, Theorem 3.6.3(b)): if k is the exact constant field of F and F' = F · k' for a separable algebraic extension k' / k, finite or not, then g(F' / k') = g(F / k). Exactness of k' in F' is not assumed. Over a perfect k this applies to an algebraic closure of k.

Divisor classes under conorms preserving degrees and dimensions

theorem TauCeti.conormClassGroup_canonicalClass_of_forall_dim_conorm_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'] [Algebra.IsIntegral F F'] [∀ (P : Place k F), Finite { P' : Place k' F' // Place.restrict k F P' = P }] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hdeg : ∀ (D : Divisor k F), Divisor.degree ((Divisor.conorm k' F') D) = Divisor.degree D) (hdim : ∀ (D : Divisor k F), ((Divisor.conorm k' F') D).dim = D.dim) (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') : (Divisor.conormClassGroup k' F' hF hF') (canonicalClass hF hex) = canonicalClass hF' hex'

The conorm of the canonical class is the canonical class when the conorm preserves the degrees and Riemann–Roch dimensions of all divisors (the genus then does not change): the canonical class is the class of degree 2g - 2 and dimension g.

theorem TauCeti.conormClassGroup_injective_of_forall_dim_conorm_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'] [Algebra.IsIntegral F F'] [∀ (P : Place k F), Finite { P' : Place k' F' // Place.restrict k F P' = P }] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hdeg : ∀ (D : Divisor k F), Divisor.degree ((Divisor.conorm k' F') D) = Divisor.degree D) (hdim : ∀ (D : Divisor k F), ((Divisor.conorm k' F') D).dim = D.dim) : Function.Injective ⇑(Divisor.conormClassGroup k' F' hF hF')

The conorm is injective on divisor classes when it preserves the degrees and Riemann–Roch dimensions of all divisors: a divisor of degree zero whose conorm is principal has a nonzero Riemann–Roch space, so it is itself principal.

Divisor classes under separable algebraic constant field extensions

@[simp]

theorem TauCeti.conormClassGroup_canonicalClass_of_constantCompositum_eq_top {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'] [Algebra.IsIntegral F F'] [∀ (P : Place k F), Finite { P' : Place k' F' // Place.restrict k F P' = P }] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) : (Divisor.conormClassGroup k' F' hF ⋯) (canonicalClass hF hex) = canonicalClass ⋯ ⋯

The conorm of the canonical class is the canonical class (Stichtenoth, Theorem 3.6.3(e)): for a separable algebraic constant field extension F · k' / k' of F / k with exact constant field k, the conorm on divisor classes sends the canonical class of F / k to the canonical class of F · k' / k', whose constant field k' is exact as well.

theorem TauCeti.conormClassGroup_injective_of_constantCompositum_eq_top {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'] [Algebra.IsIntegral F F'] [∀ (P : Place k F), Finite { P' : Place k' F' // Place.restrict k F P' = P }] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) : Function.Injective ⇑(Divisor.conormClassGroup k' F' hF ⋯)

The conorm is injective on divisor classes (Stichtenoth, Theorem 3.6.3(f)): along a separable algebraic constant field extension of a function field with exact constants, two divisors with the same conorm class lie in the same class; equivalently, a divisor whose conorm is principal is itself principal.