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

CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex

1 Instance

This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.

Open this file on GitHub
import
Imported by

Declarations

Instance CompletedGroupAlgebra.instNonemptyCompletedGroupAlgebraOpenQuotientIndex GitHub 
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.