Definitions/Def_FreyPackage_GaloisRep.lean

For a Weierstrass curve W' in affine form over a commutative ring R, a commutative R-algebra S and a field K that is an S-algebra with R \to S \to K a scalar tower (plus a DecidableEq K instance), WeierstrassCurve.Affine.Point.galoisRep W' n is the mod-n representation attached to the n-torsion of the points of the base change W'\!\mathord{⁄}K. Concretely, the group K \simeq_{\mathrm{alg}[S]} K of S-algebra automorphisms of K acts on (W'⁄K).\mathrm{Point} by transport of coordinates along \sigma (the project's Point.map action), this action preserves the \mathbb{Z}-torsion submodule \mathrm{torsionBy}\ \mathbb{Z}\ (W'⁄K).\mathrm{Point}\ n = \{P : nP = 0\}, and that submodule carries a \mathbb{Z}/n-module structure because n annihilates it. The definition is then obtained by applying Mathlib's DistribMulAction.toModuleAut, so galoisRep W' n is a monoid homomorphism from K \simeq_{\mathrm{alg}[S]} K to the group of \mathbb{Z}/n-linear automorphisms of the n-torsion, and galoisRep_apply records that its value at \sigma is the map P \mapsto \sigma \bullet P. Nothing is asserted here about freeness of the n-torsion or finite-dimensionality, so the representation is not presented as a map into \mathrm{GL}_2(\mathbb{Z}/n); it is the abstract automorphism-group form.

FreyPackage.freyGaloisRep P is the specialisation to a Frey package P = (a,b,c,p): taking R = S = \mathbb{Q}, K = \overline{\mathbb{Q}} (an algebraic closure of \mathbb{Q}, given a classical decidable-equality instance), W' the Frey curve y^2 + xy = x^3 + \frac{b^p-1-a^p}{4}x^2 - \frac{a^pb^p}{16}x attached to P, and n = p, it is the monoid homomorphism from \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) to the \mathbb{Z}/p-linear automorphisms of the p-torsion of the Frey curve over \overline{\mathbb{Q}}.