Galois actions on the places of a Weierstrass function field

For a curve defined over F, coefficient automorphisms of K/F permute the places of K(W)/K. The action transports valuations along the semilinear function-field action and preserves residue degrees. On an elliptic curve, the point–place dictionary intertwines this action with the coefficientwise action on points. These compatibilities let Galois conjugation transport the zeros and poles used in the divisor construction of the Weil pairing.

References

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

noncomputable def WeierstrassCurve.placeGaloisAction {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) : Gal(K/F) →* Equiv.Perm (TauCeti.Place K (W.baseChange K).toAffine.FunctionField)

The Galois action on places of a base-changed curve. A coefficient automorphism carries v to v ∘ σ⁻¹, where σ acts semilinearly on the function field.

Equations

• W.placeGaloisAction = { toFun := fun (σ : Gal(K/F)) => TauCeti.Place.equivOfRingEquiv σ.toRingEquiv (W.functionFieldGaloisAction σ) ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem WeierstrassCurve.placeGaloisAction_symm {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) : Equiv.symm (W.placeGaloisAction σ) = W.placeGaloisAction σ.symm

The inverse action on places is the action of the inverse coefficient automorphism.

@[simp]

theorem WeierstrassCurve.placeGaloisAction_valuation {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) (z : (W.baseChange K).toAffine.FunctionField) : ((W.placeGaloisAction σ) v).valuation z = v.valuation ((W.functionFieldGaloisAction σ).symm z)

The Galois action on places is transport of their valuations.

@[simp]

theorem WeierstrassCurve.placeGaloisAction_ord {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) (z : (W.baseChange K).toAffine.FunctionField) : ((W.placeGaloisAction σ) v).ord z = v.ord ((W.functionFieldGaloisAction σ).symm z)

Galois conjugation preserves the order at the conjugate place.

@[simp]

theorem WeierstrassCurve.placeGaloisAction_degree {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) : ((W.placeGaloisAction σ) v).degree = v.degree

Galois conjugation preserves the residue degree over K.

@[simp]

theorem WeierstrassCurve.placeGaloisAction_infinity {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) : (W.placeGaloisAction σ) (TauCeti.Place.infinity (W.baseChange K).toAffine) = TauCeti.Place.infinity (W.baseChange K).toAffine

The Galois action fixes the place at infinity.

theorem WeierstrassCurve.instIsDedekindDomainCoordinateRingToAffineBaseChange_tauCeti {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) [W.IsElliptic] : IsDedekindDomain (W.baseChange K).toAffine.CoordinateRing

@[simp]

theorem WeierstrassCurve.placeGaloisAction_pointEquivDegreeOnePlace {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) [DecidableEq K] [W.IsElliptic] (σ : Gal(K/F)) (P : (W.baseChange K).toAffine.Point) : (W.placeGaloisAction σ) ↑((W.baseChange K).toAffine.pointEquivDegreeOnePlace P) = ↑((W.baseChange K).toAffine.pointEquivDegreeOnePlace ((Multiplicative.toAdd (W.pointGaloisAction σ)) P))

The point–place dictionary is Galois-equivariant. Conjugating a point conjugates its place by the semilinear function-field action.