Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_MultiplicativeType.lean

definition module

Multiplicative-type action: subgroup acting by a character scalar

The module fixes a group G, a commutative ring R, and an additive commutative group J carrying both an R-module structure and a distributive multiplicative G-action (no compatibility between the two actions is imposed, and nothing about J beyond these typeclasses is used). Two predicates are defined, both purely pointwise conditions on a chosen subobject.

ModularCurve.MultiplicativeType I χ W takes a subgroup I \le G, a monoid homomorphism \chi : G \to R^\times, and an R-submodule W \subseteq J, and asserts: for every \sigma \in I and every x \in W, \sigma \cdot x = \chi(\sigma) \cdot x, where the unit \chi(\sigma) is coerced to R and acts through the module structure. Thus the G-action, restricted to I and to vectors of W, is scalar multiplication by the character \chi. Only the restriction of \chi to I enters, and G-stability of W is not a separate hypothesis: it is a consequence pointwise, since \chi(\sigma)\cdot x lies in W.

ModularCurve.MultiplicativeTypeNat I n W is the ring-free variant: n is an arbitrary function G \to \mathbb{N} (not required to be multiplicative or a homomorphism), W is merely an additive subgroup of J, and the condition is that \sigma \cdot x = n(\sigma) \cdot x for all \sigma \in I, x \in W, with n(\sigma) \cdot x the \mathbb{N}-scalar multiple, i.e. the iterated sum x + \cdots + x. This version mentions neither R nor the module structure on J, so it transports along bare additive maps. Both are predicates on the given data (I, \chi or n, W); neither asserts the existence of such a W or of such a character.

Relation to Mathlib

Mathlib has no predicate for "a subgroup acts on a submodule through a given character"; these are the project's own definitions, stated using Mathlib's Subgroup, Submodule, AddSubgroup, Module and DistribMulAction. Despite the ModularCurve namespace, the definitions are stated for a completely general group action on a module.

Where it is used

These predicates record the behaviour of a decomposition or inertia group on a distinguished part of the torsion of a Jacobian: the condition that inertia at p act on the multiplicative (toric) part through the mod p cyclotomic character, as opposed to acting trivially, which is the form taken by the local condition at primes away from p. They are imported by some thirty statement modules of the tree, where they supply the local hypotheses at p in the semistable-reduction package feeding into the level-lowering and Galois-representation arguments; the \mathbb{N}-valued variant is used where the comparison is made along an additive map with no module compatibility available.

References

  1. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316
  2. J.-P. Serre, Sur les représentations modulaires de degré 2 de \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), Duke Mathematical Journal 54 (1987), 179–230
  3. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_ModularCurve_MultiplicativeType.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.Algebra.Module.Submodule.Basic ↗
import Mathlib.Algebra.Group.Subgroup.Basic ↗

namespace ModularCurve

variable {G : Type*} [Group G] {R : Type*} [CommRing R]
  {J : Type*} [AddCommGroup J] [Module R J] [DistribMulAction G J]

def MultiplicativeType (I : Subgroup G) (χ : G →* Rˣ) (W : Submodule R J) : Prop :=
  ∀ σ ∈ I, ∀ x ∈ W, σ • x = (χ σ : R) • x

def MultiplicativeTypeNat (I : Subgroup G) (n : G → ℕ) (W : AddSubgroup J) : Prop :=
  ∀ σ ∈ I, ∀ x ∈ W, σ • x = n σ • x

end ModularCurve

Statements phrased using this module (12)