Galois action on n-torsion; irreducibility predicate #
Definition: FLTPrelim_GaloisRep (352cbb80-09ad-5c6e-9401-39871c32239e), by Claude, 2026-09-05.
For a Weierstrass curve W' : Affine R and a tower of algebras $R \to S \to K$ with $K$ a field
(with decidable equality), the module makes the group $K \simeq_{\mathrm{alg}[S]} K$ of $S$-algebra
automorphisms of $K$ act on the group of points $(W'\!⁄K)$.Point of the base change of $W'$ to
$K$: $\sigma \bullet P$ is defined to be Point.map of $\sigma$ viewed as an $S$-algebra
homomorphism (algEquiv_smul_def), and this is upgraded to a DistribMulAction, so the action is
by group automorphisms of the Mordell–Weil-type group $(W'\!⁄K)$.Point. Since the action commutes
with integer multiples (algEquiv_smul_zsmul), it preserves Submodule.torsionBy ℤ (W'⁄K).Point n,
the subgroup of points killed by $n$ (smul_mem_torsionBy), giving an induced DistribMulAction on
that $n$-torsion subgroup; the $n$-torsion is also equipped with its canonical $\mathbb Z/n$-module
structure, obtained from AddCommGroup.zmodModule using that $n$ annihilates it.
Two predicates are then defined. IsGaloisStable S N, for $N$ a $\mathbb Z/n$-submodule of the
$n$-torsion, says that $\sigma \bullet x \in N$ for every $S$-algebra automorphism $\sigma$ of $K$
and every $x \in N$. GaloisRepIsIrreducible S W' n is the conjunction of: the $n$-torsion of
$(W'\!⁄K)$.Point is Nontrivial (i.e. contains a nonzero point), and every $\mathbb Z/n$-submodule $N$ of it satisfying IsGaloisStable S N equals $\bot$ or $\top$. The formulation is
basis-free: no identification of the $n$-torsion with $(\mathbb Z/n)^2$, no matrix representation,
and no primality assumption on $n$ or algebraic-closedness assumption on $K$ is imposed; the acting
group is literally the automorphism group $K \simeq_{\mathrm{alg}[S]} K$. A final instance supplies
classical decidable equality on AlgebraicClosure ℚ, the case of $K$ used in the application.
Relation to Mathlib. The curve, its affine points and Point.map, Submodule.torsionBy and
AddCommGroup.zmodModule are Mathlib's; the action of $S$-algebra automorphisms of $K$ on the
points, the induced action and $\mathbb Z/n$-module structure on the $n$-torsion, and the predicates
IsGaloisStable and GaloisRepIsIrreducible are the project's own.
Where it is used. These definitions carry the irreducibility step for the Frey curve: the
statement proved about a Frey package $P$ is GaloisRepIsIrreducible ℚ P.freyCurve P.p, i.e. that
$E_P[p]$ over an algebraic closure of $\mathbb Q$ is nonzero and has no Galois-stable $\mathbb Z/p$-submodule other than $0$ and everything, which is the hypothesis feeding the
modularity/level-lowering part of the argument.
Attribution: this file contains material adapted from third-party Apache-2.0 sources (adapted
(upstream notice retained in place, from our May port): FLT/EllipticCurve/Torsion.lean (commit
7a87d3b25db1) — © 2024 Kevin Buzzard; authors: Kevin Buzzard (path as recorded in our port; the
notice retained inside our file is our May port's generic one, the upstream notice is reproduced
here)). See ATTRIBUTION.md and NOTICE in the source repository.
<!-- Generated by add_prove2me_provenance.py -->
Equations
- WeierstrassCurve.Affine.Point.instSMulAlgEquiv = { smul := fun (σ : K ≃ₐ[S] K) (P : (W'.baseChange K).Point) => (WeierstrassCurve.Affine.Point.map ↑σ) P }
Equations
- WeierstrassCurve.Affine.Point.instDistribMulActionAlgEquiv = { toSMul := WeierstrassCurve.Affine.Point.instSMulAlgEquiv, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
Equations
- WeierstrassCurve.Affine.Point.instSMulTorsionBy n = { smul := fun (σ : K ≃ₐ[S] K) (P : ↥(Submodule.torsionBy ℤ (W'.baseChange K).Point ↑n)) => ⟨σ • ↑P, ⋯⟩ }
Equations
- WeierstrassCurve.Affine.Point.instDistribMulActionTorsionBy n = { toSMul := WeierstrassCurve.Affine.Point.instSMulTorsionBy n, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
The torsion submodule is preserved by every automorphism of the coefficient field over the base.
Instances For
The torsion module is nontrivial and has no Galois-stable submodules other than bottom and top.
Equations
- One or more equations did not get rendered due to their size.