`Definitions/Def_Deformations_LiftFunctor.lean`

definition moduleadapted from the Imperial College London FLT project: FLT/Deformations/LiftFunctor.lean

Representation, lift and deformation functors on pro-Artinian algebras

Fix a finite index type n, a topological group G and a local ring \mathcal O, and work over the category ProartinianCat 𝓞 whose objects are topological \mathcal O-algebras R that are local, pro-Artinian, with \mathcal O \to R local and inducing a surjection onto the residue field of R, and whose morphisms are continuous \mathcal O-algebra maps; this category has terminal object ProartinianCat.residueField, the residue field k of \mathcal O with the discrete topology.

repnFunctor n G 𝓞 sends R to the set of continuous monoid homomorphisms G \to \mathrm{GL}_n(R) and a morphism f\colon R \to S to push-forward along the entrywise map \mathrm{GL}_n(R)\to\mathrm{GL}_n(S); repnFunctor_map records the pointwise formula ((\mathrm{repnFunctor}).map\,f\,\rho)(x) = \mathrm{GL}_n(f)(\rho x). toRepresentation turns such a point into a Representation R G (n → R), i.e. a homomorphism of G into the R-endomorphisms of R^n, by composing \rho with \mathrm{GL}_n(R)\to\mathrm{GL}(R^n) and the inclusion of units.

repnQuotFunctor n G 𝓞 sends R to the orbit quotient of G \to_{\mathrm{cont}} \mathrm{GL}_n(R) under the conjugation action of the subgroup of \mathrm{ConjAct}(\mathrm{GL}_n(R)) corresponding to the kernel of \mathrm{GL}_n(R)\to\mathrm{GL}_n(k) induced by ProartinianCat.toResidueField R; that is, quotient by strict equivalence. Functoriality of this quotient is part of the definition, and toRepnQuot is the natural transformation given objectwise by the quotient map.

For a point \bar\rho of repnFunctor at the terminal object, liftFunctor and deformationFunctor are the subfunctors obtained from Subfunctor.ofIsTerminal applied to the singleton \{\bar\rho\}, respectively its class: objectwise, the continuous \rho\colon G\to\mathrm{GL}_n(R) whose reduction along the unique map R \to k equals \bar\rho, and the strict equivalence classes reducing to the class of \bar\rho.

Relation to Mathlib

Mathlib has no deformation functors; these are the project's own, built on Mathlib's CategoryTheory.Subfunctor, Matrix.GeneralLinearGroup, Representation and MulAction.orbitRel.Quotient, together with the project's category of local pro-Artinian \mathcal O-algebras and the construction of a subfunctor from a subset of the value at a terminal object.

Where it is used

These are the functors whose pro-representing objects are the universal lifting and universal deformation rings of a residual representation \bar\rho, the deformation-theoretic input to the modularity lifting argument; deformation conditions are imposed as further subfunctors of the lift functor.

References

B. Mazur, Deforming Galois representations, in: Galois Groups over \mathbb{Q} (Berkeley, 1987), Mathematical Sciences Research Institute Publications 16, Springer, 1989, 385–437
B. de Smit and H. W. Lenstra, Jr., Explicit construction of universal deformation rings, in: Modular Forms and Fermat's Last Theorem, Springer, 1997, 313–326
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.

71 lines
7 declarations
used in the statements of 2 theorems and imported by 3 proofs
imports 2 definition modules

Source file: Definitions/Def_Deformations_LiftFunctor.lean

Imports

Imported by

Def_Deformations_TraceAlgebra

Source

import Mathlib
import Definitions.Def_Deformations_ProartinianCat
import Definitions.Def_CategoryTheory_Subfunctor_OfIsTerminal

set_option autoImplicit false

open CategoryTheory IsLocalRing

namespace Deformation

universe u

variable {n : Type} [Fintype n] [DecidableEq n] (G : Type u) [Group G] [TopologicalSpace G]
variable (𝓞 : Type u) [CommRing 𝓞] [IsLocalRing 𝓞]

variable (n) in

def repnFunctor : ProartinianCat 𝓞 ⥤ Type u where
  obj R := G →ₜ* GL n R
  map {R S} f := ↾ (fun ρ ↦ .comp (Units.mapₜ f.hom.mapMatrix.toContinuousMonoidHom) ρ)

omit [IsLocalRing 𝓞] in
@[simp]
lemma repnFunctor_map {R S : ProartinianCat 𝓞} (f : R ⟶ S) (ρ : G →ₜ* GL n R) (x : G) :
    DFunLike.coe (F := G →ₜ* GL n S) ((repnFunctor n G 𝓞).map f ρ) x =
      Matrix.GeneralLinearGroup.map (n := n) f.hom.toRingHom (ρ x) := rfl

variable {G 𝓞} in

def toRepresentation {R} (ρ : (repnFunctor n G 𝓞).obj R) :
    Representation R G (n → R) :=
  (Units.coeHom _).comp (Matrix.GeneralLinearGroup.toLin.toMonoidHom.comp ρ.toMonoidHom)

variable (n)

set_option backward.isDefEq.respectTransparency false in

noncomputable
def repnQuotFunctor : ProartinianCat 𝓞 ⥤ Type u where
  obj R := MulAction.orbitRel.Quotient ((Matrix.GeneralLinearGroup.map (n := n)
    (ProartinianCat.toResidueField R).hom.toRingHom).ker.comap (ConjAct.ofConjAct.toMonoidHom))
    (G →ₜ* GL n R)
  map {R S} f := ↾Quotient.map ((repnFunctor n G 𝓞).map f) (by
    rintro _ ρ ⟨⟨g, hg⟩, rfl⟩
    refine ⟨⟨.toConjAct (Matrix.GeneralLinearGroup.map f.hom.toRingHom g.ofConjAct), ?_⟩, ?_⟩
    · simpa [← Matrix.GeneralLinearGroup.map_comp_apply, ← Matrix.GeneralLinearGroup.map_comp,
        ← RingHom.coe_comp, ← ContinuousAlgHom.coe_comp,
        -AlgHomClass.toRingHom_toAlgHom, ← AlgHom.comp_toRingHom, ← ProartinianCat.hom_comp,
        Subsingleton.elim _ R.toResidueField]
    · obtain ⟨g, rfl⟩ := ConjAct.toConjAct.surjective g
      ext1 γ
      simp [ConjAct.toConjAct_smul, ← map_inv, -ConjAct.ofConjAct_inv, ← map_mul])
  map_id _ := by ext ⟨_⟩; rfl
  map_comp _ _ := by ext ⟨_⟩; rfl

noncomputable
def toRepnQuot : repnFunctor n G 𝓞 ⟶ repnQuotFunctor n G 𝓞 where
  app _ := ↾Quotient.mk''
  naturality _ _ _ := rfl

noncomputable
def liftFunctor (ρ : (repnFunctor n G 𝓞).obj .residueField) : Subfunctor (repnFunctor n G 𝓞) :=
  .ofIsTerminal _ ProartinianCat.isTerminalResidueField {ρ}

noncomputable
def deformationFunctor (ρ : (repnFunctor n G 𝓞).obj .residueField) :
    Subfunctor (repnQuotFunctor n G 𝓞) :=
  .ofIsTerminal _ ProartinianCat.isTerminalResidueField {(toRepnQuot n G 𝓞).app _ ρ}

end Deformation

Definitions/Def_Deformations_LiftFunctor.lean