Divisor degrees under algebraic extension of constants #
For a function field with exact constants, conorm along a separable algebraic constant extension preserves divisor degrees, even when the extension is infinite. Each place is unramified and the degrees of its finitely many extensions sum to its degree. Additivity then gives the identity for every divisor. Together with preservation of Riemann–Roch dimensions, this identifies canonical classes and detects principal divisors after extending constants.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Theorem 3.6.3(c).
@[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']
[Algebra.IsIntegral F F']
[Algebra.IsSeparable k k']
[∀ (P : Place k F), Finite { P' : Place k' F' // Place.restrict k F P' = P }]
(hF : IsFunctionField k F)
(hex : IsIntegrallyClosedIn k F)
(h : constantCompositum F k' F' = ⊤)
(D : Divisor k F)
:
Conorm preserves degrees under separable algebraic extension of exact constants
(Stichtenoth, Theorem 3.6.3(c)). The constant extension may be infinite; finiteness of its
place fibres is supplied by
Place.finite_setOf_restrict_eq_of_constantCompositum_eq_top.