ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index

2 Theorems | 1 Definition | 2 Abbreviations

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.

import

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation

Imported by

Abbreviation CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass

abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{v}) :=
  OrderDual (OpenNormalSubgroupInClass C G)

The \(C\)-indexed open-normal quotient tower for a completed group algebra. The order is chosen so that larger indices give finer quotients.

Abbreviation CompletedGroupAlgebra.CompletedGroupAlgebraQuotientInClass

abbrev CompletedGroupAlgebraQuotientInClass (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) : Type v :=
  (openNormalSubgroupInClassSystem C G).X U

The finite quotient \(G/U\) at one \(C\)-indexed stage.

Theorem CompletedGroupAlgebra.finite_completedGroupAlgebraQuotientInClass

theorem finite_completedGroupAlgebraQuotientInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Finite (CompletedGroupAlgebraQuotientInClass G C U)

Quotients appearing in a finite quotient class are finite.

Show Lean proof

Definition CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass

def terminalCompletedGroupAlgebraIndexInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    CompletedGroupAlgebraIndexInClass G C :=
  OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G))

The terminal \(C\)-indexed completed-group-algebra quotient, corresponding to \(G/G\).

Theorem CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass_le

omit [IsTopologicalGroup G] in
theorem terminalCompletedGroupAlgebraIndexInClass_le
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    terminalCompletedGroupAlgebraIndexInClass (G := G) C ≤ U

The terminal in-class completed-group-algebra index is below every in-class index.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index

Declarations