Yamaguchi26AbfaithfulGalois.exists_openNormal_padicCocycle_lifting_character
A finite character on the closed kernel of an orientation extends to a p-adic cocycle on an open normal supergroup, using precisely the relative formal Hilbert 90 hypothesis.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe uLean source · statement
theorem exists_openNormal_padicCocycle_lifting_character
{ℓ : ℕ} [Fact ℓ.Prime]
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(D : Subgroup G) [D.Normal] (hDclosed : IsClosed (D : Set G))
(θ : Orientation ℓ G) (hDθ : D ≤ θ.toMonoidHom.ker)
(hLift : RelativeFormalHilbert90 D θ)
(n : ℕ) (hn : 1 ≤ n) (χ : D →ₜ* Multiplicative (ZMod (ℓ ^ n))) :
∃ U : OpenNormalSubgroup G, ∃ hDU : D ≤ (U : Subgroup G),
∃ c : PadicCocycle θ (U : Subgroup G), ∀ d : D,
PadicInt.toZModPow n (c.toFun (Subgroup.inclusion hDU d)) = (χ d).toAdd