The Galois cocycle of a pointed twist

Let V and W be Weierstrass curves over K, and let C carry V to W over an algebraic extension L/K. Then σ ↦ C (σ C)⁻¹ is a continuous cocycle with values in the discrete automorphism group of W over L. Its cohomology class does not depend on C. Over a Galois extension, two such classes agree exactly when their source curves are isomorphic over K by a change of variables. In particular, the class is trivial exactly when V is isomorphic to W over K.

The construction applies in every characteristic, including over a separable closure of an imperfect field. It does not assume ellipticity: the equation-level construction also makes sense for singular Weierstrass cubics.

Main results

• WeierstrassCurve.VariableChange.twistCocycle: the continuous cocycle of a trivialisation.
• WeierstrassCurve.VariableChange.twistCohomologyClass_eq: independence of the trivialisation.
• WeierstrassCurve.VariableChange.twistCohomologyClass_eq_iff: equality of classes detects isomorphism over the base field.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, X.2 and X.5.
• J.-P. Serre, Galois Cohomology, III.1.

def WeierstrassCurve.AutCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_2) [Field L] [Algebra K L] : Type u_2

The automorphisms of W over L, with the discrete topology imposed, as coefficients for continuous nonabelian Galois cohomology.

@[instance_reducible]

noncomputable instance WeierstrassCurve.instGroupAutCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_2) [Field L] [Algebra K L] : Group (W.AutCoeff L)

@[instance_reducible]

noncomputable instance WeierstrassCurve.instTopologicalSpaceAutCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_2) [Field L] [Algebra K L] : TopologicalSpace (W.AutCoeff L)

instance WeierstrassCurve.instDiscreteTopologyAutCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_2) [Field L] [Algebra K L] : DiscreteTopology (W.AutCoeff L)

noncomputable def WeierstrassCurve.autCoeffEquiv {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_2) [Field L] [Algebra K L] : ↥(W.baseChange L).autGroup ≃* W.AutCoeff L

Identify the discrete coefficient group with the stabilizer of the base-changed equation.

theorem WeierstrassCurve.AutCoeff.ext {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_2) [Field L] [Algebra K L] {a b : W.AutCoeff L} (h : ↑((W.autCoeffEquiv L).symm a) = ↑((W.autCoeffEquiv L).symm b)) : a = b

Automorphism coefficients are determined by their underlying change of variables.

theorem WeierstrassCurve.AutCoeff.ext_iff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {a b : W.AutCoeff L} : a = b ↔ ↑((W.autCoeffEquiv L).symm a) = ↑((W.autCoeffEquiv L).symm b)

@[instance_reducible]

noncomputable instance WeierstrassCurve.instSMulAlgEquivAutCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) {L : Type u_2} [Field L] [Algebra K L] : SMul Gal(L/K) (W.AutCoeff L)

@[simp]

theorem WeierstrassCurve.autCoeffEquiv_symm_smul {K : Type u_1} [Field K] (W : WeierstrassCurve K) {L : Type u_2} [Field L] [Algebra K L] (σ : Gal(L/K)) (a : W.AutCoeff L) : ↑((W.autCoeffEquiv L).symm (σ • a)) = (↑((W.autCoeffEquiv L).symm a)).map ↑σ

Galois acts on the automorphism group by conjugating the four coefficients.

@[simp]

theorem WeierstrassCurve.smul_autCoeffEquiv {K : Type u_1} [Field K] (W : WeierstrassCurve K) {L : Type u_2} [Field L] [Algebra K L] (σ : Gal(L/K)) (a : ↥(W.baseChange L).autGroup) : σ • (W.autCoeffEquiv L) a = (W.autCoeffEquiv L) ⟨(↑a).map ↑σ, ⋯⟩

Galois conjugation commutes with the identification of the automorphism coefficient group.

@[instance_reducible]

noncomputable instance WeierstrassCurve.instMulDistribMulActionAlgEquivAutCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) {L : Type u_2} [Field L] [Algebra K L] : MulDistribMulAction Gal(L/K) (W.AutCoeff L)

instance WeierstrassCurve.AutCoeff.instContinuousSMul {K : Type u_1} [Field K] (W : WeierstrassCurve K) {L : Type u_2} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : ContinuousSMul Gal(L/K) (W.AutCoeff L)

Over an algebraic extension the discrete automorphism group has a continuous Galois action: its orbit maps depend on only four algebraic coefficients.

noncomputable def WeierstrassCurve.VariableChange.twistCocycle {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [Algebra.IsAlgebraic K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) : TauCeti.NonabelianH1.Cocycle Gal(L/K) (W.AutCoeff L)

The continuous cocycle of a pointed trivialisation C : V_L ≅ W_L: σ ↦ C (σ C)⁻¹.

theorem WeierstrassCurve.VariableChange.twistCocycle_apply {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [Algebra.IsAlgebraic K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) (σ : Gal(L/K)) : (C.twistCocycle hC) σ = (W.autCoeffEquiv L) ⟨C * (C.map ↑σ)⁻¹, ⋯⟩

The cocycle of a trivialisation, expressed in the automorphism coefficient group.

@[simp]

theorem WeierstrassCurve.VariableChange.autCoeffEquiv_symm_twistCocycle {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [Algebra.IsAlgebraic K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) (σ : Gal(L/K)) : ↑((W.autCoeffEquiv L).symm ((C.twistCocycle hC) σ)) = C * (C.map ↑σ)⁻¹

The coefficient formula for the cocycle of a trivialisation.

noncomputable def WeierstrassCurve.VariableChange.twistCohomologyClass {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [Algebra.IsAlgebraic K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) : TauCeti.NonabelianH1 Gal(L/K) (W.AutCoeff L)

The nonabelian cohomology class associated to a pointed trivialisation.

theorem WeierstrassCurve.VariableChange.twistCohomologyClass_def {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [Algebra.IsAlgebraic K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) : C.twistCohomologyClass hC = TauCeti.NonabelianH1.mk (C.twistCocycle hC)

The class is represented by the cocycle σ ↦ C (σ C)⁻¹.

theorem WeierstrassCurve.VariableChange.twistCohomologyClass_eq {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [Algebra.IsAlgebraic K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) (D : VariableChange L) (hD : D • V.baseChange L = W.baseChange L) : C.twistCohomologyClass hC = D.twistCohomologyClass hD

Two trivialisations of the same pointed twist give the same cohomology class.

@[simp]

theorem WeierstrassCurve.VariableChange.twistCocycle_one {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : twistCocycle 1 ⋯ = 1

The identity trivialisation gives the trivial cocycle.

theorem WeierstrassCurve.VariableChange.twistCohomologyClass_eq_iff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [IsGalois K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) {U : WeierstrassCurve K} (D : VariableChange L) (hD : D • U.baseChange L = W.baseChange L) : C.twistCohomologyClass hC = D.twistCohomologyClass hD ↔ ∃ (B : VariableChange K), B • V = U

Two pointed twists give the same Galois cohomology class exactly when they are isomorphic by a change of variables over the base field.

@[simp]

theorem WeierstrassCurve.VariableChange.twistCohomologyClass_eq_one_iff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_2} [Field L] [Algebra K L] {V : WeierstrassCurve K} [IsGalois K L] (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) : C.twistCohomologyClass hC = 1 ↔ ∃ (B : VariableChange K), B • V = W

A twist has trivial Galois cohomology class exactly when V is isomorphic to W by a change of variables defined over the base field.