Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ExtEndgame_ProductionDatum.lean

definition module

Arithmetic datum at the places ∞ and p; dual Selmer group

For a prime q, ExtCitation.primeLocalGaloisGroup is the group of \mathbb{Q}_q-algebra automorphisms of an algebraic closure \overline{\mathbb{Q}}_q of \mathbb{Q}_q, i.e. the local absolute Galois group; primeLocalPlace is the valuation subring of \overline{\mathbb{Q}} obtained by pulling back the unit ball of \overline{\mathbb{Q}}_q along a fixed embedding \overline{\mathbb{Q}} \to \overline{\mathbb{Q}}_q, and primeLocalToGlobal is the resulting homomorphism from the local Galois group to \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) given by restricting a \mathbb{Q}_q-automorphism to \overline{\mathbb{Q}}.

For a finite set S of primes, extArithIndex S is the index set \{*\} \sqcup S, one archimedean index together with the primes of S. The associated local groups extArithLocalGroups are, at the archimedean index, the subgroup of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) generated by complex conjugation (the restriction to \overline{\mathbb{Q}} of complex conjugation along a chosen embedding into \mathbb{C}), and at q \in S the local Galois group at q; extArithLoc assembles the inclusion and the maps primeLocalToGlobal into a family of homomorphisms to the global Galois group, with two lemmas recording its two branches. For P_2 \subseteq S, extArithDistinguished S P₂ is the set of indices consisting of the image of P_2 together with the archimedean index.

For a prime p, pSet p is the singleton \{p\}, so that the datum is taken at \infty and p only. extDualModule p is the one-dimensional \mathbb{Z}/p-representation of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) on which \sigma acts by the square of the mod p cyclotomic character, that is \mathbb{Z}/p(2). Finally, extDualSelmerAdm, given local pairings between the H^1 of the restriction of \mathbb{Z}/p(-1) and of \mathbb{Z}/p(2) at each index and a subspace \mathrm{adm}' of H^1(\mathbb{Z}/p(2)), is the Selmer group of \mathbb{Z}/p(2) for the local conditions orthogonal to those on \mathbb{Z}/p(-1), intersected with \mathrm{adm}'. Here the conditions on \mathbb{Z}/p(-1) are extConditions for the distinguished set extArithDistinguished (pSet p) Set.univ, which is all of \{*\} \sqcup \{p\}, so the primal conditions are zero at every index; consequently their orthogonal complements are the full local cohomology groups and the dual Selmer group reduces to \mathrm{adm}'.

Relation to Mathlib

The Galois groups, valuation subrings, the p-adic algebraic closure and group cohomology H^1 of Rep objects are Mathlib's; the Selmer-group apparatus used here (ofChar, extConditions, dualConditions, selmerAdm) is the project's own, Mathlib having no notion of Selmer group for Galois cohomology.

Where it is used

These objects are the concrete instantiation, at the set of places \{\infty, p\} of \mathbb{Q}, of the abstract data (local groups, local conditions, dual module and admissible subspace) entering the project's Greenberg–Wiles inequality and its Stickelberger-theoretic input, used to show that certain extensions of \mathbb{Z}/p by \mathbb{Z}/p(1) over \mathbb{Q} which are unramified outside p and locally split at p split globally.

References

  1. L. C. Washington, Introduction to Cyclotomic Fields, Graduate Texts in Mathematics 83, Springer, 2nd edition, 1997
  2. J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Grundlehren der mathematischen Wissenschaften 323, Springer, 2nd edition, 2008

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ExtEndgame_ChainAdm
import Definitions.Def_GaloisRep_ComplexConjugation
import Definitions.Def_GaloisRep_CompletionBridge
import Definitions.Def_ClassGroup_GaloisAction

set_option autoImplicit false

open CategoryTheory Module groupCohomology

namespace ExtCitation

def primeLocalGaloisGroup (q : Nat.Primes) : Type :=
  letI : Fact (q : ℕ).Prime := ⟨q.2⟩
  PadicAlgCl (q : ℕ) ≃ₐ[ℚ_[(q : ℕ)]] PadicAlgCl (q : ℕ)

noncomputable instance (q : Nat.Primes) : Group (primeLocalGaloisGroup q) :=
  letI : Fact (q : ℕ).Prime := ⟨q.2⟩
  inferInstanceAs (Group (PadicAlgCl (q : ℕ) ≃ₐ[ℚ_[(q : ℕ)]] PadicAlgCl (q : ℕ)))

noncomputable def primeLocalPlace (q : Nat.Primes) : ValuationSubring (AlgebraicClosure ℚ) :=
  letI : Fact (q : ℕ).Prime := ⟨q.2⟩
  padicPlace (q : ℕ)

noncomputable def primeLocalToGlobal (q : Nat.Primes) :
    primeLocalGaloisGroup q →* (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) :=
  letI : Fact (q : ℕ).Prime := ⟨q.2⟩
  localGaloisToGlobal (q : ℕ)

section Datum

variable (S : Finset Nat.Primes)

def extArithIndex : Type := Unit ⊕ ↥S

noncomputable instance : Fintype (extArithIndex S) :=
  inferInstanceAs (Fintype (Unit ⊕ ↥S))

def extArithLocalGroups : extArithIndex S → Type
  | Sum.inl _ => ↥archimedeanDecomposition
  | Sum.inr q => primeLocalGaloisGroup q.1

noncomputable instance : ∀ v : extArithIndex S, Group (extArithLocalGroups S v)
  | Sum.inl _ => inferInstanceAs (Group ↥archimedeanDecomposition)
  | Sum.inr q => inferInstanceAs (Group (primeLocalGaloisGroup q.1))

noncomputable def extArithLoc :
    ∀ v : extArithIndex S,
      extArithLocalGroups S v →* (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
  | Sum.inl _ => archimedeanLoc
  | Sum.inr q => primeLocalToGlobal q.1

@[simp] lemma extArithLoc_inl (v : Unit) : extArithLoc S (Sum.inl v) = archimedeanLoc := rfl
@[simp] lemma extArithLoc_inr (q : ↥S) : extArithLoc S (Sum.inr q) = primeLocalToGlobal q.1 := rfl

def extArithDistinguished (P₂ : Set ↥S) : Set (extArithIndex S) :=
  Sum.inr '' P₂ ∪ Set.range Sum.inl

end Datum

variable (p : ℕ) [Fact p.Prime]

def pPrime : Nat.Primes := ⟨p, Fact.out⟩

@[simp] lemma pPrime_coe : ((pPrime p : Nat.Primes) : ℕ) = p := rfl

def pSet : Finset Nat.Primes := {pPrime p}

noncomputable abbrev extDualModule :
    Rep (ZMod p) (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) :=
  ofChar (k := ZMod p) ((cycloChar p) ^ 2)

noncomputable abbrev extDualSelmerAdm
    (pairing : ∀ v, H1 (Rep.res (extArithLoc (pSet p) v)
        (ofChar (k := ZMod p) (cycloChar p)⁻¹)) →ₗ[ZMod p]
      H1 (Rep.res (extArithLoc (pSet p) v) (extDualModule p)) →ₗ[ZMod p] (ZMod p))
    (adm' : Submodule (ZMod p) (H1 (extDualModule p))) :
    Submodule (ZMod p) (H1 (extDualModule p)) :=
  selmerAdm (extArithLoc (pSet p)) (extDualModule p)
    (dualConditions (extArithLoc (pSet p)) (ofChar (k := ZMod p) (cycloChar p)⁻¹)
      (extDualModule p) pairing
      (extConditions (extArithLoc (pSet p)) (ofChar (k := ZMod p) (cycloChar p)⁻¹)
        (extArithDistinguished (pSet p) Set.univ) (fun _ => ⊥))) adm'

end ExtCitation

Statements phrased using this module (140)