Source: ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation
3/-!
4# Completed Group Algebra / Basic / Within a Class / Index
6This module defines the reverse-ordered open normal subgroups whose quotients lie in a finite-group
7class \(C\), together with their finite quotient groups and canonical quotient projections.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
20universe u v w
22variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24section InClass
26/--
27The \(C\)-indexed open-normal quotient tower for a completed group algebra. The order is chosen
28so that larger indices give finer quotients.
29-/
30abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{v}) :=
31 OrderDual (OpenNormalSubgroupInClass C G)
33/-- The finite quotient \(G/U\) at one \(C\)-indexed stage. -/
34abbrev CompletedGroupAlgebraQuotientInClass (C : ProCGroups.FiniteGroupClass.{v})
35 (U : CompletedGroupAlgebraIndexInClass G C) : Type v :=
36 (openNormalSubgroupInClassSystem C G).X U
38/-- Quotients appearing in a finite quotient class are finite. -/
39theorem finite_completedGroupAlgebraQuotientInClass
40 (C : ProCGroups.FiniteGroupClass.{v})
41 (U : CompletedGroupAlgebraIndexInClass G C) :
42 Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
43 C.finite (OrderDual.ofDual U).2
45/-- The terminal \(C\)-indexed completed-group-algebra quotient, corresponding to \(G/G\). -/
46def terminalCompletedGroupAlgebraIndexInClass
47 (C : ProCGroups.FiniteGroupClass.{v})
49 CompletedGroupAlgebraIndexInClass G C :=
50 OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G))
52omit [IsTopologicalGroup G] in
53/-- The terminal in-class completed-group-algebra index is below every in-class index. -/
54theorem terminalCompletedGroupAlgebraIndexInClass_le
55 (C : ProCGroups.FiniteGroupClass.{v})
57 (U : CompletedGroupAlgebraIndexInClass G C) :
58 terminalCompletedGroupAlgebraIndexInClass (G := G) C ≤ U := by
59 change ((OrderDual.ofDual U).1 : Subgroup G) ≤ (⊤ : Subgroup G)
60 exact le_top
62variable (R : Type u) [CommRing R]
64end InClass
66end
68end CompletedGroupAlgebra