Source: ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex
1import ProCGroups.CompletedGroupAlgebra.Separation
3/-!
4# A base index for all-finite augmentation
6This file constructs a canonical inhabitant of the open-quotient index used by the all-finite
7completed group algebra, ensuring that its inverse system is nonempty.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
19open ProCGroups.Completion
21universe u v w
23variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27/--
28The finite quotient index type is nonempty, witnessed by the terminal quotient or canonical base
29object.
30-/
31instance instNonemptyCompletedGroupAlgebraOpenQuotientIndex
32 (R : Type u) [CommRing R] [TopologicalSpace R] :
33 Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) :=
34 inferInstance
35end
37end CompletedGroupAlgebra