CocycleLifting.lean

theorem finiteCocycle_lift_succ_of_fixed_group
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (θ : Orientation ℓ G) (H : Subgroup G)
    (hH : ∀ n : ℕ, ∀ hn : 1 ≤ n,
      HasH1ReductionSurjective θ H n hn)
    (n : ℕ) (hn : 1 ≤ n) (c : FiniteCocycle θ H n) :
    ∃ d : FiniteCocycle θ H (n + 1),
      ∀ x : H,
        ZMod.castHom (pow_dvd_pow ℓ (Nat.le_succ n))
          (ZMod (ℓ ^ n)) (d.toFun x) = c.toFun x

theorem finiteCocycle_lift_padic_of_fixed_group
    {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (θ : Orientation ℓ G) (H : Subgroup G)
    (hH : ∀ n : ℕ, ∀ hn : 1 ≤ n,
      HasH1ReductionSurjective θ H n hn)
    (n : ℕ) (hn : 1 ≤ n) (c : FiniteCocycle θ H n) :
    ∃ d : PadicCocycle θ H,
      ∀ x : H, PadicInt.toZModPow n (d.toFun x) = c.toFun x