The automorphism group acting on Riemann–Roch spaces

An F-automorphism σ of F' permutes the places of F' / k, and hence the divisors of F' / k. Because σ moves the valuation at a place to the valuation at the moved place, it carries the Riemann–Roch space L(D) onto L(σ • D). The two spaces are therefore isomorphic over the constants, so the dimension ℓ(D) is constant on the orbit of D.

Together with the invariance of the degree, this says that deg and ℓ are constant on automorphism orbits of divisors.

Main definitions

• TauCeti.riemannRochSpaceEquivSmul: the isomorphism L(D) ≃ₗ[k] L(σ • D) induced by σ.

Main results

• TauCeti.mem_riemannRochSpace_smul_iff and TauCeti.riemannRochSpace_map_smul: σ carries L(D) onto L(σ • D), pointwise and as a submodule;
• TauCeti.apply_eq_self_of_mem_riemannRochSpace_of_degree_lt_card: an automorphism fixing more rational places than the degree of a fixed divisor acts trivially on its Riemann–Roch space;
• TauCeti.Divisor.dim_smul: ℓ(σ • D) = ℓ(D).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.4 for Riemann–Roch spaces and Section III.5 for the automorphism action on places.
• G. D. Villa Salvador, Topics in the Theory of Algebraic Function Fields, Birkhäuser, 2006, Chapter 9, for automorphism groups of function fields.

@[simp]

theorem TauCeti.mem_riemannRochSpace_smul_iff {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (D : Divisor k F') {f : F'} : σ f ∈ riemannRochSpace (σ • D) ↔ f ∈ riemannRochSpace D

σ f lies in L(σ • D) exactly when f lies in L(D): σ moves the valuation at a place to the valuation at the moved place, where the bound imposed by σ • D is the one D imposed before.

@[simp]

theorem TauCeti.riemannRochSpace_map_smul {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (D : Divisor k F') : Submodule.map (AlgEquiv.restrictScalars k σ).toLinearMap (riemannRochSpace D) = riemannRochSpace (σ • D)

An automorphism carries L(D) onto L(σ • D), as a k-submodule of F'.

noncomputable def TauCeti.riemannRochSpaceEquivSmul {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (D : Divisor k F') : ↥(riemannRochSpace D) ≃ₗ[k] ↥(riemannRochSpace (σ • D))

The isomorphism of Riemann–Roch spaces induced by an automorphism: σ restricts to a k-linear isomorphism L(D) ≃ L(σ • D).

Equations

• TauCeti.riemannRochSpaceEquivSmul σ D = (↑(AlgEquiv.restrictScalars k σ)).ofSubmodules (TauCeti.riemannRochSpace D) (TauCeti.riemannRochSpace (σ • D)) ⋯

@[simp]

theorem TauCeti.riemannRochSpaceEquivSmul_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (D : Divisor k F') (f : ↥(riemannRochSpace D)) : ↑((riemannRochSpaceEquivSmul σ D) f) = σ ↑f

@[simp]

theorem TauCeti.riemannRochSpaceEquivSmul_symm_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (D : Divisor k F') (f : ↥(riemannRochSpace (σ • D))) : ↑((riemannRochSpaceEquivSmul σ D).symm f) = σ.symm ↑f

theorem TauCeti.apply_eq_self_of_mem_riemannRochSpace_of_degree_lt_card {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (hF : IsFunctionField k F') {σ : Gal(F'/F)} {D : Divisor k F'} (hD : σ • D = D) {T : Finset (Place k F')} (hT : ∀ Q ∈ T, Q.degree = 1 ∧ σ • Q = Q ∧ AlgebraicGeometry.WeilDivisor.coeff D Q = 0) (hdeg : Divisor.degree D < ↑T.card) {z : F'} (hz : z ∈ riemannRochSpace D) : σ z = z

An automorphism fixing enough rational places fixes a Riemann–Roch space pointwise. Let σ fix the divisor D, and let T be a finite set of rational places outside the support of D, each fixed by σ. If deg D < #T, then σ z = z for every z ∈ L(D).

@[simp]

theorem TauCeti.Divisor.dim_smul {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (D : Divisor k F') : (σ • D).dim = D.dim

The dimension ℓ(D) is invariant under the automorphism group: an automorphism identifies L(D) with L(σ • D) over the constants.