Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex
ProCGroups/CompletedGroupAlgebra/AllFiniteAugmentation/TerminalIndex

ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex

1 Instance

This file constructs a canonical inhabitant of the open-quotient index used by the all-finite completed group algebra, ensuring that its inverse system is nonempty.

import
Imported by

Declarations

Instance CompletedGroupAlgebra.instNonemptyCompletedGroupAlgebraOpenQuotientIndex 
instance instNonemptyCompletedGroupAlgebraOpenQuotientIndex
    (R : Type u) [CommRing R] [TopologicalSpace R] :
    Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) :=
  inferInstance

The finite quotient index type is nonempty, witnessed by the terminal quotient or canonical base object.