The automorphism group acting on the divisors of a function field

An F-automorphism σ of F' permutes the places of F' / k (TauCeti.Place.instMulActionAlgEquiv), hence permutes the divisors of F' / k. Taking the middle field to be k itself, this is the action of Aut(F'/k) on the divisor group of F' / k.

The formal action is the one a permutation of the points induces on formal divisors (TauCeti.AlgebraicGeometry.WeilDivisor.instDistribMulAction, a scoped instance), registered here globally as TauCeti.Divisor.instDistribMulActionAlgEquiv: automorphisms do not act on the integer coefficients, so there is no competing action. What is new here is that it is compatible with the two pieces of structure that make a formal divisor a divisor of a function field. The degree is preserved, because an automorphism identifies the residue field of σ • P with that of P over the constants; and the divisor map z ↦ div z is equivariant, so the action carries principal divisors to principal divisors and descends to divisor classes.

Main results

• TauCeti.Divisor.degree_smul: an automorphism preserves the degree of a divisor;
• TauCeti.Divisor.principal_smul: div (σ z) = σ • div z, the equivariance of the principal divisor map;
• TauCeti.Divisor.smul_mem_principalSubgroup_iff and TauCeti.Divisor.linearlyEquivalent_smul_iff: the action preserves the principal divisors and linear equivalence, so it descends to the divisor classes.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.4 for divisors 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.

@[instance_reducible]

noncomputable instance TauCeti.Divisor.instDistribMulActionAlgEquiv {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'] : DistribMulAction Gal(F'/F) (Divisor k F')

The automorphism group acts on the divisors by moving the places: the specialization of the point-pushforward action on formal divisors to the action of F' ≃ₐ[F] F' on places.

Equations

• TauCeti.Divisor.instDistribMulActionAlgEquiv = TauCeti.AlgebraicGeometry.WeilDivisor.instDistribMulAction

@[simp]

theorem TauCeti.Divisor.degree_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') : degree (σ • D) = degree D

An automorphism preserves the degree of a divisor: it permutes the places and leaves each residue degree unchanged, so the weighted sum defining the degree is only reindexed.

@[simp]

theorem TauCeti.Divisor.principal_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)) (hF : IsFunctionField k F') (z : F'ˣ) : principal hF ((Units.map ↑σ) z) = σ • principal hF z

The principal divisor map is equivariant: an automorphism carries div z to div (σ z).

@[simp]

theorem TauCeti.Divisor.smul_mem_principalSubgroup_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)) (hF : IsFunctionField k F') {D : Divisor k F'} : σ • D ∈ (Place.orderSystem hF).principalSubgroup ↔ D ∈ (Place.orderSystem hF).principalSubgroup

The action preserves the principal divisors, so it descends to the divisor classes.

@[simp]

theorem TauCeti.Divisor.linearlyEquivalent_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)) (hF : IsFunctionField k F') {A B : Divisor k F'} : (Place.orderSystem hF).LinearlyEquivalent (σ • A) (σ • B) ↔ (Place.orderSystem hF).LinearlyEquivalent A B

Linear equivalence is preserved by the automorphism group: σ • A and σ • B are linearly equivalent exactly when A and B are.

@[instance_reducible]

noncomputable instance TauCeti.Divisor.instDistribMulActionClassGroup {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') : DistribMulAction Gal(F'/F) (Place.orderSystem hF).ClassGroup

The automorphism group acts on divisor classes by applying each automorphism to a representative divisor.

Equations

• TauCeti.Divisor.instDistribMulActionClassGroup hF = Function.Surjective.distribMulAction (TauCeti.Place.orderSystem hF).divisorClass ⋯ ⋯

@[simp]

theorem TauCeti.Divisor.smul_divisorClass {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)) (hF : IsFunctionField k F') (D : Divisor k F') : σ • (Place.orderSystem hF).divisorClass D = (Place.orderSystem hF).divisorClass (σ • D)

The action on divisor classes sends the class of D to the class of σ • D.