Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_HeckeEis_BinaryFormRep.lean

definition module

Binary forms: substitution action and evaluation on the projective line

Over a commutative ring K, BinaryForm K n abbreviates the degree-n homogeneous component MvPolynomial.homogeneousSubmodule (Fin 2) K n, i.e. the submodule of K[X_0,X_1] spanned by the monomials of total degree n. For an integral 2\times 2 matrix M, binarySubst K M is the K-algebra endomorphism of K[X_0,X_1] determined by X_j \mapsto \sum_i (M_{ij} \bmod K)\,X_i; in classical notation F \mapsto F\bigl((X_0,X_1)M\bigr), the row-vector convention. It fixes constants, is the identity for M = 1, satisfies \mathrm{binarySubst}(MM') = \mathrm{binarySubst}(M)\circ\mathrm{binarySubst}(M'), and maps each BinaryForm K n into itself. Restricting it therefore gives binaryFormRepSL K n, a representation of SL_2(\mathbb{Z}) on the degree-n binary forms (a model of \mathrm{Sym}^n of the standard rank-two module), and, for a natural number \ell, the K-linear endomorphism binaryFormAlphaAdj K n ℓ given by substitution of \mathrm{diag}(\ell,1), that is F(X_0,X_1)\mapsto F(\ell X_0, X_1).

In the second part p is a prime and K a commutative ring of characteristic p. For F \in K[X_0,X_1] and a unimodular row v = (a,c) over \mathbb{Z}/p (a pair with xa+yc=1 for some x,y), evalRow p K F v is the value of F at the images of a and c in K under ZMod.castHom. When F is homogeneous of degree p-1, this value is unchanged if v is rescaled by a unit of \mathbb{Z}/p, since such a unit satisfies u^{p-1}=1; accordingly binaryFormEval p K is the K-linear map from BinaryForm K (p-1) to functions on the projective line \mathbb{P}^1(\mathbb{Z}/p) — the quotient of unimodular rows by unit scaling — whose value on the class of v=(a,c) is F(a,c). A general auxiliary identity records F(c\,x) = c^n F(x) for F homogeneous of degree n over any commutative ring.

Relation to Mathlib

BinaryForm is an abbreviation for Mathlib's MvPolynomial.homogeneousSubmodule, binarySubst is Mathlib's MvPolynomial.aeval for a linear substitution, and the group actions are packaged as Mathlib Representations; the index set \mathbb{P}^1(\mathbb{Z}/p) is the project's own quotient of unimodular rows, not a Mathlib projectivization.

Where it is used

These two coefficient modules, \mathrm{Sym}^{p-1} in characteristic p and the functions on \mathbb{P}^1(\mathbb{F}_p), together with the evaluation map intertwining the SL_2(\mathbb{Z})-actions and the \mathrm{diag}(\ell,1) operators, provide the dictionary between weight p+1 at level N and weight 2 at level Np that is used in the mod-p weight and level comparisons of the argument.

References

  1. A. Ash and G. Stevens, Modular forms in characteristic \ell and special values of their L-functions, Duke Mathematical Journal 53 (1986), 849–868
  2. B. Edixhoven, The weight in Serre's conjectures on modular forms, Inventiones Mathematicae 109 (1992), 563–594

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ProjectiveLineMatrixAction

namespace HeckeEis

open MvPolynomial ModularCurve
open scoped MatrixGroups

theorem eval_smul_of_isHomogeneous {σ : Type*} {R : Type*} [CommRing R] {φ : MvPolynomial σ R} {n : ℕ}
    (hφ : φ.IsHomogeneous n) (c : R) (x : σ → R) :
    MvPolynomial.eval (c • x) φ = c ^ n * MvPolynomial.eval x φ := by
  classical
  rw [MvPolynomial.eval_eq, MvPolynomial.eval_eq, Finset.mul_sum]
  refine Finset.sum_congr rfl fun d hd => ?_
  have hdeg : ∑ i ∈ d.support, d i = n := by
    have h := hφ (MvPolynomial.mem_support_iff.mp hd)
    simpa [Finsupp.degree, Finsupp.weight, Finsupp.sum, Finsupp.linearCombination, Finsupp.lsum] using h
  simp only [Pi.smul_apply, smul_eq_mul, mul_pow, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, hdeg]
  ring

section BinaryForms

variable (K : Type*) [CommRing K]

abbrev BinaryForm (n : ℕ) : Submodule K (MvPolynomial (Fin 2) K) :=
  MvPolynomial.homogeneousSubmodule (Fin 2) K n

noncomputable def binarySubst (M : Matrix (Fin 2) (Fin 2) ℤ) :
    MvPolynomial (Fin 2) K →ₐ[K] MvPolynomial (Fin 2) K :=
  MvPolynomial.aeval fun j => ∑ i : Fin 2, C ((M i j : ℤ) : K) * X i

theorem binarySubst_X (M : Matrix (Fin 2) (Fin 2) ℤ) (j : Fin 2) :
    binarySubst K M (X j) = ∑ i : Fin 2, C ((M i j : ℤ) : K) * X i :=
  MvPolynomial.aeval_X _ _

theorem binarySubst_C (M : Matrix (Fin 2) (Fin 2) ℤ) (r : K) : binarySubst K M (C r) = C r := by
  rw [binarySubst, MvPolynomial.aeval_C, MvPolynomial.algebraMap_eq]

theorem binarySubst_one : binarySubst K (1 : Matrix (Fin 2) (Fin 2) ℤ) = AlgHom.id K _ := by
  refine MvPolynomial.algHom_ext fun j => ?_
  rw [binarySubst_X, AlgHom.id_apply, Fin.sum_univ_two]
  fin_cases j <;> simp [Matrix.one_apply]

theorem binarySubst_mul (M M' : Matrix (Fin 2) (Fin 2) ℤ) :
    binarySubst K (M * M') = (binarySubst K M).comp (binarySubst K M') := by
  refine MvPolynomial.algHom_ext fun j => ?_
  rw [AlgHom.comp_apply, binarySubst_X, binarySubst_X]
  simp only [Fin.sum_univ_two, Matrix.mul_apply, map_add, map_mul, binarySubst_C, binarySubst_X,
    Int.cast_add, Int.cast_mul, C_mul]
  ring

theorem binarySubst_mem {n : ℕ} (M : Matrix (Fin 2) (Fin 2) ℤ) {F : MvPolynomial (Fin 2) K}
    (hF : F ∈ BinaryForm K n) : binarySubst K M F ∈ BinaryForm K n := by
  rw [MvPolynomial.mem_homogeneousSubmodule] at hF ⊢
  have h := hF.aeval (fun j => ∑ i : Fin 2, C ((M i j : ℤ) : K) * X i)
    (fun j => MvPolynomial.IsHomogeneous.sum _ _ _ fun i _ => (MvPolynomial.isHomogeneous_X K i).C_mul _)
  simpa only [binarySubst, one_mul] using h

variable (n : ℕ)

noncomputable def binaryFormRepSL : Representation K SL(2, ℤ) (BinaryForm K n) where
  toFun g := (binarySubst K (g : Matrix (Fin 2) (Fin 2) ℤ)).toLinearMap.restrict
    fun F hF => binarySubst_mem K _ hF
  map_one' := by
    refine LinearMap.ext fun F => Subtype.ext ?_
    change binarySubst K ((1 : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) F.1 = F.1
    rw [Matrix.SpecialLinearGroup.coe_one, binarySubst_one]
    rfl
  map_mul' g h := by
    refine LinearMap.ext fun F => Subtype.ext ?_
    change binarySubst K ((g * h : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) F.1
      = binarySubst K (g : Matrix (Fin 2) (Fin 2) ℤ) (binarySubst K (h : Matrix (Fin 2) (Fin 2) ℤ) F.1)
    rw [Matrix.SpecialLinearGroup.coe_mul, binarySubst_mul]
    rfl

@[simp]
theorem binaryFormRepSL_apply_coe (g : SL(2, ℤ)) (F : BinaryForm K n) :
    ((binaryFormRepSL K n g F : BinaryForm K n) : MvPolynomial (Fin 2) K)
      = binarySubst K (g : Matrix (Fin 2) (Fin 2) ℤ) F :=
  rfl

noncomputable def binaryFormAlphaAdj (ℓ : ℕ) : BinaryForm K n →ₗ[K] BinaryForm K n :=
  (binarySubst K !![(ℓ : ℤ), 0; 0, 1]).toLinearMap.restrict fun F hF => binarySubst_mem K _ hF

@[simp]
theorem binaryFormAlphaAdj_apply_coe (ℓ : ℕ) (F : BinaryForm K n) :
    ((binaryFormAlphaAdj K n ℓ F : BinaryForm K n) : MvPolynomial (Fin 2) K)
      = binarySubst K !![(ℓ : ℤ), 0; 0, 1] F :=
  rfl

end BinaryForms

section Eval

variable (p : ℕ) [Fact p.Prime] (K : Type*) [CommRing K] [CharP K p]

noncomputable def evalRow (F : MvPolynomial (Fin 2) K) (v : UnimodularRow (ZMod p)) : K :=
  MvPolynomial.eval ![ZMod.castHom (dvd_refl p) K v.1.1, ZMod.castHom (dvd_refl p) K v.1.2] F

theorem evalRow_eq_of_unit_mul {F : MvPolynomial (Fin 2) K} (hF : F ∈ BinaryForm K (p - 1))
    (u : (ZMod p)ˣ) (v w : UnimodularRow (ZMod p))
    (h1 : (u : ZMod p) * v.1.1 = w.1.1) (h2 : (u : ZMod p) * v.1.2 = w.1.2) :
    evalRow p K F w = evalRow p K F v := by
  have hu : (ZMod.castHom (dvd_refl p) K (u : ZMod p)) ^ (p - 1) = 1 := by
    rw [← map_pow, ZMod.pow_card_sub_one_eq_one (Units.ne_zero u), map_one]
  have hvec : (![ZMod.castHom (dvd_refl p) K w.1.1, ZMod.castHom (dvd_refl p) K w.1.2] : Fin 2 → K)
      = (ZMod.castHom (dvd_refl p) K (u : ZMod p)) •
          ![ZMod.castHom (dvd_refl p) K v.1.1, ZMod.castHom (dvd_refl p) K v.1.2] := by
    funext i
    fin_cases i <;> simp [← h1, ← h2, map_mul]
  unfold evalRow
  rw [hvec, eval_smul_of_isHomogeneous ((MvPolynomial.mem_homogeneousSubmodule _ _).mp hF), hu, one_mul]

noncomputable def binaryFormEval : BinaryForm K (p - 1) →ₗ[K] (ProjectiveLine (ZMod p) → K) where
  toFun F := Quotient.lift (evalRow p K (F : MvPolynomial (Fin 2) K)) fun v w hvw => by
    obtain ⟨u, h1, h2⟩ := hvw
    exact (evalRow_eq_of_unit_mul p K F.2 u v w h1 h2).symm
  map_add' F G := by
    funext P
    induction P using Quotient.inductionOn with
    | h v =>
      change evalRow p K ((F + G : BinaryForm K (p - 1)) : MvPolynomial (Fin 2) K) v
        = evalRow p K (F : MvPolynomial (Fin 2) K) v + evalRow p K (G : MvPolynomial (Fin 2) K) v
      simp [evalRow]
  map_smul' c F := by
    funext P
    induction P using Quotient.inductionOn with
    | h v =>
      change evalRow p K ((c • F : BinaryForm K (p - 1)) : MvPolynomial (Fin 2) K) v
        = c • evalRow p K (F : MvPolynomial (Fin 2) K) v
      simp [evalRow, MvPolynomial.smul_eval]

@[simp]
theorem binaryFormEval_mk (F : BinaryForm K (p - 1)) (v : UnimodularRow (ZMod p)) :
    binaryFormEval p K F (⟦v⟧ : ProjectiveLine (ZMod p)) = evalRow p K F v :=
  rfl

end Eval

end HeckeEis

Statements phrased using this module (84)