Yamaguchi26AbfaithfulGalois.exists_primaryCharacter_transfer_fixed
Transfer of a p-adic character evaluates on a globally fixed primary class as multiplication by the index of the open normal subgroup.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe uLean source · statement
theorem exists_primaryCharacter_transfer_fixed
{ℓ : ℕ} [Fact ℓ.Prime]
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
(D : Subgroup G) [D.Normal] (hD : IsClosed (D : Set G))
(U : OpenNormalSubgroup G) (hDU : D ≤ (U : Subgroup G))
(χ : (U : Subgroup G) →ₜ* Multiplicative (PadicInt ℓ))
(f : PrimaryAbelianization ℓ D →ₜ* Multiplicative (PadicInt ℓ))
(hχ : ∀ d : D, χ (Subgroup.inclusion hDU d) =
f (QuotientGroup.mk' (proCResidualCore (ProCGroups.FiniteGroupClass.pGroup ℓ)
(TopologicalAbelianization D)) (TopologicalAbelianization.mk D d))) :
∃ F : GroupPrimaryAbelianization ℓ G →ₜ* Multiplicative (PadicInt ℓ),
∀ a : PrimaryAbelianization ℓ D,
a ∈ primaryFixedSubgroup ℓ D hD (⊤ : Subgroup G) →
F (primaryInclusionMap ℓ D hD a) =
f a ^ Nat.card (G ⧸ (U : Subgroup G))