Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_PeriodMap.lean

definition module

Equivariant primitives, period characters, parabolic homomorphisms

Fix a subgroup \Gamma \le \mathrm{SL}_2(\mathbb{Z}) acting on the upper half plane \mathbb{H} by Möbius transformations, and a function F : \mathbb{H} \to \mathbb{C}. The predicate ModularCurve.Period.IsEquivariantPrimitive Γ F asserts that for every \gamma \in \Gamma there is a constant c \in \mathbb{C} with F(\gamma \cdot z) - F(z) = c for all z \in \mathbb{H}, i.e. that each coboundary of F is constant on \mathbb{H}. Given such an F, the period IsEquivariantPrimitive.period hF γ is defined concretely as the value F(\gamma \cdot i) - F(i) at the point i \in \mathbb{H}; sub_eq_period then says that F(\gamma \cdot z) - F(z) equals this number for every z, so the base point is immaterial. From this, period_one gives \mathrm{per}(1) = 0 and period_mul gives the additivity \mathrm{per}(\gamma\delta) = \mathrm{per}(\gamma) + \mathrm{per}(\delta); periodHom packages these as an additive group homomorphism Additive Γ →+ ℂ — the multiplicative group \Gamma viewed additively — whose value at \gamma is \mathrm{per}(\gamma) (periodHom_apply). Thus characters of \Gamma with values in a trivial module are modelled throughout as maps of type Additive Γ →+ A.

For an abelian group A, the predicate ModularCurve.Period.IsParabolicHom Γ φ on such a homomorphism \varphi : Additive Γ →+ A asserts that \varphi(\gamma) = 0 whenever the underlying integer matrix of \gamma \in \Gamma satisfies \mathrm{tr}(\gamma)^2 = 4; the elements so constrained are exactly \pm 1 together with the parabolic elements of \Gamma. For a semiring R and an R-module structure on A, ModularCurve.Period.parabolicHoms R Γ A is the R-submodule of Additive Γ →+ A cut out by this vanishing condition, with mem_parabolicHoms_iff recording that membership is precisely the predicate; it is the parabolic part of \mathrm{Hom}(\Gamma, A) = H^1(\Gamma, A) for trivial coefficients.

Relation to Mathlib

Built on Mathlib's Möbius action of \mathrm{SL}(2,\mathbb{Z}) on the upper half plane and on Additive to regard group homomorphisms out of \Gamma additively; the notions of equivariant primitive, period character and parabolic homomorphism are the project's own.

Where it is used

These definitions provide the group-cohomological language on the modular-curve side of the argument: period characters of primitives of weight-two forms, and the parabolic submodule of \mathrm{Hom}(\Gamma, A) that models H^1_{\mathrm{par}}(\Gamma, A), i.e. the first cohomology of the compactified modular curve with trivial coefficients.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Chapter 8

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction ↗
import Mathlib.Algebra.Module.Hom ↗

namespace ModularCurve.Period

open UpperHalfPlane

open scoped MatrixGroups

variable (Γ : Subgroup SL(2, ℤ)) (F : ℍ → ℂ)

def IsEquivariantPrimitive : Prop :=
  ∀ γ : Γ, ∃ c : ℂ, ∀ z : ℍ, F ((γ : SL(2, ℤ)) • z) - F z = c

def IsParabolicHom {A : Type*} [AddCommGroup A] (φ : Additive Γ →+ A) : Prop :=
  ∀ γ : Γ, ((γ : SL(2, ℤ)) : Matrix (Fin 2) (Fin 2) ℤ).trace ^ 2 = 4 → φ (Additive.ofMul γ) = 0

variable {Γ F}

namespace IsEquivariantPrimitive

noncomputable def period (_hF : IsEquivariantPrimitive Γ F) (γ : Γ) : ℂ :=
  F ((γ : SL(2, ℤ)) • UpperHalfPlane.I) - F UpperHalfPlane.I

theorem sub_eq_period (hF : IsEquivariantPrimitive Γ F) (γ : Γ) (z : ℍ) :
    F ((γ : SL(2, ℤ)) • z) - F z = hF.period γ := by
  obtain ⟨c, hc⟩ := hF γ
  rw [hc z, period, hc UpperHalfPlane.I]

@[simp]
theorem period_one (hF : IsEquivariantPrimitive Γ F) : hF.period 1 = 0 := by
  have h := hF.sub_eq_period 1 UpperHalfPlane.I
  simpa using h.symm

theorem period_mul (hF : IsEquivariantPrimitive Γ F) (γ δ : Γ) :
    hF.period (γ * δ) = hF.period γ + hF.period δ := by
  have h1 := hF.sub_eq_period (γ * δ) UpperHalfPlane.I
  have h2 := hF.sub_eq_period γ ((δ : SL(2, ℤ)) • UpperHalfPlane.I)
  have h3 := hF.sub_eq_period δ UpperHalfPlane.I
  have hsmul : ((γ * δ : Γ) : SL(2, ℤ)) • UpperHalfPlane.I
      = (γ : SL(2, ℤ)) • ((δ : SL(2, ℤ)) • UpperHalfPlane.I) := by
    rw [← mul_smul]; rfl
  rw [hsmul] at h1
  linear_combination h2 + h3 - h1

noncomputable def periodHom (hF : IsEquivariantPrimitive Γ F) : Additive Γ →+ ℂ where
  toFun γ := hF.period (Additive.toMul γ)
  map_zero' := hF.period_one
  map_add' γ δ := hF.period_mul (Additive.toMul γ) (Additive.toMul δ)

@[simp]
theorem periodHom_apply (hF : IsEquivariantPrimitive Γ F) (γ : Γ) :
    hF.periodHom (Additive.ofMul γ) = hF.period γ :=
  rfl

end IsEquivariantPrimitive

section ParabolicHoms

variable (R : Type*) [Semiring R] (Γ : Subgroup SL(2, ℤ)) (A : Type*) [AddCommGroup A] [Module R A]

def parabolicHoms : Submodule R (Additive Γ →+ A) where
  carrier := {φ | IsParabolicHom Γ φ}
  zero_mem' := fun _ _ => rfl
  add_mem' := by
    intro φ ψ hφ hψ γ hγ
    show φ (Additive.ofMul γ) + ψ (Additive.ofMul γ) = 0
    rw [hφ γ hγ, hψ γ hγ, add_zero]
  smul_mem' := by
    intro c φ hφ γ hγ
    show c • φ (Additive.ofMul γ) = 0
    rw [hφ γ hγ, smul_zero]

variable {R Γ A}

theorem mem_parabolicHoms_iff {φ : Additive Γ →+ A} : φ ∈ parabolicHoms R Γ A ↔ IsParabolicHom Γ φ :=
  Iff.rfl

end ParabolicHoms

end ModularCurve.Period

Statements phrased using this module (117)