Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ProjectiveLine.lean

definition module

Projective line over a commutative ring; Borel subgroup of SL₂

Over a commutative ring R, a pair (a,c)\in R^2 is called a unimodular row, IsUnimodularRow a c, when it admits a Bézout relation: there exist x,y\in R with xa+yc=1. Two trivial instances are recorded, (1,t) and (m,1), together with the fact that unimodularity is preserved by any ring homomorphism f:R\to S, applied entrywise. The subtype UnimodularRow R consists of the pairs v\in R\times R satisfying this predicate, and unimodularRowSetoid R equips it with the equivalence relation v\sim w iff there is a unit u\in R^\times with u\,v_1=w_1 and u\,v_2=w_2; reflexivity, symmetry and transitivity come from 1, u^{-1} and products of units. The projective line ProjectiveLine R is defined to be the quotient of UnimodularRow R by this relation, so \mathbb{P}^1(R) is here the set of unimodular rows up to scaling by R^\times, a quotient of a chosen model by a congruence rather than an abstractly characterised object. It is finite whenever R is. Functoriality is provided by ProjectiveLine.map f, induced by entrywise application of a ring homomorphism f:R\to S (well defined because f carries units to units), with the expected description of its value on the class of a unimodular row.

The second section defines borel R, the subgroup of \mathrm{SL}_2(R) whose carrier is the set of matrices M with M_{1,0}=0 (indices in Fin 2), i.e. the upper-triangular matrices of determinant 1; closure under multiplication and inversion is checked from the explicit formulae for 2\times 2 products and for the inverse of an element of \mathrm{SL}_2. The membership criterion mem_borel_iff states that A\in borel R is exactly the condition A_{1,0}=0.

Relation to Mathlib

Mathlib's Projectivization is built for vector spaces over a division ring; the projective line of a commutative ring defined here is the project's own construction, as is the Borel subgroup of Matrix.SpecialLinearGroup (Fin 2) R.

Where it is used

These definitions serve the computation of the index of \Gamma_0(N): left cosets of borel in \mathrm{SL}_2(R) correspond to points of \mathbb{P}^1(R) through the class of the first column, and for R=\mathbb{Z}/N one has \#\mathbb{P}^1(\mathbb{Z}/N)=\psi(N), with \Gamma_0(N) the preimage of borel (ZMod N) under reduction.

References

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

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup ↗
import Mathlib.GroupTheory.GroupAction.Quotient ↗
import Mathlib.Data.Finite.Prod ↗

namespace ModularCurve

open Matrix
open scoped MatrixGroups

section ProjectiveLine

variable {R S : Type*} [CommRing R] [CommRing S]

def IsUnimodularRow (a c : R) : Prop :=
  ∃ x y : R, x * a + y * c = 1

theorem isUnimodularRow_one_left (t : R) : IsUnimodularRow (1 : R) t :=
  ⟨1, 0, by simp⟩

theorem isUnimodularRow_one_right (m : R) : IsUnimodularRow m (1 : R) :=
  ⟨0, 1, by simp⟩

theorem IsUnimodularRow.map (f : R →+* S) {a c : R} (h : IsUnimodularRow a c) :
    IsUnimodularRow (f a) (f c) := by
  obtain ⟨x, y, hxy⟩ := h
  exact ⟨f x, f y, by rw [← map_mul, ← map_mul, ← map_add, hxy, map_one]⟩

abbrev UnimodularRow (R : Type*) [CommRing R] := { v : R × R // IsUnimodularRow v.1 v.2 }

instance unimodularRowSetoid (R : Type*) [CommRing R] : Setoid (UnimodularRow R) where
  r v w := ∃ u : Rˣ, (u : R) * v.1.1 = w.1.1 ∧ (u : R) * v.1.2 = w.1.2
  iseqv := by
    refine ⟨fun v => ⟨1, by simp, by simp⟩, ?_, ?_⟩
    · rintro v w ⟨u, h1, h2⟩
      exact ⟨u⁻¹, by rw [← h1, Units.inv_mul_cancel_left],
        by rw [← h2, Units.inv_mul_cancel_left]⟩
    · rintro v w z ⟨u, h1, h2⟩ ⟨u', h1', h2'⟩
      exact ⟨u' * u, by rw [Units.val_mul, mul_assoc, h1, h1'],
        by rw [Units.val_mul, mul_assoc, h2, h2']⟩

def ProjectiveLine (R : Type*) [CommRing R] : Type _ :=
  Quotient (unimodularRowSetoid R)

instance instFiniteProjectiveLine [Finite R] : Finite (ProjectiveLine R) :=
  Quotient.finite _

def ProjectiveLine.map (f : R →+* S) : ProjectiveLine R → ProjectiveLine S :=
  Quotient.lift (fun v => (⟦⟨(f v.1.1, f v.1.2), v.2.map f⟩⟧ : ProjectiveLine S)) <| by
    rintro v w ⟨u, h1, h2⟩
    refine Quotient.sound ⟨⟨f u, f ↑u⁻¹, ?_, ?_⟩, ?_, ?_⟩
    · rw [← map_mul, Units.mul_inv, map_one]
    · rw [← map_mul, Units.inv_mul, map_one]
    · show f ↑u * f v.1.1 = f w.1.1
      rw [← map_mul, h1]
    · show f ↑u * f v.1.2 = f w.1.2
      rw [← map_mul, h2]

@[simp]
theorem ProjectiveLine.map_mk (f : R →+* S) (v : UnimodularRow R) :
    ProjectiveLine.map f ⟦v⟧ = ⟦⟨(f v.1.1, f v.1.2), v.2.map f⟩⟧ :=
  rfl

end ProjectiveLine

section Borel

variable {R : Type*} [CommRing R]

def borel (R : Type*) [CommRing R] : Subgroup (SpecialLinearGroup (Fin 2) R) where
  carrier := { M | M.1 1 0 = 0 }
  one_mem' := by
    show (1 : SpecialLinearGroup (Fin 2) R).1 1 0 = 0
    simp
  mul_mem' := by
    intro A B hA hB
    simp only [Set.mem_setOf_eq] at *
    show (A * B).1 1 0 = 0
    rw [SpecialLinearGroup.coe_mul, (Matrix.two_mul_expl A.1 B.1).2.2.1, hA, hB]
    ring
  inv_mem' := by
    intro A hA
    simp only [Set.mem_setOf_eq] at *
    show (A⁻¹).1 1 0 = 0
    rw [SpecialLinearGroup.SL2_inv_expl A]
    simp only [Matrix.cons_val_one, Matrix.cons_val_zero, neg_eq_zero]
    exact hA

theorem mem_borel_iff {A : SpecialLinearGroup (Fin 2) R} : A ∈ borel R ↔ A.1 1 0 = 0 :=
  Iff.rfl

end Borel

end ModularCurve

Statements phrased using this module (1)