Deformation rings

Stream: FLT

[Junyan Xu]

FLT#481 now builds, and only the docBlame/simpNF linters report errors. I count 67 sorrys and 11 #exits in the PR: one #exit (in FLT/Deformation/Algebra/InverseLimit/Topology.lean) is marked "this is the old version", and most #exits are at the beginning of the file. Are all these files to be abandoned? Should we fill sorrys in all remaining files? Are there blueprint chapter/section(s) corresponding to this PR?

[Notification Bot]

A message was moved here from #Is there code for X? > CompleteGroupAlgebra by Kevin Buzzard.

[Kevin Buzzard]

@Junyan Xu I've moved the discussion to here. Right now @Andrew Yang is going to take a look at the branch (he was involved in writing some of it but mostly it was not his work). The "big goal" is to state and then prove the kind of representability results which Wiles and others use, i.e. if $F$ is a fixed totally real field and $k$ is a finite field of characteristic $p$ and $\rho:Gal(\overline{F}/F)\to GL_2(k)$ is a continuous irreducible representation and we consider "nice" deformations to Artin local $k$-algebras with residue field $k$ (here "nice" will one day mean things like "unramified outside a finite set of places, flat at $p$ and with cyclotomic determinant" but initially it will mean "deformations satisfying a predicate which obeys a list of axioms") then this functor is prorepresentable.

[Kevin Buzzard]

My understanding is that the proposal is to follow Lenstra's proof in Cornell-Silverman-Stevens which first proves a result for $G$ finite; I think that this was as far as the PR got.

[Kevin Buzzard]

@Junyan Xu @Jz Pan Andrew now got Javier's work on deformation rings compiling again. Is there anything here you have any comments on? There is IsProartinian, Deformation.repnFunctor, subfunctors and more! The review process is nothing like mathlib's -- basically I will read through this stuff and merge it rather than debating for a long time whether definitions are "the best for mathlib", I'm happy to be more experimental.

[Jz Pan]

Kevin Buzzard said:

Junyan Xu Jz Pan Andrew now got Javier's work on deformation rings compiling again. Is there anything here you have any comments on? There is IsProartinian, Deformation.repnFunctor, subfunctors and more! The review process is nothing like mathlib's -- basically I will read through this stuff and merge it rather than debating for a long time whether definitions are "the best for mathlib", I'm happy to be more experimental.

Not yet; I'm busying with other things. Maybe I'll take a look later.

By the way, does the deformation rings theory use completed group algebra like $\Z_p[[\Gamma]]$?

[Jz Pan]

I remembered that there are at least formal power series.

[Kevin Buzzard]

These completed group algebras are the answers to questions. For example the universal deformation ring of the trivial mod p 1-dimensional representation of $\Z_p^\times$ is isomorphic to $\Z_p[[(1+p\Z_p)]].$

[Jz Pan]

But you don't need to use the fact that it is isomorphic to $\Z_p[[T]]$?

[Andrew Yang]

The new PR is FLT#504 by the way.