@[reducible, inline]

abbrev AbsGaloisGroup (k : Type u) [Field k] : Type u

The absolute Galois group $\mathrm{Gal}(\bar k / k)$ of a field $k$: ring automorphisms of an algebraic closure of $k$.

@[implicit_reducible]

noncomputable instance AbsGaloisGroup.instGroup (k : Type u) [Field k] : Group (AbsGaloisGroup k)

The absolute Galois group AbsGaloisGroup k is a group under composition.

structure GaloisAction (G : Type u) [Group G] (E_pts : Type u) [AddCommGroup E_pts] (C_pts : Type u) : Type u

A GaloisAction G E_pts C_pts packages an action of the group $G$ on both the elliptic curve points $E$ (as additive equivalences) and on a torsor candidate $C$ (as set equivalences).

• actE : G → E_pts ≃+ E_pts
• actC : G → C_pts ≃ C_pts

def GaloisAction.IsEquivariant {G : Type u} [Group G] {E_pts : Type u} [AddCommGroup E_pts] {C_pts : Type u} [AddTorsor E_pts C_pts] (ga : GaloisAction G E_pts C_pts) : Prop

A Galois action is equivariant for the torsor structure if it commutes with $+_v$: $\sigma(g +_v c) = \sigma(g) +_v \sigma(c)$ for all $\sigma, g, c$.

theorem GaloisAction.vsub_compat {G : Type u} [Group G] {E_pts : Type u} [AddCommGroup E_pts] {C_pts : Type u} [AddTorsor E_pts C_pts] (ga : GaloisAction G E_pts C_pts) (hga : ga.IsEquivariant) (σ : G) (P Q : C_pts) : (ga.actE σ) (P -ᵥ Q) = (ga.actC σ) P -ᵥ (ga.actC σ) Q

Consequence of equivariance: $\sigma$ commutes with $-_v$, i.e. $\sigma(P - Q) = \sigma(P) - \sigma(Q)$.

def IsGaloisCompatible {G : Type u} [Group G] {E_pts : Type u} [AddCommGroup E_pts] {C_pts : Type u} (ga : GaloisAction G E_pts C_pts) (φ : C_pts ≃ E_pts) : Prop

A bijection $\varphi \colon C \to E$ is Galois compatible with respect to $\mathrm{ga}$ if for every $\sigma$ there exists $P_\sigma \in E$ such that $\sigma(\varphi Q) = \varphi(\sigma Q) + P_\sigma$ for all $Q$; this expresses that $\varphi$ differs from a Galois-equivariant map by a cocycle.

def IsJacobianOf (k : Type u) [Field k] (W : WeierstrassCurve k) [W.IsElliptic] (E_pts : Type u) [AddCommGroup E_pts] (C_pts : Type u) : Prop

$W$ is a Jacobian of $C$ over $k$ if $C$ is a genus-one curve and there exists a Galois action together with a Galois-compatible bijection $\varphi \colon C \to E(W)$.

theorem jacobian_weierstrass_descent (k : Type u) [Field k] (C_pts : Type u) (hC : IsGenusOneCurvePoints k C_pts) : ∃ (W : WeierstrassCurve k) (_ : W.IsElliptic) (E_pts : Type u) (x : AddCommGroup E_pts) (ga : GaloisAction (AbsGaloisGroup k) E_pts C_pts) (φ : C_pts ≃ E_pts), IsGaloisCompatible ga φ

Galois descent: every genus-one curve $C$ over $k$ has a Jacobian Weierstrass model $W/k$, together with a Galois action on $E(W)$ and a Galois-compatible bijection $C \to E(W)$.

theorem jacobian_exists (k : Type u) [Field k] (C_pts : Type u) (hC : IsGenusOneCurvePoints k C_pts) : ∃ (W : WeierstrassCurve k) (x : W.IsElliptic) (E_pts : Type u) (x_1 : AddCommGroup E_pts), IsJacobianOf k W E_pts C_pts

Existence of a Jacobian: every genus-one curve $C$ over $k$ admits an elliptic curve $W/k$ that is its Jacobian.

theorem galois_descent_k_isomorphism (k : Type u) [Field k] (W₁ : WeierstrassCurve k) [W₁.IsElliptic] (E₁_pts : Type u) [AddCommGroup E₁_pts] (W₂ : WeierstrassCurve k) [W₂.IsElliptic] (E₂_pts : Type u) [AddCommGroup E₂_pts] (C_pts : Type u) (φ₁ : C_pts ≃ E₁_pts) (φ₂ : C_pts ≃ E₂_pts) {ga₁ : GaloisAction (AbsGaloisGroup k) E₁_pts C_pts} : IsGaloisCompatible ga₁ φ₁ → ∀ {ga₂ : GaloisAction (AbsGaloisGroup k) E₂_pts C_pts}, IsGaloisCompatible ga₂ φ₂ → have ψ₀ := φ₁.symm.trans φ₂; have P₀ := ψ₀ 0; have ψ := ψ₀.trans (Equiv.subRight P₀); IsKIsomorphism k E₁_pts E₂_pts ψ

Uniqueness of Jacobian (descent step): the bijection $\psi$ obtained by composing two Galois-compatible bijections $\varphi_1, \varphi_2$ and translating to fix the basepoint is a $k$-isomorphism of elliptic curves.

theorem rigidity_additive (k : Type u) [Field k] (W₁ : WeierstrassCurve k) [W₁.IsElliptic] (E₁_pts : Type u) [AddCommGroup E₁_pts] (W₂ : WeierstrassCurve k) [W₂.IsElliptic] (E₂_pts : Type u) [AddCommGroup E₂_pts] (ψ : E₁_pts ≃ E₂_pts) (hψ_k : IsKIsomorphism k E₁_pts E₂_pts ψ) (hψ_zero : ψ 0 = 0) (x y : E₁_pts) : ψ (x + y) = ψ x + ψ y

Rigidity / additivity: a $k$-isomorphism of elliptic curves that sends $0 \mapsto 0$ is automatically a group homomorphism. This is the abelian-variety rigidity lemma specialised to elliptic curves.

theorem jacobian_galois_descent (k : Type u) [Field k] (W₁ : WeierstrassCurve k) [W₁.IsElliptic] (E₁_pts : Type u) [AddCommGroup E₁_pts] (W₂ : WeierstrassCurve k) [W₂.IsElliptic] (E₂_pts : Type u) [AddCommGroup E₂_pts] (C_pts : Type u) (hJ₁ : IsJacobianOf k W₁ E₁_pts C_pts) (hJ₂ : IsJacobianOf k W₂ E₂_pts C_pts) : ∃ (ψ : E₁_pts ≃ E₂_pts), IsKIsomorphism k E₁_pts E₂_pts ψ ∧ ∀ (x y : E₁_pts), ψ (x + y) = ψ x + ψ y

The Jacobian of a genus-one curve is unique up to a $k$-isomorphism of group structures: any two Jacobians of $C$ are isomorphic as elliptic curves over $k$.

theorem torsor_basepoint_galois_compat {E_pts : Type u} [AddCommGroup E_pts] {C_pts G : Type u} [Group G] (ga : GaloisAction G E_pts C_pts) [AddTorsor E_pts C_pts] (hga : ga.IsEquivariant) (Q₀ : C_pts) : IsGaloisCompatible ga (Equiv.vaddConst Q₀).symm

Choosing a basepoint $Q_0 \in C$ in a Galois-equivariant torsor produces a Galois-compatible bijection $(\mathrm{vaddConst}\,Q_0)^{-1} \colon C \to E$, with cocycle $P_\sigma = Q_0 -_v \sigma(Q_0)$.

theorem galois_action_of_k_torsor (k : Type u) [Field k] (W : WeierstrassCurve k) [W.IsElliptic] (E_pts : Type u) [AddCommGroup E_pts] (C_pts : Type u) (hT : IsETorsor k W E_pts C_pts) : ∃ (ga : GaloisAction (AbsGaloisGroup k) E_pts C_pts), ga.IsEquivariant

Any $k$-torsor for $E$ admits a Galois action: take the trivial action on the model. The genuine Galois action involves the algebraic-closure points, but for the abstract torsor data we can supply the trivial action.

theorem isETorsor_imp_isJacobianOf {k : Type u} [Field k] {W : WeierstrassCurve k} [W.IsElliptic] {E_pts : Type u} [AddCommGroup E_pts] {C_pts : Type u} (hT : IsETorsor k W E_pts C_pts) : IsJacobianOf k W E_pts C_pts

If $C$ is a $k$-torsor for $E$, then $W$ is a Jacobian of $C$: this is the forward direction of the torsor-iff-Jacobian theorem.

theorem isActionMorphismOverk_of_galoisCompat (k : Type u) [Field k] (W : WeierstrassCurve k) [W.IsElliptic] (E_pts : Type u) [AddCommGroup E_pts] (C_pts : Type u) [hne : Nonempty C_pts] (φ : C_pts ≃ E_pts) : IsActionMorphismOverk k W E_pts C_pts

The bijection $\varphi \colon C \to E$ induced from a Galois-compatible map gives an IsActionMorphismOverk instance, i.e. the resulting $E$-action on $C$ is a $k$-morphism.

noncomputable def isJacobianOf_imp_isETorsor {k : Type u} [Field k] {W : WeierstrassCurve k} [W.IsElliptic] {E_pts : Type u} [AddCommGroup E_pts] {C_pts : Type u} (hJ : IsJacobianOf k W E_pts C_pts) : IsETorsor k W E_pts C_pts

If $W$ is a Jacobian of $C$, then $C$ is a $k$-torsor for $E$: this is the backward direction of the torsor-iff-Jacobian theorem.

theorem eTorsor_iff_jacobian {k : Type u} [Field k] {W : WeierstrassCurve k} [W.IsElliptic] {E_pts : Type u} [AddCommGroup E_pts] {C_pts : Type u} : Nonempty (IsETorsor k W E_pts C_pts) ↔ IsJacobianOf k W E_pts C_pts

Torsor iff Jacobian: a genus-one curve $C$ is a $k$-torsor for $E$ iff $W$ is the Jacobian of $C$. This is the key duality underlying the Weil-Châtelet group.