Galois actions on divisors of Weierstrass curves

Coefficient automorphisms act on divisors by transporting their places and retaining their integer coefficients. This action preserves degree and takes div f to div (σ f), so it preserves linear equivalence. Together with the equivariance of the point–place dictionary, this transports the divisors and rational functions entering the Weil pairing.

The action reuses Mathlib's Finsupp.domCongr on the existing TauCeti.Divisor carrier.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.3 and III.8.

noncomputable def WeierstrassCurve.divisorGaloisAction {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) : Gal(K/F) →* Multiplicative (AddAut (TauCeti.Divisor K (W.baseChange K).toAffine.FunctionField))

The Galois action on divisors of a base-changed curve. It pushes forward each place by placeGaloisAction and leaves its integer coefficient unchanged.

Equations

• W.divisorGaloisAction = { toFun := fun (σ : Gal(K/F)) => Multiplicative.ofAdd (Finsupp.domCongr (W.placeGaloisAction σ)), map_one' := ⋯, map_mul' := ⋯ }

theorem WeierstrassCurve.divisorGaloisAction_apply {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (D : TauCeti.Divisor K (W.baseChange K).toAffine.FunctionField) : (Multiplicative.toAdd (W.divisorGaloisAction σ)) D = (TauCeti.AlgebraicGeometry.WeilDivisor.pushforward ⇑(W.placeGaloisAction σ)) D

The divisor action is the formal pushforward along the Galois action on places.

@[simp]

theorem WeierstrassCurve.divisorGaloisAction_coeff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (D : TauCeti.Divisor K (W.baseChange K).toAffine.FunctionField) (v : TauCeti.Place K (W.baseChange K).toAffine.FunctionField) : TauCeti.AlgebraicGeometry.WeilDivisor.coeff ((Multiplicative.toAdd (W.divisorGaloisAction σ)) D) v = TauCeti.AlgebraicGeometry.WeilDivisor.coeff D ((W.placeGaloisAction σ.symm) v)

The coefficient at v after conjugation is the old coefficient at σ⁻¹ v.

@[simp]

theorem WeierstrassCurve.divisorGaloisAction_ofPoint {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (v : TauCeti.Place K (W.baseChange K).toAffine.FunctionField) : (Multiplicative.toAdd (W.divisorGaloisAction σ)) (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint v) = TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ((W.placeGaloisAction σ) v)

Conjugation takes a prime divisor to the prime divisor at the conjugate place.

@[simp]

theorem WeierstrassCurve.divisorGaloisAction_degree {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (D : TauCeti.Divisor K (W.baseChange K).toAffine.FunctionField) : TauCeti.Divisor.degree ((Multiplicative.toAdd (W.divisorGaloisAction σ)) D) = TauCeti.Divisor.degree D

Galois conjugation preserves divisor degree.

@[simp]

theorem WeierstrassCurve.divisorGaloisAction_principal {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (f : (W.baseChange K).toAffine.FunctionFieldˣ) : TauCeti.Divisor.principal ⋯ ((Units.map ↑(W.functionFieldGaloisAction σ)) f) = (Multiplicative.toAdd (W.divisorGaloisAction σ)) (TauCeti.Divisor.principal ⋯ f)

Principal divisors are Galois-equivariant. The zeros and poles of σ f are the conjugates of those of f, with the same multiplicities.

@[simp]

theorem WeierstrassCurve.divisorGaloisAction_linearlyEquivalent_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (A B : TauCeti.Divisor K (W.baseChange K).toAffine.FunctionField) : (TauCeti.Place.orderSystem ⋯).LinearlyEquivalent ((Multiplicative.toAdd (W.divisorGaloisAction σ)) A) ((Multiplicative.toAdd (W.divisorGaloisAction σ)) B) ↔ (TauCeti.Place.orderSystem ⋯).LinearlyEquivalent A B

Galois conjugation preserves and reflects linear equivalence of divisors.