Riemann–Roch spaces 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, and let D be a divisor of F / k. The Riemann–Roch space L(Con D) of the conorm of D is spanned over k' by the image of L(D), any k-basis of L(D) is a k'-basis of L(Con D), and in particular ℓ(Con D) = ℓ(D).

The inclusion of L(D) into L(Con D) and the linear independence over k' of a k-basis of L(D) are the elementary half, coming from the local comparison of orders and from linear disjointness. Spanning is the local integral-basis statement: an element of L(Con D) multiplied by a function of F of order D P at a place P is integral over 𝒪_P, so its coordinates in a basis of constants lie in 𝒪_P; running over all places, the coordinates lie in L(D).

Together with the preservation of divisor degrees, the dimension identity is what transports the genus, the Riemann–Roch theorem and its consequences between F / k and F' / k'.

Main results

• TauCeti.repr_constantBasis_mem_riemannRochSpace: the coordinates of an element of L(Con D) in a basis of constants lie in L(D).
• TauCeti.riemannRochSpace_conorm_eq_span: L(Con D) is the k'-span of the image of L(D).
• TauCeti.riemannRochSpaceConormBasis: a k-basis of L(D) as a k'-basis of L(Con D).
• TauCeti.Divisor.dim_conorm: ℓ(Con D) = ℓ(D).

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6, Theorem 3.6.3(d).

theorem TauCeti.repr_constantBasis_mem_riemannRochSpace {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' = ⊤) (hF' : IsFunctionField k' F') {ι : Type u_1} (b : Module.Basis ι k k') {D : Divisor k F} {z : F'} (hz : z ∈ riemannRochSpace ((Divisor.conorm k' F') D)) (i : ι) : ((constantBasis hex h b).repr z) i ∈ riemannRochSpace D

The coordinates of an element of L(Con D) in a basis of constants lie in L(D): at each place P of F / k, clearing the pole order allowed by D makes the element integral over 𝒪_P, and a basis of constants is an integral basis at P.

theorem TauCeti.riemannRochSpace_conorm_eq_span {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' = ⊤) (hF' : IsFunctionField k' F') (D : Divisor k F) : riemannRochSpace ((Divisor.conorm k' F') D) = Submodule.span k' (⇑(algebraMap F F') '' ↑(riemannRochSpace D))

L(Con D) is spanned over k' by L(D) (Stichtenoth, Theorem 3.6.3(d)): the Riemann–Roch space of the conorm of D in a finite separable constant field extension is the k'-span of the image of the Riemann–Roch space of D.

theorem TauCeti.linearIndependent_algebraMap_riemannRochSpace {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'] (hex : IsIntegrallyClosedIn k F) {D : Divisor k F} {ι : Type u_1} (b : Module.Basis ι k ↥(riemannRochSpace D)) : LinearIndependent k' fun (i : ι) => (algebraMap F F') ↑(b i)

The image of a k-basis of L(D) is linearly independent over k': F and k' are linearly disjoint over k (Stichtenoth, Proposition 3.6.1(b)).

theorem TauCeti.span_range_algebraMap_eq_riemannRochSpace_conorm {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' = ⊤) (hF' : IsFunctionField k' F') (D : Divisor k F) {ι : Type u_1} (b : Module.Basis ι k ↥(riemannRochSpace D)) : Submodule.span k' (Set.range fun (i : ι) => (algebraMap F F') ↑(b i)) = riemannRochSpace ((Divisor.conorm k' F') D)

The k'-span of the image of a k-basis of L(D) is L(Con D).

noncomputable def TauCeti.riemannRochSpaceConormBasis {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' = ⊤) (hF' : IsFunctionField k' F') (D : Divisor k F) {ι : Type u_1} (b : Module.Basis ι k ↥(riemannRochSpace D)) : Module.Basis ι k' ↥(riemannRochSpace ((Divisor.conorm k' F') D))

A basis of L(D) is a basis of L(Con D) (Stichtenoth, Theorem 3.6.3(d)): in a finite separable constant field extension, the image of a k-basis of the Riemann–Roch space of D is a k'-basis of the Riemann–Roch space of the conorm of D.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.riemannRochSpaceConormBasis_apply {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' = ⊤) (hF' : IsFunctionField k' F') (D : Divisor k F) {ι : Type u_1} (b : Module.Basis ι k ↥(riemannRochSpace D)) (i : ι) : ↑((riemannRochSpaceConormBasis hex h hF' D b) i) = (algebraMap F F') ↑(b i)

theorem TauCeti.Divisor.dim_conorm {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' = ⊤) (hF' : IsFunctionField k' F') (D : Divisor k F) : ((conorm k' F') D).dim = D.dim

ℓ(Con D) = ℓ(D) (Stichtenoth, Theorem 3.6.3(d)): the dimension of a Riemann–Roch space is unchanged by a finite separable constant field extension.