ModuleIndex.lean
Nyll.ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index
5 declarations indexed from sourceView source ↗ Module documentation
Completed Group Algebra / Basic / Within a Class / Index
This module defines the reverse-ordered open normal subgroups whose quotients lie in a finite-group class \(C\), together with their finite quotient groups and canonical quotient projections.
Declarations
CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass
DocumentationThe \(C\)-indexed open-normal quotient tower for a completed group algebra. The order is chosen so that larger indices give finer quotients.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section InClass
CompletedGroupAlgebra.CompletedGroupAlgebraQuotientInClass
DocumentationThe finite quotient \(G/U\) at one \(C\)-indexed stage.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section InClass
CompletedGroupAlgebra.finite_completedGroupAlgebraQuotientInClass
DocumentationQuotients appearing in a finite quotient class are finite.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section InClass
CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass
DocumentationThe terminal \(C\)-indexed completed-group-algebra quotient, corresponding to \(G/G\).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section InClass
CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass_le
DocumentationThe terminal in-class completed-group-algebra index is below every in-class index.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section InClass
omit [IsTopologicalGroup G] in