Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_Gamma0FundamentalSet.lean

definition module

Fundamental sets for subgroups of on

For a subgroup \Gamma \le SL(2,\mathbb Z), gammaFundamentalSet is the subset of the upper half plane obtained as the union, over all cosets q \in SL(2,\mathbb Z)/\Gamma, of g_q^{-1}\cdot\mathcal D, where \mathcal D is Mathlib's standard fundamental domain ModularGroup.fd for the full modular group and g_q is the chosen representative Quotient.out q of the coset. Thus z lies in the set exactly when g_q\cdot z \in \mathcal D for some coset q (mem_gammaFundamentalSet_iff). No disjointness of the translates is asserted: what is proved is the covering property that every z \in \mathbb H has some \gamma \in \Gamma with \gamma\cdot z in the set, and, when the quotient SL(2,\mathbb Z)/\Gamma is finite, the identification of the set with a finite union \bigcup_{\gamma\in S}\gamma\cdot\mathcal D over the finite set S of inverse coset representatives. Measure-theoretically, the hyperbolic volume of gammaFundamentalSet Γ is always strictly positive, and is finite whenever SL(2,\mathbb Z)/\Gamma is finite, hence lies strictly between 0 and \mathrm{vol}(\mathbb H) = \infty; for \Gamma = \top the volume equals \mathrm{vol}(\mathcal D). These statements are specialised to \Gamma = \Gamma_0(N) with N \ne 0, where finiteness of the quotient comes from finiteness of the index.

The companion definition truncatedGammaFundamentalSet Γ y replaces \mathcal D in the same coset union by truncatedFundamentalDomain y, the part of \mathcal D whose imaginary part is bounded by y; it is contained in gammaFundamentalSet Γ, it is compact when SL(2,\mathbb Z)/\Gamma is finite (in particular for \Gamma_0(N)), and it is nonempty for y = 2, witnessed by the translate of \rho (of imaginary part \sqrt 3/2). The module also records the continuity of the action of each fixed element of SL(2,\mathbb Z) on \mathbb H, obtained from the GL_2(\mathbb R)-action through Matrix.SpecialLinearGroup.mapGL.

Relation to Mathlib

Mathlib supplies the standard fundamental domain \mathcal D for SL(2,\mathbb Z), its truncations, the hyperbolic measure on \mathbb H and the congruence subgroups Gamma0; the coset union attached to an arbitrary subgroup, together with its positivity, finiteness of volume and compactness of the truncation, is the project's own. A ContinuousConstSMul SL(2, ℤ) ℍ instance is registered here.

Where it is used

These fundamental sets provide the geometric base for the analytic theory of modular forms of level N: finiteness of the covolume of \Gamma_0(N) and compactness of truncated fundamental sets are the starting points for integration and spectral arguments on \Gamma_0(N)\backslash\mathbb H used in the modularity input to Fermat's Last Theorem.

References

  1. H. Iwaniec, Spectral Methods of Automorphic Forms, Graduate Studies in Mathematics 53, American Mathematical Society, 2002, Chapter 2
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, Chapter 2
  3. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, Chapter 1

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AutomorphicForm_FundamentalDomainVolume
import Definitions.Def_AutomorphicForm_SiegelSetCover

set_option autoImplicit false

open Matrix Matrix.SpecialLinearGroup UpperHalfPlane ModularGroup CongruenceSubgroup
open MeasureTheory
open scoped Modular MatrixGroups Pointwise

namespace FLT.Gamma0FundamentalSet

def gammaFundamentalSet (Γ : Subgroup SL(2, ℤ)) : Set ℍ :=
  ⋃ q : SL(2, ℤ) ⧸ Γ, (Quotient.out q)⁻¹ • 𝒟

theorem mem_gammaFundamentalSet_iff {Γ : Subgroup SL(2, ℤ)} {z : ℍ} :
    z ∈ gammaFundamentalSet Γ ↔ ∃ q : SL(2, ℤ) ⧸ Γ, Quotient.out q • z ∈ 𝒟 := by
  simp only [gammaFundamentalSet, Set.mem_iUnion, Set.mem_inv_smul_set_iff]

theorem exists_smul_mem_gammaFundamentalSet (Γ : Subgroup SL(2, ℤ)) (z : ℍ) :
    ∃ γ ∈ Γ, γ • z ∈ gammaFundamentalSet Γ :=
  FLT.SiegelSetCover.exists_smul_mem_iUnion_smul_fd Γ z

theorem gammaFundamentalSet_eq_biUnion (Γ : Subgroup SL(2, ℤ)) [Finite (SL(2, ℤ) ⧸ Γ)] :
    haveI : Fintype (SL(2, ℤ) ⧸ Γ) := Fintype.ofFinite _
    gammaFundamentalSet Γ =
      ⋃ γ ∈ (Finset.univ.image fun q : SL(2, ℤ) ⧸ Γ => (Quotient.out q)⁻¹), γ • 𝒟 := by
  haveI : Fintype (SL(2, ℤ) ⧸ Γ) := Fintype.ofFinite _
  ext z
  simp only [gammaFundamentalSet, Set.mem_iUnion, Finset.mem_image, Finset.mem_univ,
    true_and]
  exact ⟨fun ⟨q, hq⟩ => ⟨_, ⟨q, rfl⟩, hq⟩, fun ⟨γ, ⟨q, hq⟩, hz⟩ => ⟨q, hq ▸ hz⟩⟩

theorem volume_gammaFundamentalSet_lt_top (Γ : Subgroup SL(2, ℤ))
    [Finite (SL(2, ℤ) ⧸ Γ)] : volume (gammaFundamentalSet Γ) < ⊤ := by
  haveI : Fintype (SL(2, ℤ) ⧸ Γ) := Fintype.ofFinite _
  rw [gammaFundamentalSet_eq_biUnion Γ]
  exact FLT.FundamentalDomainVolume.volume_biUnion_smul_fd_lt_top _

theorem volume_gammaFundamentalSet_pos (Γ : Subgroup SL(2, ℤ)) :
    0 < volume (gammaFundamentalSet Γ) := by
  refine lt_of_lt_of_le ?_
    (measure_mono (Set.subset_iUnion _ (QuotientGroup.mk 1 : SL(2, ℤ) ⧸ Γ)))
  rw [FLT.HyperbolicMeasure.volume_smul_sl2z]
  exact FLT.FundamentalDomainVolume.volume_fd_pos

theorem volume_gammaFundamentalSet_ne_zero_ne_top (Γ : Subgroup SL(2, ℤ))
    [Finite (SL(2, ℤ) ⧸ Γ)] :
    volume (gammaFundamentalSet Γ) ≠ 0 ∧ volume (gammaFundamentalSet Γ) ≠ ⊤ :=
  ⟨(volume_gammaFundamentalSet_pos Γ).ne', (volume_gammaFundamentalSet_lt_top Γ).ne⟩

theorem volume_gamma0_lt_top (N : ℕ) [NeZero N] :
    volume (gammaFundamentalSet (Gamma0 N)) < ⊤ :=
  haveI : Finite (SL(2, ℤ) ⧸ Gamma0 N) := FLT.SiegelSetCover.finite_quotient_gamma0 N
  volume_gammaFundamentalSet_lt_top (Gamma0 N)

theorem exists_gamma0_smul_mem (N : ℕ) (z : ℍ) :
    ∃ γ ∈ Gamma0 N, γ • z ∈ gammaFundamentalSet (Gamma0 N) :=
  exists_smul_mem_gammaFundamentalSet (Gamma0 N) z

def truncatedGammaFundamentalSet (Γ : Subgroup SL(2, ℤ)) (y : ℝ) : Set ℍ :=
  ⋃ q : SL(2, ℤ) ⧸ Γ, (Quotient.out q)⁻¹ • truncatedFundamentalDomain y

instance : ContinuousConstSMul SL(2, ℤ) ℍ where
  continuous_const_smul γ := by
    have h : (fun z : ℍ => γ • z) =
        fun z : ℍ => (Matrix.SpecialLinearGroup.mapGL ℝ γ) • z := by
      funext z
      exact MulAction.compHom_smul_def (Matrix.SpecialLinearGroup.mapGL ℝ) γ z
    rw [h]
    exact continuous_const_smul _

theorem isCompact_smul_truncated (γ : SL(2, ℤ)) (y : ℝ) :
    IsCompact (γ • truncatedFundamentalDomain y) :=
  IsCompact.smul γ (isCompact_truncatedFundamentalDomain y)

theorem isCompact_truncatedGammaFundamentalSet (Γ : Subgroup SL(2, ℤ))
    [Finite (SL(2, ℤ) ⧸ Γ)] (y : ℝ) :
    IsCompact (truncatedGammaFundamentalSet Γ y) :=
  isCompact_iUnion fun q => isCompact_smul_truncated (Quotient.out q)⁻¹ y

theorem isCompact_truncatedGamma0 (N : ℕ) [NeZero N] (y : ℝ) :
    IsCompact (truncatedGammaFundamentalSet (Gamma0 N) y) :=
  haveI : Finite (SL(2, ℤ) ⧸ Gamma0 N) := FLT.SiegelSetCover.finite_quotient_gamma0 N
  isCompact_truncatedGammaFundamentalSet (Gamma0 N) y

theorem truncatedGammaFundamentalSet_subset (Γ : Subgroup SL(2, ℤ)) (y : ℝ) :
    truncatedGammaFundamentalSet Γ y ⊆ gammaFundamentalSet Γ := by
  refine Set.iUnion_mono fun q => Set.smul_set_mono ?_
  exact fun z hz => hz.1

theorem gate_volume_lt_volume_univ (Γ : Subgroup SL(2, ℤ)) [Finite (SL(2, ℤ) ⧸ Γ)] :
    volume (gammaFundamentalSet Γ) < volume (Set.univ : Set ℍ) := by
  rw [FLT.HyperbolicMeasure.volume_univ_eq_top]
  exact volume_gammaFundamentalSet_lt_top Γ

theorem gate_volume_top_eq : volume (gammaFundamentalSet (⊤ : Subgroup SL(2, ℤ))) =
    volume 𝒟 := by
  haveI : Subsingleton (SL(2, ℤ) ⧸ (⊤ : Subgroup SL(2, ℤ))) :=
    QuotientGroup.subsingleton_quotient_top
  have huniq : ∀ q : SL(2, ℤ) ⧸ (⊤ : Subgroup SL(2, ℤ)),
      q = (QuotientGroup.mk 1 : SL(2, ℤ) ⧸ (⊤ : Subgroup SL(2, ℤ))) := fun q =>
    Subsingleton.elim _ _
  have : gammaFundamentalSet (⊤ : Subgroup SL(2, ℤ)) =
      (Quotient.out (QuotientGroup.mk 1 : SL(2, ℤ) ⧸ (⊤ : Subgroup SL(2, ℤ))))⁻¹ • 𝒟 := by
    refine Set.Subset.antisymm (Set.iUnion_subset fun q => ?_)
      (Set.subset_iUnion (fun q : SL(2, ℤ) ⧸ (⊤ : Subgroup SL(2, ℤ)) =>
        (Quotient.out q)⁻¹ • 𝒟) (QuotientGroup.mk 1))
    rw [huniq q]
  rw [this, FLT.HyperbolicMeasure.volume_smul_sl2z]

example : volume (gammaFundamentalSet (Gamma0 11)) < ⊤ := volume_gamma0_lt_top 11

theorem gate_truncated_nonempty (Γ : Subgroup SL(2, ℤ)) :
    (truncatedGammaFundamentalSet Γ 2).Nonempty := by
  refine ⟨(Quotient.out (QuotientGroup.mk 1 : SL(2, ℤ) ⧸ Γ))⁻¹ • UpperHalfPlane.ρ,
    Set.mem_iUnion.mpr ⟨QuotientGroup.mk 1, Set.smul_mem_smul_set ?_⟩⟩
  refine ⟨FLT.SiegelSetCover.gate_rho_mem_fd, ?_⟩
  rw [FLT.SiegelSetCover.gate_im_rho]
  nlinarith [Real.sq_sqrt (by norm_num : (3 : ℝ) ≥ 0),
    Real.sqrt_nonneg (3 : ℝ)]

end FLT.Gamma0FundamentalSet

Statements phrased using this module (30)