Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Deformations_TraceAlgebra.lean

definition module

Trace subalgebra of a lift and its descent condition

The standing context is a local ring \mathcal O, a topological group G, a finite index type n, and the category \mathrm{ProartinianCat}\ \mathcal O of local pro-Artinian \mathcal O-algebras with residue field that of \mathcal O; objects are written A with underlying ring A.\mathrm{carrier}, and a lift is a continuous monoid homomorphism \rho\colon G \to \mathrm{GL}_n(A). Three groups of declarations are made. First, for R in the category, conjKer R is the subgroup of \mathrm{ConjAct}(\mathrm{GL}_n R) consisting of those \gamma whose underlying matrix maps to 1 under reduction \mathrm{GL}_n(R) \to \mathrm{GL}_n(k) along the canonical map ProartinianCat.toResidueField R; mem_conjKer_iff records this membership criterion, and conjAct_smul_apply states that the conjugation action on lifts is (\gamma\cdot\rho)(g) = \gamma\,\rho(g)\,\gamma^{-1}. Alongside, mapRepn names the pushforward of a lift along a morphism f\colon A \to B, i.e. the action of repnFunctor on f, with mapRepn_apply identifying it as entrywise application of f to \rho(g).

Second, traceSet π“ž ρ is the set of values \operatorname{tr}\rho(g), g \in G, in A, and traceSubalgebra π“ž ρ is the topological closure of the \mathcal O-subalgebra generated by this set. Three lemmas give its basic properties: it is a closed subset of A; it contains every \operatorname{tr}\rho(g); and it is contained in any closed \mathcal O-subalgebra T of A with \operatorname{tr}\rho(g) \in T for all g, so it is the smallest such. Traces are unchanged by the conjugation action (trace_smul_eq) and commute with pushforward, \operatorname{tr}(f_*\rho)(g) = f(\operatorname{tr}\rho(g)) (trace_mapRepn).

Third, TraceAlgebra.Descends ρ is the predicate asserting the existence of \gamma \in conjKer A such that every matrix entry ((\gamma\cdot\rho)(g))_{ij}, for all g \in G and all i,j, lies in traceSubalgebra π“ž ρ. This is a condition on \rho itself, formulated via an explicit conjugating element rather than an abstract equivalence of lifts.

Relation to Mathlib

Mathlib supplies the ambient notions used here (\mathrm{ConjAct}, \mathrm{GL}_n, Algebra.adjoin, Subalgebra.topologicalClosure and its minimality, Matrix.trace); the trace subalgebra of a lift and the descent predicate are the project's own definitions, built over the project's ProartinianCat and repnFunctor.

Where it is used

The trace subalgebra is the candidate ring for a lift of a residual representation, and the descent predicate expresses that the lift can be conjugated, by an element congruent to the identity modulo the maximal ideal, into matrices with entries in that subalgebra. Descent for lifts of an absolutely irreducible residual representation is what makes the trace subalgebra the relevant deformation ring, hence feeds the representability of the deformation functor used in the modularity-lifting argument.

References

  1. B. Mazur, Deforming Galois representations, in: Galois Groups over \mathbb{Q}, MSRI Publications 16, Springer, 1989, 385–437
  2. H. Carayol, Formes modulaires et reprΓ©sentations galoisiennes Γ  valeurs dans un anneau local complet, in: p-adic Monodromy and the Birch and Swinnerton-Dyer Conjecture, Contemporary Mathematics 165, American Mathematical Society, 1994, 213–237
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, Β§2

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_Deformations_LiftFunctor

set_option autoImplicit false

universe u

open CategoryTheory IsLocalRing

namespace Deformation

variable {n : Type} [Fintype n] [DecidableEq n]
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {π“ž : Type u} [CommRing π“ž] [IsLocalRing π“ž]

noncomputable abbrev conjKer (R : ProartinianCat π“ž) : Subgroup (ConjAct (GL n R)) :=
  ((Matrix.GeneralLinearGroup.map (n := n)
    (ProartinianCat.toResidueField R).hom.toRingHom).ker.comap (ConjAct.ofConjAct.toMonoidHom))

variable (n) in
lemma mem_conjKer_iff {R : ProartinianCat π“ž} (Ξ³ : ConjAct (GL n R)) :
    Ξ³ ∈ conjKer (n := n) R ↔
      Matrix.GeneralLinearGroup.map (ProartinianCat.toResidueField R).hom.toRingHom
        (ConjAct.ofConjAct Ξ³) = 1 :=
  Iff.rfl

variable (n G π“ž) in

abbrev mapRepn {A B : ProartinianCat π“ž} (f : A ⟢ B) (ρ : G β†’β‚œ* GL n A) : G β†’β‚œ* GL n B :=
  (repnFunctor n G π“ž).map f ρ

omit [IsLocalRing π“ž] in
@[simp]
lemma mapRepn_apply {A B : ProartinianCat π“ž} (f : A ⟢ B) (ρ : G β†’β‚œ* GL n A) (g : G) :
    mapRepn n G π“ž f ρ g = Matrix.GeneralLinearGroup.map f.hom.toRingHom (ρ g) :=
  rfl

omit [IsLocalRing π“ž] in

lemma conjAct_smul_apply {R : ProartinianCat π“ž} (Ξ³ : ConjAct (GL n R))
    (ρ : G β†’β‚œ* GL n R) (g : G) :
    (Ξ³ β€’ ρ) g = ConjAct.ofConjAct Ξ³ * ρ g * (ConjAct.ofConjAct Ξ³)⁻¹ :=
  rfl

section TraceAlgebra

open ProartinianCat

variable (π“ž) in

def traceSet {A : ProartinianCat π“ž} (ρ : G β†’β‚œ* GL n A) : Set A.carrier :=
  Set.range fun g => Matrix.trace ((ρ g : GL n A.carrier) : Matrix n n A.carrier)

variable (π“ž) in

def traceSubalgebra {A : ProartinianCat π“ž} (ρ : G β†’β‚œ* GL n A) : Subalgebra π“ž A.carrier :=
  (Algebra.adjoin π“ž (traceSet π“ž ρ)).topologicalClosure

omit [IsLocalRing π“ž] in
lemma isClosed_traceSubalgebra {A : ProartinianCat π“ž} (ρ : G β†’β‚œ* GL n A) :
    IsClosed ((traceSubalgebra π“ž ρ : Subalgebra π“ž A.carrier) : Set A.carrier) :=
  Subalgebra.isClosed_topologicalClosure _

omit [IsLocalRing π“ž] in
lemma trace_mem_traceSubalgebra {A : ProartinianCat π“ž} (ρ : G β†’β‚œ* GL n A) (g : G) :
    Matrix.trace ((ρ g : GL n A.carrier) : Matrix n n A.carrier) ∈ traceSubalgebra π“ž ρ :=
  (Algebra.adjoin π“ž (traceSet π“ž ρ)).le_topologicalClosure
    (Algebra.subset_adjoin ⟨g, rfl⟩)

omit [IsLocalRing π“ž] in

lemma traceSubalgebra_le {A : ProartinianCat π“ž} (ρ : G β†’β‚œ* GL n A) {T : Subalgebra π“ž A.carrier}
    (hT : IsClosed (T : Set A.carrier))
    (h : βˆ€ g, Matrix.trace ((ρ g : GL n A.carrier) : Matrix n n A.carrier) ∈ T) :
    traceSubalgebra π“ž ρ ≀ T :=
  Subalgebra.topologicalClosure_minimal
    (Algebra.adjoin_le (by rintro _ ⟨g, rfl⟩; exact h g)) hT

end TraceAlgebra

section TraceConj

omit [IsLocalRing π“ž] in

lemma trace_smul_eq {A : ProartinianCat π“ž} (Ξ³ : ConjAct (GL n A.carrier))
    (ρ : G β†’β‚œ* GL n A) (g : G) :
    Matrix.trace (((Ξ³ β€’ ρ) g : GL n A.carrier) : Matrix n n A.carrier) =
      Matrix.trace ((ρ g : GL n A.carrier) : Matrix n n A.carrier) := by
  have h1 : ((Ξ³ β€’ ρ) g : GL n A.carrier) =
      ConjAct.ofConjAct γ * ρ g * (ConjAct.ofConjAct γ)⁻¹ := conjAct_smul_apply γ ρ g
  rw [h1]
  have h2 : ((ConjAct.ofConjAct γ * ρ g * (ConjAct.ofConjAct γ)⁻¹ : GL n A.carrier) :
      Matrix n n A.carrier) =
      ((ConjAct.ofConjAct Ξ³ : GL n A.carrier) : Matrix n n A.carrier) *
        ((ρ g : GL n A.carrier) : Matrix n n A.carrier) *
        ((↑(ConjAct.ofConjAct Ξ³)⁻¹ : GL n A.carrier) : Matrix n n A.carrier) := by
    rw [Units.val_mul, Units.val_mul]
  rw [h2]
  exact Matrix.trace_units_conj (ConjAct.ofConjAct Ξ³) _

omit [IsLocalRing π“ž] in

lemma trace_mapRepn {A B : ProartinianCat π“ž} (f : A ⟢ B) (ρ : G β†’β‚œ* GL n A) (g : G) :
    Matrix.trace ((mapRepn n G π“ž f ρ g : GL n B.carrier) : Matrix n n B.carrier) =
      f.hom (Matrix.trace ((ρ g : GL n A.carrier) : Matrix n n A.carrier)) := by
  have h1 : ((mapRepn n G π“ž f ρ g : GL n B.carrier) : Matrix n n B.carrier) =
      ((ρ g : GL n A.carrier) : Matrix n n A.carrier).map f.hom.toRingHom := by
    rw [mapRepn_apply]
    rfl
  rw [h1]
  exact (AddMonoidHom.map_trace f.hom.toRingHom _).symm

end TraceConj

section Universal

open ProartinianCat

def TraceAlgebra.Descends {A : ProartinianCat π“ž} (ρ : G β†’β‚œ* GL n A) : Prop :=
  βˆƒ Ξ³ ∈ conjKer (n := n) A, βˆ€ (g : G) (i j : n),
    (((Ξ³ β€’ ρ) g : GL n A.carrier) : Matrix n n A.carrier) i j ∈ traceSubalgebra π“ž ρ

end Universal

end Deformation

Statements phrased using this module (3)