Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_X0MqResolvedTable.lean

definition module

Component table of the resolved special fibre of

Fix a finite type \iota and a function e : \iota \to \mathbb{N}. ModularCurve.X0MqComponents e is the index type \mathrm{Fin}\,2 \oplus \bigl(\Sigma_{x:\iota}\,\mathrm{Fin}(e_x-1)\bigr): two distinguished components, written here Z_0, Z_1, together with, for each x \in \iota, a chain of e_x - 1 further components indexed by 0,\dots,e_x-2 (truncated natural subtraction, so e_x \le 1 contributes nothing).

ModularCurve.x0MqAdj e is the \mathbb{N}-valued adjacency function on this index type: a(Z_i,Z_j) for i \ne j is the number of x \in \iota with e_x = 1, and a(Z_i,Z_i) = 0; a(Z_i,(x,k)) = a((x,k),Z_i) equals 1 exactly when i = 0 and k = 0, or i = 1 and k = e_x - 2, and is 0 otherwise; a((x,k),(x',k')) equals 1 exactly when x = x' and k,k' are consecutive, so that in particular the diagonal vanishes. The lemma ModularCurve.x0MqAdj_symm records that a is symmetric.

ModularCurve.x0MqResolvedTable e is the resulting term of the project's structure MazurRapoportAppendix.SpecialFibreComponentTable: all multiplicities are 1, and the intersection pairing is \mathrm{inter}(i,j) = a(i,j) for i \ne j and \mathrm{inter}(i,i) = -\sum_{j} a(i,j). The structure's fields are discharged as part of the definition: positivity of the multiplicities, symmetry of the pairing, and the relation \sum_j \mathrm{inter}(i,j)\,\mathrm{mult}(j) = 0 for every i, which here reduces to the fact that each row of \mathrm{inter} sums to zero. No geometric interpretation is asserted: the declarations produce purely combinatorial data of the shape required by the component-group machinery.

Relation to Mathlib

Mathlib has no notion of a special-fibre component table or of the associated component group; SpecialFibreComponentTable is the project's own structure, and this module supplies one particular such table.

Where it is used

This table is the combinatorial input to the Mazur–Rapoport construction of MazurRapoportAppendix.AppendixComponentGroup, the quotient \ker\beta / \operatorname{im}\alpha attached to a component table. The shape chosen here — two components meeting at the points x with e_x = 1, joined by chains of length e_x - 1 elsewhere — is that of the minimal regular model of X_0(Mq) at q, whose component group enters the level-lowering step.

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. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  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_X0MqResolvedTable.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicGeometry_MazurRapoportAppendixPicNeronCarriers

set_option autoImplicit false

namespace ModularCurve
open MazurRapoportAppendix

variable {ι : Type*} [Fintype ι] [DecidableEq ι]

abbrev X0MqComponents (e : ι → ℕ) : Type _ := Fin 2 ⊕ (Σ x : ι, Fin (e x - 1))

def x0MqAdj (e : ι → ℕ) : X0MqComponents e → X0MqComponents e → ℕ
  | .inl i, .inl j => if i ≠ j then (Finset.univ.filter fun x => e x = 1).card else 0
  | .inl i, .inr p => if (i = 0 ∧ p.2.val = 0) ∨ (i = 1 ∧ p.2.val = e p.1 - 2) then 1 else 0
  | .inr p, .inl i => if (i = 0 ∧ p.2.val = 0) ∨ (i = 1 ∧ p.2.val = e p.1 - 2) then 1 else 0
  | .inr p, .inr p' => if p.1 = p'.1 ∧ (p.2.val + 1 = p'.2.val ∨ p'.2.val + 1 = p.2.val) then 1 else 0

theorem x0MqAdj_symm (e : ι → ℕ) (i j : X0MqComponents e) : x0MqAdj e i j = x0MqAdj e j i := by
  rcases i with i | p <;> rcases j with j | p'
  · simp only [x0MqAdj, ne_comm]
  · rfl
  · rfl
  · simp only [x0MqAdj]
    congr 1
    apply propext
    constructor
    · rintro ⟨h1, h2⟩; exact ⟨h1.symm, h2.symm⟩
    · rintro ⟨h1, h2⟩; exact ⟨h1.symm, h2.symm⟩

def x0MqResolvedTable (e : ι → ℕ) :
    SpecialFibreComponentTable (X0MqComponents e) where
  mult _ := 1
  inter i j := (x0MqAdj e i j : ℤ) - if i = j then ∑ j', (x0MqAdj e i j' : ℤ) else 0
  mult_pos _ := Nat.one_pos
  inter_symm i j := by
    by_cases h : i = j
    · subst h; rfl
    · rw [if_neg h, if_neg (Ne.symm h), x0MqAdj_symm]
  fibre_inter_zero i := by
    simp only [Nat.cast_one, mul_one, Finset.sum_sub_distrib, Finset.sum_ite_eq, Finset.mem_univ, if_true, sub_self]

end ModularCurve

Statements phrased using this module (42)