theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← GaloisRepresentation.IsHardlyRamified.lifts
⌘↵
Environment
Lean 4.29.1
·
Mathlib v4.29.1
Ubuntu 24.04 LTS · x86_64 · toolchain via elan
timeout 120s lake env lean Check.lean
Details
Posted
13 days ago
Language
Lean 4 / Mathlib
Editor
Upload .lean
textarea
↺ Reset
import Mathlib /-- An irreducible mod p hardly ramified representation lifts to a p-adic one. -/ theorem lifts (ρ : GaloisRep ℚ k V) (hρirred : ρ.IsIrreducible) (hρ : IsHardlyRamified hpodd hV ρ) : ∃ (R : Type u) (_ : CommRing R) (_ : IsLocalRing R) (_ : TopologicalSpace R) (_ : IsTopologicalRing 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
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…