ClassFieldTower.ProP.exists_finiteStage_invariant_character_family
A finite family of invariant continuous characters descends to one common finite stage.
Each descended character pulls back to the original one and remains invariant under conjugation. Moreover, a pointwise ZMod p-linear combination of the descended family vanishes identically if and only if the corresponding combination of the original family vanishes identically.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u v
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [IsTopologicalGroup F] [CompactSpace F] [T2Space F]
[TotallyDisconnectedSpace F] inLean source · statement
theorem exists_finiteStage_invariant_character_family
{ι : Type v} [Fintype ι]
(hF : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) F)
(R : ClosedSubgroup F) [R.Normal]
(χ : ι → R →ₜ* Multiplicative (ZMod p))
(hχinv : ∀ (i : ι) (f : F) (r : R),
χ i (MulAut.conjNormal f r) = χ i r) :
∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F,
∃ χbar : ι → MonoidHom (finiteStageImage R U) (Multiplicative (ZMod p)),
(∀ i, (χbar i).comp (finiteStageImageMap R U) = (χ i).toMonoidHom) ∧
(∀ (i : ι) (g : F ⧸ (U.1 : Subgroup F)) (n : finiteStageImage R U),
χbar i (MulAut.conjNormal g n) = χbar i n) ∧
∀ a : ι → ZMod p,
(∀ n : finiteStageImage R U,
∑ i, a i * (χbar i n).toAdd = 0) ↔
∀ r : R, ∑ i, a i * (χ i r).toAdd = 0