Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ProjectiveLineMatrixAction.lean

definition module

Matrix action on the projective line modulo

Over a commutative ring R, a unimodular row is a pair v=(v_1,v_2)\in R\times R together with a witness x,y of xv_1+yv_2=1, and \mathbb{P}^1(R) is the quotient of such rows by the relation 'w=uv for a unit u'. ModularCurve.ProjectiveLine.vecMulRow M hM sends a unimodular row v to vM=(v_1M_{00}+v_2M_{10},\,v_1M_{01}+v_2M_{11}) for a 2\times2 matrix M over R with \det M a unit, the unimodularity of the image being produced from a left inverse of the determinant; vecMulRow_fst/vecMulRow_snd record its two coordinates. This descends to the right action ModularCurve.ProjectiveLine.vecMul M hM on \mathbb{P}^1(R), with vecMul_one (v\cdot 1=v) and vecMul_mul (the action of MM' is the action of M followed by that of M').

In the HeckeEis namespace, redMat N M is the entrywise reduction of an integer matrix modulo N, and projLineAct N M is the induced self-map of \mathbb{P}^1(\mathbb{Z}/N): the above action of \mathrm{red}_N M when its determinant is a unit, and the identity otherwise, so as to be total; projLineAct_of_isUnit, isUnit_det_redMat_coe (determinants of reductions of \mathrm{SL}_2(\mathbb{Z})-matrices are units), projLineAct_one, projLineAct_mul and projLineAct_coe_mul give the expected unit and composition identities. For a commutative ring K, projLineRepSL N K is the resulting permutation representation of \mathrm{SL}_2(\mathbb{Z}) on functions \mathbb{P}^1(\mathbb{Z}/N)\to K, (g\cdot f)(P)=f(P\cdot g), and projLineRep N K its restriction along the inclusion of the subgroup \Gamma_0(1); projLineAlphaAdj N K \ell is precomposition with the action of \mathrm{diag}(\ell,1), the adjugate of \mathrm{diag}(1,\ell). Finally projLineFixedCard N M is the number of points of \mathbb{P}^1(\mathbb{Z}/N) fixed by projLineAct N M; projLineCuspSetoid N is the equivalence relation generated by P\mapsto P\cdot\begin{pmatrix}1&1\\0&1\end{pmatrix}, with quotient ProjLineCusps N (finite for N\neq0), class map projLineCuspMk, and fixedCuspCount N M the number of classes c such that every P in c has P\cdot M again in c.

Relation to Mathlib

Mathlib's Projectivization is built for modules over division rings; the projective line over a commutative ring as a quotient of unimodular rows, and the matrix action on it defined here, are the project's own. The representations are Mathlib Representations of Mathlib's SL(2, ℤ) and CongruenceSubgroup.Gamma0 1.

Where it is used

Under the bottom-row dictionary between \Gamma_0(N)\backslash\mathrm{SL}_2(\mathbb{Z}) and \mathbb{P}^1(\mathbb{Z}/N), these actions and the representation on K-valued functions on \mathbb{P}^1(\mathbb{Z}/N) provide the coefficient module in which level-N data is handled at level one, together with the combinatorics of cusps (\begin{pmatrix}1&1\\0&1\end{pmatrix}-orbits) and fixed-point counts needed for Hecke operators.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §3.8
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, §1.6

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_ProjectiveLine

namespace ModularCurve.ProjectiveLine

variable {R : Type*} [CommRing R]

def vecMulRow (M : Matrix (Fin 2) (Fin 2) R) (hM : IsUnit M.det) (v : UnimodularRow R) :
    UnimodularRow R :=
  ⟨(v.1.1 * M 0 0 + v.1.2 * M 1 0, v.1.1 * M 0 1 + v.1.2 * M 1 1), by
    obtain ⟨x, y, h⟩ := v.2
    obtain ⟨e, he⟩ := hM.exists_left_inv
    rw [Matrix.det_fin_two] at he
    exact ⟨e * (x * M 1 1 - y * M 0 1), e * (y * M 0 0 - x * M 1 0), by
      linear_combination (x * v.1.1 + y * v.1.2) * he + h⟩⟩

@[simp]
theorem vecMulRow_fst (M : Matrix (Fin 2) (Fin 2) R) (hM : IsUnit M.det) (v : UnimodularRow R) :
    (vecMulRow M hM v).1.1 = v.1.1 * M 0 0 + v.1.2 * M 1 0 :=
  rfl

@[simp]
theorem vecMulRow_snd (M : Matrix (Fin 2) (Fin 2) R) (hM : IsUnit M.det) (v : UnimodularRow R) :
    (vecMulRow M hM v).1.2 = v.1.1 * M 0 1 + v.1.2 * M 1 1 :=
  rfl

def vecMul (M : Matrix (Fin 2) (Fin 2) R) (hM : IsUnit M.det) : ProjectiveLine R → ProjectiveLine R :=
  Quotient.map (vecMulRow M hM) <| by
    rintro v w ⟨u, h1, h2⟩
    refine ⟨u, ?_, ?_⟩
    · simp only [vecMulRow_fst]
      linear_combination M 0 0 * h1 + M 1 0 * h2
    · simp only [vecMulRow_snd]
      linear_combination M 0 1 * h1 + M 1 1 * h2

@[simp]
theorem vecMul_mk (M : Matrix (Fin 2) (Fin 2) R) (hM : IsUnit M.det) (v : UnimodularRow R) :
    vecMul M hM (⟦v⟧ : ProjectiveLine R) = ⟦vecMulRow M hM v⟧ :=
  rfl

theorem vecMul_one (h : IsUnit (1 : Matrix (Fin 2) (Fin 2) R).det) (P : ProjectiveLine R) :
    vecMul 1 h P = P := by
  induction P using Quotient.inductionOn with
  | h v =>
    rw [vecMul_mk]
    congr 1
    apply Subtype.ext
    refine Prod.ext ?_ ?_ <;> simp

theorem vecMul_mul (M M' : Matrix (Fin 2) (Fin 2) R) (hM : IsUnit M.det) (hM' : IsUnit M'.det)
    (hMM' : IsUnit (M * M').det) (P : ProjectiveLine R) :
    vecMul (M * M') hMM' P = vecMul M' hM' (vecMul M hM P) := by
  induction P using Quotient.inductionOn with
  | h v =>
    simp only [vecMul_mk]
    congr 1
    apply Subtype.ext
    refine Prod.ext ?_ ?_
    · simp only [vecMulRow_fst, vecMulRow_snd, Matrix.mul_apply, Fin.sum_univ_two]
      ring
    · simp only [vecMulRow_fst, vecMulRow_snd, Matrix.mul_apply, Fin.sum_univ_two]
      ring

end ModularCurve.ProjectiveLine

namespace HeckeEis

open ModularCurve
open scoped MatrixGroups

abbrev redMat (N : ℕ) (M : Matrix (Fin 2) (Fin 2) ℤ) : Matrix (Fin 2) (Fin 2) (ZMod N) :=
  M.map (Int.castRingHom (ZMod N))

noncomputable def projLineAct (N : ℕ) (M : Matrix (Fin 2) (Fin 2) ℤ) :
    ProjectiveLine (ZMod N) → ProjectiveLine (ZMod N) :=
  open scoped Classical in
  if h : IsUnit (redMat N M).det then ProjectiveLine.vecMul (redMat N M) h else id

theorem projLineAct_of_isUnit (N : ℕ) (M : Matrix (Fin 2) (Fin 2) ℤ) (h : IsUnit (redMat N M).det) :
    projLineAct N M = ProjectiveLine.vecMul (redMat N M) h := by
  classical
  rw [projLineAct, dif_pos h]

theorem isUnit_det_redMat_coe (N : ℕ) (g : SL(2, ℤ)) : IsUnit (redMat N (g : Matrix (Fin 2) (Fin 2) ℤ)).det := by
  have : (redMat N (g : Matrix (Fin 2) (Fin 2) ℤ)).det = 1 := by
    rw [redMat, ← RingHom.mapMatrix_apply, ← RingHom.map_det, g.det_coe, map_one]
  rw [this]
  exact isUnit_one

@[simp]
theorem projLineAct_one (N : ℕ) (P : ProjectiveLine (ZMod N)) : projLineAct N 1 P = P := by
  have h1 : redMat N 1 = 1 := by simp [redMat]
  have h : IsUnit (redMat N (1 : Matrix (Fin 2) (Fin 2) ℤ)).det := by rw [h1, Matrix.det_one]; exact isUnit_one
  rw [projLineAct_of_isUnit N 1 h]
  have h' : IsUnit (1 : Matrix (Fin 2) (Fin 2) (ZMod N)).det := by rw [Matrix.det_one]; exact isUnit_one
  rw [show ProjectiveLine.vecMul (redMat N 1) h = ProjectiveLine.vecMul 1 h' from by congr 1]
  exact ProjectiveLine.vecMul_one h' P

theorem projLineAct_mul (N : ℕ) (M M' : Matrix (Fin 2) (Fin 2) ℤ)
    (hM : IsUnit (redMat N M).det) (hM' : IsUnit (redMat N M').det) (P : ProjectiveLine (ZMod N)) :
    projLineAct N (M * M') P = projLineAct N M' (projLineAct N M P) := by
  have hmul : redMat N (M * M') = redMat N M * redMat N M' := by
    rw [redMat, redMat, redMat, ← RingHom.mapMatrix_apply, ← RingHom.mapMatrix_apply,
      ← RingHom.mapMatrix_apply, map_mul]
  have hMM' : IsUnit (redMat N (M * M')).det := by
    rw [hmul, Matrix.det_mul]
    exact hM.mul hM'
  rw [projLineAct_of_isUnit N _ hMM', projLineAct_of_isUnit N _ hM, projLineAct_of_isUnit N _ hM']
  have hMM'2 : IsUnit (redMat N M * redMat N M').det := by rw [← hmul]; exact hMM'
  rw [show ProjectiveLine.vecMul (redMat N (M * M')) hMM' = ProjectiveLine.vecMul _ hMM'2 from by
    congr 1]
  exact ProjectiveLine.vecMul_mul _ _ hM hM' hMM'2 P

theorem projLineAct_coe_mul (N : ℕ) (g h : SL(2, ℤ)) (P : ProjectiveLine (ZMod N)) :
    projLineAct N ((g * h : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) P
      = projLineAct N (h : Matrix (Fin 2) (Fin 2) ℤ) (projLineAct N (g : Matrix (Fin 2) (Fin 2) ℤ) P) := by
  rw [Matrix.SpecialLinearGroup.coe_mul]
  exact projLineAct_mul N _ _ (isUnit_det_redMat_coe N g) (isUnit_det_redMat_coe N h) P

section Rep

variable (N : ℕ) (K : Type*) [CommRing K]

noncomputable def projLineRepSL : Representation K SL(2, ℤ) (ProjectiveLine (ZMod N) → K) where
  toFun g := LinearMap.funLeft K K (projLineAct N (g : Matrix (Fin 2) (Fin 2) ℤ))
  map_one' := by
    apply LinearMap.ext
    intro f
    funext P
    simp [LinearMap.funLeft_apply, projLineAct_one]
  map_mul' g h := by
    apply LinearMap.ext
    intro f
    funext P
    simp only [LinearMap.funLeft_apply, Module.End.mul_apply, projLineAct_coe_mul]

@[simp]
theorem projLineRepSL_apply (g : SL(2, ℤ)) (f : ProjectiveLine (ZMod N) → K) (P : ProjectiveLine (ZMod N)) :
    projLineRepSL N K g f P = f (projLineAct N (g : Matrix (Fin 2) (Fin 2) ℤ) P) :=
  rfl

noncomputable def projLineRep :
    Representation K (CongruenceSubgroup.Gamma0 1) (ProjectiveLine (ZMod N) → K) :=
  (projLineRepSL N K).comp (CongruenceSubgroup.Gamma0 1).subtype

@[simp]
theorem projLineRep_apply (g : CongruenceSubgroup.Gamma0 1) (f : ProjectiveLine (ZMod N) → K)
    (P : ProjectiveLine (ZMod N)) :
    projLineRep N K g f P = f (projLineAct N ((g : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) P) :=
  rfl

noncomputable def projLineAlphaAdj (ℓ : ℕ) :
    (ProjectiveLine (ZMod N) → K) →ₗ[K] (ProjectiveLine (ZMod N) → K) :=
  LinearMap.funLeft K K (projLineAct N !![(ℓ : ℤ), 0; 0, 1])

@[simp]
theorem projLineAlphaAdj_apply (ℓ : ℕ) (f : ProjectiveLine (ZMod N) → K) (P : ProjectiveLine (ZMod N)) :
    projLineAlphaAdj N K ℓ f P = f (projLineAct N !![(ℓ : ℤ), 0; 0, 1] P) :=
  rfl

end Rep

noncomputable def projLineFixedCard (N : ℕ) (M : Matrix (Fin 2) (Fin 2) ℤ) : ℕ :=
  Nat.card {P : ProjectiveLine (ZMod N) // projLineAct N M P = P}

def projLineCuspSetoid (N : ℕ) : Setoid (ProjectiveLine (ZMod N)) :=
  Relation.EqvGen.setoid fun P Q => projLineAct N !![1, 1; 0, 1] P = Q

def ProjLineCusps (N : ℕ) : Type _ :=
  Quotient (projLineCuspSetoid N)

def projLineCuspMk (N : ℕ) (P : ProjectiveLine (ZMod N)) : ProjLineCusps N :=
  Quotient.mk (projLineCuspSetoid N) P

instance instFiniteProjLineCusps (N : ℕ) [NeZero N] : Finite (ProjLineCusps N) :=
  Quotient.finite _

noncomputable def fixedCuspCount (N : ℕ) (M : Matrix (Fin 2) (Fin 2) ℤ) : ℕ :=
  Nat.card {c : ProjLineCusps N //
    ∀ P : ProjectiveLine (ZMod N), projLineCuspMk N P = c → projLineCuspMk N (projLineAct N M P) = c}

end HeckeEis

Statements phrased using this module (7)