Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_SL2Elementary.lean

definition module

Elementary unipotent matrices in

Over a commutative ring R, two families of elements of \mathrm{SL}(2,R) are defined: ModularCurve.upperElem c is the matrix \begin{pmatrix}1&c\\0&1\end{pmatrix} and ModularCurve.lowerElem c is the matrix \begin{pmatrix}1&0\\c&1\end{pmatrix}, each packaged with its determinant-one proof, together with the lemmas identifying the underlying 2\times 2 matrix of each. The arithmetic of these transvections is recorded: \mathrm{upperElem}(a)\,\mathrm{upperElem}(b)=\mathrm{upperElem}(a+b) and likewise for lowerElem, so that c\mapsto\mathrm{upperElem}(c) and c\mapsto\mathrm{lowerElem}(c) are homomorphisms from the additive group of R; the value at c=0 is the identity matrix; and the n-th power (n a natural number) is \mathrm{upperElem}(n\cdot a), respectively \mathrm{lowerElem}(n\cdot a), where n is taken in R via the canonical map.

The set ModularCurve.elemSet R is defined as the union of the ranges of upperElem and lowerElem, i.e. the subset of \mathrm{SL}(2,R) consisting of all upper and all lower unipotent matrices with arbitrary off-diagonal entry in R. Two further lemmas state that for every c\in R the elements \mathrm{upperElem}(c) and \mathrm{lowerElem}(c) lie in the subgroup generated by elemSet R; these are immediate from the definition of elemSet as that union, and serve as the interface by which later arguments about the subgroup \langle \mathrm{elemSet}\,R\rangle are used.

Relation to Mathlib

Mathlib supplies the group \mathrm{SL}(2,R) (Matrix.SpecialLinearGroup, with the SL(2, R) notation) and Subgroup.closure; the named transvections upperElem, lowerElem over an arbitrary commutative ring and the generating set elemSet are introduced by this development.

Where it is used

These elementary matrices are the generators used in the analysis of the image of a mod-p Galois representation: the standard criterion that a subgroup of \mathrm{GL}_2(\mathbb{F}_p) acting irreducibly and containing a nontrivial unipotent element contains all of \mathrm{SL}_2(\mathbb{F}_p) is proved by exhibiting the transvections, and the additive and power identities above are what drive that argument.

References

  1. J.-P. Serre, Propriétés galoisiennes des points d'ordre fini des courbes elliptiques, Inventiones Mathematicae 15 (1972), 259–331
  2. B. Mazur, Rational isogenies of prime degree, Inventiones Mathematicae 44 (1978), 129–162

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_SL2Elementary.lean

Declarations

Source

import Mathlib.LinearAlgebra.Matrix.FixedDetMatrices ↗
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs ↗
import Mathlib.GroupTheory.Index ↗
import Mathlib.Tactic.NoncommRing ↗

set_option autoImplicit false

open Matrix MatrixGroups Subgroup

namespace ModularCurve

section Elementary

variable {R : Type*} [CommRing R]

def upperElem (c : R) : SL(2, R) :=
  ⟨!![1, c; 0, 1], by simp [Matrix.det_fin_two_of]⟩

def lowerElem (c : R) : SL(2, R) :=
  ⟨!![1, 0; c, 1], by simp [Matrix.det_fin_two_of]⟩

@[simp] lemma upperElem_coe (c : R) :
    (upperElem c : Matrix (Fin 2) (Fin 2) R) = !![1, c; 0, 1] := rfl

@[simp] lemma lowerElem_coe (c : R) :
    (lowerElem c : Matrix (Fin 2) (Fin 2) R) = !![1, 0; c, 1] := rfl

lemma upperElem_mul (a b : R) : upperElem a * upperElem b = upperElem (a + b) := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two]
  ring

lemma lowerElem_mul (a b : R) : lowerElem a * lowerElem b = lowerElem (a + b) := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_two]

@[simp] lemma upperElem_zero : upperElem (0 : R) = 1 := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp

@[simp] lemma lowerElem_zero : lowerElem (0 : R) = 1 := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp

lemma upperElem_pow (a : R) (n : ℕ) : upperElem a ^ n = upperElem ((n : R) * a) := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ih, upperElem_mul]
    congr 1
    push_cast
    ring

lemma lowerElem_pow (a : R) (n : ℕ) : lowerElem a ^ n = lowerElem ((n : R) * a) := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ih, lowerElem_mul]
    congr 1
    push_cast
    ring

def elemSet (R : Type*) [CommRing R] : Set SL(2, R) :=
  Set.range upperElem ∪ Set.range lowerElem

lemma upperElem_mem_closure_elemSet (c : R) : upperElem c ∈ closure (elemSet R) :=
  subset_closure (Or.inl ⟨c, rfl⟩)

lemma lowerElem_mem_closure_elemSet (c : R) : lowerElem c ∈ closure (elemSet R) :=
  subset_closure (Or.inr ⟨c, rfl⟩)

end Elementary

end ModularCurve

Statements phrased using this module (4)