Pointed twists and nonabelian Galois cohomology

Let W be a Weierstrass curve over a field K and let L/K be a Galois extension. A pointed twist of W split by L is a Weierstrass curve V over K together with a change of variables identifying V_L with W_L, modulo change of variables over K. This file constructs the type WeierstrassCurve.PointedTwist W L of these isomorphism classes and proves the classification

PointedTwist W L ≃ H¹(Gal(L/K), Aut(W_L)).

The equivalence sends a trivialisation C : V_L ≅ W_L to the class of the cocycle σ ↦ C (σ C)⁻¹. Its injectivity is Galois descent for changes of variables; its surjectivity is effective descent for Weierstrass equations. The distinguished class of W corresponds to the base point of nonabelian cohomology.

The construction does not require ellipticity. It classifies pointed Weierstrass forms, and hence specializes to pointed elliptic twists when W is elliptic.

Main definitions

• WeierstrassCurve.PointedTwist: pointed twists split by a fixed extension.
• WeierstrassCurve.PointedTwist.mk: the class represented by a curve and a trivialisation.
• WeierstrassCurve.PointedTwist.lift: descend a representative-invariant function to pointed twists.
• WeierstrassCurve.PointedTwist.toCohomologyClass: the associated nonabelian cohomology class.
• WeierstrassCurve.pointedTwistEquivNonabelianH1: the classification equivalence.

References

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

def WeierstrassCurve.PointedTwist {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_3) [Field L] [Algebra K L] : Type (max u_1 u_3)

The pointed twists of W over K which split over L, up to pointed isomorphism over K.

A representative is a curve V/K together with a change of variables C carrying V_L to W_L. Two representatives are identified exactly when their curves are related by a change of variables over K; the chosen trivialisations over L do not form part of the resulting class.

def WeierstrassCurve.PointedTwist.mk {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_3) [Field L] [Algebra K L] (V : WeierstrassCurve K) (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) : W.PointedTwist L

The pointed-twist class represented by V and a trivialisation C : V_L ≅ W_L.

theorem WeierstrassCurve.PointedTwist.mk_eq_mk_iff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] {V U : WeierstrassCurve K} {C D : VariableChange L} {hC : C • V.baseChange L = W.baseChange L} {hD : D • U.baseChange L = W.baseChange L} : mk W L V C hC = mk W L U D hD ↔ ∃ (B : VariableChange K), B • V = U

Two presentations define the same pointed twist exactly when their curves are related by a change of variables over the base field.

theorem WeierstrassCurve.PointedTwist.induction_on {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] {motive : W.PointedTwist L → Prop} (T : W.PointedTwist L) (mk : ∀ (V : WeierstrassCurve K) (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L), motive (mk W L V C hC)) : motive T

Every pointed twist may be proved about using a representing curve and trivialisation.

def WeierstrassCurve.PointedTwist.lift {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] {β : Sort u_4} (f : (V : WeierstrassCurve K) → (C : VariableChange L) → C • V.baseChange L = W.baseChange L → β) (hf : ∀ (V : WeierstrassCurve K) (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), (∃ (B : VariableChange K), B • V = U) → f V C hC = f U D hD) : W.PointedTwist L → β

Descend a function of a representing curve and trivialisation to pointed twists, provided it takes equal values on representatives whose curves differ by a change of variables over K.

@[simp]

theorem WeierstrassCurve.PointedTwist.lift_mk {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] {β : Sort u_4} (f : (V : WeierstrassCurve K) → (C : VariableChange L) → C • V.baseChange L = W.baseChange L → β) (hf : ∀ (V : WeierstrassCurve K) (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), (∃ (B : VariableChange K), B • V = U) → f V C hC = f U D hD) (V : WeierstrassCurve K) (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) : lift f hf (mk W L V C hC) = f V C hC

A lifted function computes on a represented twist by evaluating on the representative.

theorem WeierstrassCurve.PointedTwist.lift_unique {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] {β : Sort u_4} (f : (V : WeierstrassCurve K) → (C : VariableChange L) → C • V.baseChange L = W.baseChange L → β) (hf : ∀ (V : WeierstrassCurve K) (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), (∃ (B : VariableChange K), B • V = U) → f V C hC = f U D hD) (g : W.PointedTwist L → β) (hg : ∀ (V : WeierstrassCurve K) (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L), g (mk W L V C hC) = f V C hC) : g = lift f hf

A function on pointed twists that agrees with f on every representative is lift f hf.

@[instance_reducible]

instance WeierstrassCurve.PointedTwist.instOne {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] : One (W.PointedTwist L)

The distinguished pointed twist, represented by W with the identity trivialisation.

theorem WeierstrassCurve.PointedTwist.one_def {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] : 1 = mk W L W 1 ⋯

The distinguished pointed twist is represented by W with the identity trivialisation.

noncomputable def WeierstrassCurve.PointedTwist.toCohomologyClass {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] [IsGalois K L] : W.PointedTwist L → TauCeti.NonabelianH1 Gal(L/K) (W.AutCoeff L)

The nonabelian Galois cohomology class of a pointed twist. It is represented by σ ↦ C (σ C)⁻¹ for any trivialisation C : V_L ≅ W_L.

@[simp]

theorem WeierstrassCurve.PointedTwist.toCohomologyClass_mk {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] [IsGalois K L] (V : WeierstrassCurve K) (C : VariableChange L) (hC : C • V.baseChange L = W.baseChange L) : (mk W L V C hC).toCohomologyClass = C.twistCohomologyClass hC

The cohomology class of a represented twist is the class of its trivialisation cocycle.

theorem WeierstrassCurve.PointedTwist.toCohomologyClass_injective {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] [IsGalois K L] : Function.Injective toCohomologyClass

The cohomology class determines a pointed twist.

theorem WeierstrassCurve.PointedTwist.toCohomologyClass_surjective {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] [IsGalois K L] : Function.Surjective toCohomologyClass

Every nonabelian cohomology class is the class of a pointed twist.

@[simp]

theorem WeierstrassCurve.PointedTwist.toCohomologyClass_one {K : Type u_1} [Field K] {W : WeierstrassCurve K} {L : Type u_3} [Field L] [Algebra K L] [IsGalois K L] : toCohomologyClass 1 = 1

The distinguished pointed twist maps to the base point of nonabelian cohomology.

noncomputable def WeierstrassCurve.pointedTwistEquivNonabelianH1 {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_3) [Field L] [Algebra K L] [IsGalois K L] : W.PointedTwist L ≃ TauCeti.NonabelianH1 Gal(L/K) (W.AutCoeff L)

Pointed twists are classified by nonabelian Galois cohomology. For a Galois extension L/K, the pointed twists of W split by L are in bijection with H¹(Gal(L/K), Aut(W_L)). The equivalence sends a trivialisation C to the class of the cocycle σ ↦ C (σ C)⁻¹.

@[simp]

theorem WeierstrassCurve.pointedTwistEquivNonabelianH1_apply {K : Type u_1} [Field K] (W : WeierstrassCurve K) (L : Type u_3) [Field L] [Algebra K L] [IsGalois K L] (T : W.PointedTwist L) : (W.pointedTwistEquivNonabelianH1 L) T = T.toCohomologyClass

The twist-classification equivalence is the cohomology-class map on representatives.