Riemann–Roch spaces under extension of function fields #
For a finite extension of function fields, the functions in L(D) are exactly those
functions from the smaller field whose images belong to L(Con D). This gives the
intersection of L(Con D) with the smaller field as a submodule equality.
Reference #
H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6, Theorem 3.6.3(d).
theorem
TauCeti.mem_riemannRochSpace_conorm_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 F F']
[Algebra k F']
[IsScalarTower k k' F']
[IsScalarTower k F F']
[Algebra.IsIntegral k k']
[FiniteDimensional F F']
(hF' : IsFunctionField k' F')
(D : Divisor k F)
(f : F)
:
A function from F belongs to L(D) precisely when its image in F' belongs to the
Riemann–Roch space of the conorm of D.
@[simp]
theorem
TauCeti.riemannRochSpace_conorm_comap
{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 F F']
[Algebra k F']
[IsScalarTower k k' F']
[IsScalarTower k F F']
[Algebra.IsIntegral k k']
[FiniteDimensional F F']
(hF' : IsFunctionField k' F')
(D : Divisor k F)
:
Submodule.comap (IsScalarTower.toAlgHom k F F').toLinearMap
(Submodule.restrictScalars k (riemannRochSpace ((Divisor.conorm k' F') D))) = riemannRochSpace D
The intersection of L(Con D) with the image of F is L(D), expressed as a
k-submodule equality. This form can be used without unfolding either Riemann–Roch space.