Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_Adic.lean

definition module

Rank-two Galois representations over a local coefficient ring

Fix a commutative local ring A with maximal ideal \mathfrak m. GaloisActionIsAdicContinuous A ρ, for a monoid homomorphism \rho from \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q) (realised as \overline{\mathbb Q}\simeq_{\mathbb Q}\overline{\mathbb Q}, with \overline{\mathbb Q}= AlgebraicClosure ℚ) to \mathrm{End}_A(V), asserts: for every n there is an intermediate field L of \overline{\mathbb Q}/\mathbb Q, finite-dimensional over \mathbb Q, such that every \sigma fixing L pointwise satisfies \rho(\sigma)v-v\in\mathfrak m^n\cdot V for all v. No topology on A, on V or on the Galois group is used; this is the project's own substitute for continuity. A GaloisRepAdic A then bundles a type V with an A-module structure that is free and finite, the equation \operatorname{finrank}_A V=2, a monoid homomorphism \rho into \mathrm{End}_A(V), and the above condition as a field.

For \rho : GaloisRepAdic A: IsUnramifiedAt ρ q says that for every valuation subring P of \overline{\mathbb Q} lying over the prime q (predicate LiesOverPrime, from an imported module), every element of P.inertiaSubgroupIn ℚ acts as the identity; det ρ is the character \mathrm{Gal}\to A^\times obtained from \sigma\mapsto\det(\rho(\sigma)) via toHomUnits, and trace ρ σ is \operatorname{tr}_A(\rho(\sigma)). baseChangeAlong φ hφ transports \rho along an explicit ring homomorphism \varphi:A\to B of local rings that is assumed local, with carrier B\otimes_A V and \rho(\sigma) replaced by its base change; residual ρ is the representation on \kappa\otimes_A V, \kappa the residue field of A, as a ResidualGaloisRep, its finite-level field being deduced from adic continuity for n=1.

Equivalence is data: Equiv ρ₁ ρ₂ consists of an A-linear isomorphism e:V_1\to V_2 together with the intertwining identity e(\rho_1(\sigma)x)=\rho_2(\sigma)(e(x)) for all \sigma,x; IsEquiv is its Nonempty. Helper declarations give reflexivity, symmetry, transitivity, compatibility of Equiv with base change and with passage to the residual representation, and, when the coefficients form a field k, mutually inverse passages between GaloisRepAdic k and ResidualGaloisRep k on the same carrier.

Relation to Mathlib

Mathlib has no notion of a Galois representation; the structures and the adic-continuity predicate are the project's own, built on Mathlib's Module.Free/Module.Finite, Module.finrank, LinearMap.det/LinearMap.trace, tensor-product base change, IsLocalRing.ResidueField and ValuationSubring.inertiaSubgroupIn. Change of coefficients is always along an explicit φ : A →+* B with an explicit IsLocalHom φ argument, never an ambient Algebra A B instance.

Where it is used

These are the coefficient-ring-valued two-dimensional representations used throughout the lifting argument: representations with values in a localised Hecke algebra, universal deformations of a residual representation, and Tate modules of elliptic curves over p-adic rings. The module supplies the currency (unramifiedness, trace and determinant, base change, reduction to the residue field, and equivalence) on which the deformation-theoretic and Hecke-algebra modules that import it are phrased.

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. B. Mazur, Deforming Galois representations, in Galois Groups over Q (Berkeley, 1987), MSRI Publications 16, Springer, 1989, pp. 385–437
  3. A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551

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

Imports

Imported by

Declarations

Source

import Mathlib.LinearAlgebra.Charpoly.BaseChange ↗
import Mathlib.LinearAlgebra.Trace ↗
import Mathlib.RingTheory.LocalRing.ResidueField.Basic ↗
import Definitions.Def_GaloisRep_Residual
import Definitions.Def_GaloisRep_ResidualEquiv

open scoped TensorProduct

def GaloisActionIsAdicContinuous (A : Type) [CommRing A] [IsLocalRing A]
    {V : Type} [AddCommGroup V] [Module A V]
    (ρ : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* Module.End A V) : Prop :=
  ∀ n : ℕ, ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ L ∧
    ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, (∀ x ∈ L, σ x = x) →
      ∀ v : V, ρ σ v - v ∈ (IsLocalRing.maximalIdeal A ^ n) • (⊤ : Submodule A V)

structure GaloisRepAdic (A : Type) [CommRing A] [IsLocalRing A] : Type 1 where

  V : Type
  [instAddCommGroup : AddCommGroup V]
  [instModule : Module A V]
  [instFree : Module.Free A V]
  [instFinite : Module.Finite A V]

  finrank_eq : Module.finrank A V = 2

  ρ : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* Module.End A V

  isAdicContinuous : GaloisActionIsAdicContinuous A ρ

attribute [instance] GaloisRepAdic.instAddCommGroup GaloisRepAdic.instModule
  GaloisRepAdic.instFree GaloisRepAdic.instFinite

namespace GaloisRepAdic

variable {A : Type} [CommRing A] [IsLocalRing A]

def IsUnramifiedAt (ρ : GaloisRepAdic A) (q : ℕ) : Prop :=
  ∀ P : ValuationSubring (AlgebraicClosure ℚ), P.LiesOverPrime q →
    ∀ σ ∈ P.inertiaSubgroupIn ℚ, ρ.ρ σ = 1

noncomputable def det (ρ : GaloisRepAdic A) : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* Aˣ :=
  (LinearMap.det.comp ρ.ρ).toHomUnits

noncomputable def trace (ρ : GaloisRepAdic A) (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) :
    A :=
  LinearMap.trace A ρ.V (ρ.ρ σ)

noncomputable def baseChangeAlong {B : Type} [CommRing B] [IsLocalRing B] (φ : A →+* B)
    (hφ : IsLocalHom φ) (ρ : GaloisRepAdic A) : GaloisRepAdic B :=
  letI : Algebra A B := φ.toAlgebra
  { V := B ⊗[A] ρ.V
    finrank_eq := by rw [Module.finrank_baseChange, ρ.finrank_eq]
    ρ := { toFun := fun σ => (ρ.ρ σ).baseChange B
           map_one' := by rw [map_one, LinearMap.baseChange_one]
           map_mul' := fun σ τ => by rw [map_mul, LinearMap.baseChange_mul] }
    isAdicContinuous := by
      intro n
      obtain ⟨L, hL, h1⟩ := ρ.isAdicContinuous n
      refine ⟨L, hL, fun σ hσ => ?_⟩
      have hmap : (IsLocalRing.maximalIdeal A ^ n).map φ ≤ IsLocalRing.maximalIdeal B ^ n := by
        rw [Ideal.map_pow]
        exact Ideal.pow_right_mono (Ideal.map_le_iff_le_comap.mpr fun a ha =>
          Ideal.mem_comap.mpr (haveI := hφ; map_nonunit φ a ha)) n
      have hpure : ∀ (b : B) (v : ρ.V),
          (ρ.ρ σ).baseChange B (b ⊗ₜ[A] v) - b ⊗ₜ[A] v ∈
            (IsLocalRing.maximalIdeal B ^ n) • (⊤ : Submodule B (B ⊗[A] ρ.V)) := by
        intro b v
        rw [LinearMap.baseChange_tmul, ← TensorProduct.tmul_sub]
        refine Submodule.smul_induction_on (p := fun x => b ⊗ₜ[A] x ∈
          (IsLocalRing.maximalIdeal B ^ n) • (⊤ : Submodule B (B ⊗[A] ρ.V))) (h1 σ hσ v) ?_ ?_
        · intro a ha w _
          rw [TensorProduct.tmul_smul, TensorProduct.smul_tmul', Algebra.smul_def, ← smul_eq_mul,
            ← TensorProduct.smul_tmul']
          exact Submodule.smul_mem_smul (hmap (Ideal.mem_map_of_mem φ ha)) Submodule.mem_top
        · intro x y hx hy
          rw [TensorProduct.tmul_add]
          exact Submodule.add_mem _ hx hy
      intro w
      induction w using TensorProduct.induction_on with
      | zero => rw [map_zero, sub_zero]; exact Submodule.zero_mem _
      | tmul b v => exact hpure b v
      | add x y hx hy =>
        rw [map_add, add_sub_add_comm]
        exact Submodule.add_mem _ hx hy }

noncomputable def residual (ρ : GaloisRepAdic A) :
    ResidualGaloisRep (IsLocalRing.ResidueField A) :=
  { V := IsLocalRing.ResidueField A ⊗[A] ρ.V
    finrank_eq := by rw [Module.finrank_baseChange, ρ.finrank_eq]
    ρ := { toFun := fun σ => (ρ.ρ σ).baseChange (IsLocalRing.ResidueField A)
           map_one' := by rw [map_one, LinearMap.baseChange_one]
           map_mul' := fun σ τ => by rw [map_mul, LinearMap.baseChange_mul] }
    factorsThroughFiniteLevel := by
      obtain ⟨L, hL, h1⟩ := ρ.isAdicContinuous 1
      refine ⟨L, hL, fun σ hσ => ?_⟩
      have hkill : ∀ x ∈ (IsLocalRing.maximalIdeal A ^ 1) • (⊤ : Submodule A ρ.V),
          ∀ c : IsLocalRing.ResidueField A, c ⊗ₜ[A] x = 0 := by
        intro x hx c
        refine Submodule.smul_induction_on
          (p := fun x => c ⊗ₜ[A] x = (0 : IsLocalRing.ResidueField A ⊗[A] ρ.V)) hx ?_ ?_
        · intro a ha w _
          rw [pow_one] at ha
          rw [TensorProduct.tmul_smul, TensorProduct.smul_tmul', Algebra.smul_def,
            IsLocalRing.ResidueField.algebraMap_eq, (IsLocalRing.residue_eq_zero_iff a).mpr ha,
            zero_mul, TensorProduct.zero_tmul]
        · intro x y hx hy
          rw [TensorProduct.tmul_add, hx, hy, add_zero]
      refine LinearMap.ext fun w => ?_
      rw [MonoidHom.coe_mk, OneHom.coe_mk]
      induction w using TensorProduct.induction_on with
      | zero => rw [map_zero, map_zero]
      | tmul c v =>
        rw [LinearMap.baseChange_tmul, Module.End.one_apply, ← sub_eq_zero,
          ← TensorProduct.tmul_sub]
        exact hkill _ (h1 σ hσ v) c
      | add x y hx hy => rw [map_add, map_add, hx, hy] }

structure Equiv (ρ₁ ρ₂ : GaloisRepAdic A) where

  toLinearEquiv : ρ₁.V ≃ₗ[A] ρ₂.V

  map_apply : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : ρ₁.V),
    toLinearEquiv (ρ₁.ρ σ x) = ρ₂.ρ σ (toLinearEquiv x)

def IsEquiv (ρ₁ ρ₂ : GaloisRepAdic A) : Prop :=
  Nonempty (Equiv ρ₁ ρ₂)

namespace Equiv

def refl (ρ : GaloisRepAdic A) : Equiv ρ ρ :=
  { toLinearEquiv := LinearEquiv.refl A ρ.V
    map_apply := fun _ _ => rfl }

def symm {ρ₁ ρ₂ : GaloisRepAdic A} (e : Equiv ρ₁ ρ₂) : Equiv ρ₂ ρ₁ :=
  { toLinearEquiv := e.toLinearEquiv.symm
    map_apply := fun σ y => e.toLinearEquiv.injective (by
      rw [LinearEquiv.apply_symm_apply, e.map_apply, LinearEquiv.apply_symm_apply]) }

def trans {ρ₁ ρ₂ ρ₃ : GaloisRepAdic A} (e : Equiv ρ₁ ρ₂) (e' : Equiv ρ₂ ρ₃) : Equiv ρ₁ ρ₃ :=
  { toLinearEquiv := e.toLinearEquiv.trans e'.toLinearEquiv
    map_apply := fun σ x => by
      rw [LinearEquiv.trans_apply, LinearEquiv.trans_apply, e.map_apply, e'.map_apply] }

noncomputable def baseChangeAlong {B : Type} [CommRing B] [IsLocalRing B] (φ : A →+* B)
    (hφ : IsLocalHom φ) {ρ₁ ρ₂ : GaloisRepAdic A} (e : Equiv ρ₁ ρ₂) :
    Equiv (ρ₁.baseChangeAlong φ hφ) (ρ₂.baseChangeAlong φ hφ) :=
  letI : Algebra A B := φ.toAlgebra
  { toLinearEquiv := e.toLinearEquiv.baseChange A B ρ₁.V ρ₂.V
    map_apply := fun σ x => by
      show e.toLinearEquiv.baseChange A B ρ₁.V ρ₂.V ((ρ₁.ρ σ).baseChange B x) =
        (ρ₂.ρ σ).baseChange B (e.toLinearEquiv.baseChange A B ρ₁.V ρ₂.V x)
      induction x using TensorProduct.induction_on with
      | zero => simp only [map_zero]
      | tmul b v =>
        rw [LinearMap.baseChange_tmul, LinearEquiv.baseChange_tmul, LinearEquiv.baseChange_tmul,
          LinearMap.baseChange_tmul, e.map_apply]
      | add x y hx hy => simp only [map_add, hx, hy] }

end Equiv

end GaloisRepAdic

namespace GaloisRepAdic

variable {A : Type} [CommRing A] [IsLocalRing A]

noncomputable def Equiv.residual {ρ₁ ρ₂ : GaloisRepAdic A} (e : Equiv ρ₁ ρ₂) :
    ResidualGaloisRep.Equiv ρ₁.residual ρ₂.residual :=
  { toLinearEquiv :=
      e.toLinearEquiv.baseChange A (IsLocalRing.ResidueField A) ρ₁.V ρ₂.V
    map_apply := fun σ x => by
      show e.toLinearEquiv.baseChange A (IsLocalRing.ResidueField A) ρ₁.V ρ₂.V
          ((ρ₁.ρ σ).baseChange (IsLocalRing.ResidueField A) x) =
        (ρ₂.ρ σ).baseChange (IsLocalRing.ResidueField A)
          (e.toLinearEquiv.baseChange A (IsLocalRing.ResidueField A) ρ₁.V ρ₂.V x)
      induction x using TensorProduct.induction_on with
      | zero => simp only [map_zero]
      | tmul b v =>
        rw [LinearMap.baseChange_tmul, LinearEquiv.baseChange_tmul, LinearEquiv.baseChange_tmul,
          LinearMap.baseChange_tmul, e.map_apply]
      | add x y hx hy => simp only [map_add, hx, hy] }

def toResidualGaloisRep {k : Type} [Field k] (ρ : GaloisRepAdic k) : ResidualGaloisRep k :=
  { V := ρ.V
    finrank_eq := ρ.finrank_eq
    ρ := ρ.ρ
    factorsThroughFiniteLevel := by
      obtain ⟨L, hL, h1⟩ := ρ.isAdicContinuous 1
      refine ⟨L, hL, fun σ hσ => LinearMap.ext fun v => ?_⟩
      have hbot : IsLocalRing.maximalIdeal k = ⊥ :=
        (Ideal.eq_bot_or_top _).resolve_right (Ideal.IsMaximal.ne_top inferInstance)
      have h := h1 σ hσ v
      rw [hbot, pow_one, Submodule.bot_smul, Submodule.mem_bot, sub_eq_zero] at h
      exact h }

def ofResidualGaloisRep {k : Type} [Field k] (ρ : ResidualGaloisRep k) : GaloisRepAdic k :=
  { V := ρ.V
    finrank_eq := ρ.finrank_eq
    ρ := ρ.ρ
    isAdicContinuous := by
      intro n
      obtain ⟨L, hL, h1⟩ := ρ.factorsThroughFiniteLevel
      refine ⟨L, hL, fun σ hσ v => ?_⟩
      rw [h1 σ hσ, Module.End.one_apply, sub_self]
      exact Submodule.zero_mem _ }

end GaloisRepAdic

Statements phrased using this module (97)