Statement of the "lifts" theorem

Stream: FLT

[Stepan Nesterov]

Currently, the main theorem of Lift.lean is stated like this:

theorem lifts (ρ : GaloisRep ℚ k V) (hρirred : ρ.IsIrreducible)
    (hρ : IsHardlyRamified hpodd hV ρ) :
    ∃ (R : Type u) (_ : CommRing R) (_ : IsLocalRing R)
      (_ : TopologicalSpace R) (_ : IsTopologicalRing R)
      (_ : IsDomain R) (_ : Algebra ℤ_[p] R) (_ : IsLocalHom (algebraMap ℤ_[p] R))
      (_ : Module.Finite ℤ_[p] R) (_ : Module.Free ℤ_[p] R)
      (_ : IsModuleTopology ℤ_[p] R)
      (_ : Algebra R k) (_ : IsScalarTower ℤ_[p] R k) (_ : ContinuousSMul R k)
      (W : Type v) (_ : AddCommGroup W) (_ : Module R W) (_ : Module.Finite R W)
      (_ : Module.Free R W) (hW : Module.rank R W = 2)
      (σ : GaloisRep ℚ R W) (r : k ⊗[R] W ≃ₗ[k] V),
    IsHardlyRamified hpodd hW σ ∧ (σ.baseChange k).conj r = ρ := sorry

Is this zoo of assumptions mathematically equivalent to saying that k is isomorphic to the residue field of R? If so, once the instance of a topological R-algebra is put on the residue field of R, what are the downside of just saying "k is isomorphic to the residue field of R" instead?

[Kevin Buzzard]

Ha ha yes I think so! Feel free to propose another definition here and we can compare and contrast. I just wrote down all these definitions because I wanted to state some theorems formally. I am very open to the statements being changed as long as they remain mathematically essentially the same.