Yamaguchi26AbfaithfulGalois.exists_surjective_padic_character_of_formalHilbert90_trivial
A nonzero prime cyclic character lifts to a surjective p-adic character when the trivial orientation satisfies formal Hilbert 90.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G]Lean source · statement
theorem exists_surjective_padic_character_of_formalHilbert90_trivial
(hF : FormalHilbert90 (1 : Orientation p G))
(χ : G →ₜ* Multiplicative (ZMod p)) (hχ : ∃ g : G, χ g ≠ 1) :
∃ ν : G →ₜ* Multiplicative (PadicInt p), Function.Surjective ν