The genus under a constant field extension

Let F' = F · k' be a finite separable constant field extension of an algebraic function field F / k with exact constant field k. The conorm Con : Div(F) → Div(F') preserves degrees, and — since it also preserves the dimensions of Riemann–Roch spaces — the genus of F' / k' is the genus of F / k. Consequently the conorm carries the canonical class to the canonical class and is injective on divisor classes.

Exactness of k' in F' is not needed for the degree and genus identities; it is assumed only where the canonical class of F' / k' is spoken of.

Main results

• 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).
• 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.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6, Theorem 3.6.3(b), (c), (e) and (f).

@[simp]

theorem TauCeti.Divisor.degree_conorm_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 F F'] [Algebra.IsSeparable k k'] (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) (D : Divisor k F) : degree ((conorm k' F') D) = degree D

The conorm along a constant field extension preserves degrees (Stichtenoth, Theorem 3.6.3(c)): for a finite separable constant field extension F · k' / k' of F / k with exact constant field k, deg (Con D) = deg D for every divisor D of F / k. No function-field hypothesis on F / k is needed.

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'] [FiniteDimensional 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 finite separable constant field extension (Stichtenoth, Theorem 3.6.3(b)): if k is the exact constant field of F, then g(F · k' / k') = g(F / k). Exactness of k' in F · k' is not assumed.

@[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'] [FiniteDimensional F F'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') (h : constantCompositum F k' F' = ⊤) : (Divisor.conormClassGroup k' F' hF ⋯) (canonicalClass hF hex) = canonicalClass ⋯ hex'

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

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'] [FiniteDimensional F F'] [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 finite separable constant field extension of a function field with exact constant field, two divisors with the same conorm class lie in the same class; equivalently, a divisor whose conorm is principal is itself principal.