CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.System
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
def completedGroupAlgebraOpenFiniteQuotientSystem
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
ProCGroups.InverseSystems.InverseSystem
(I := CompletedGroupAlgebraOpenQuotientIndex R G) where
X := CompletedGroupAlgebraOpenFiniteQuotientStage R G
topologicalSpace := completedGroupAlgebraOpenFiniteQuotientStageTopology R G
map := fun {K L} hKL => completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
continuous_map := by
intro K L hKL
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G L) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G L
haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G L) :=
completedGroupAlgebraOpenFiniteQuotientStage_discrete R G L
exact continuous_of_discreteTopology
map_id := by
intro K
exact congrArg DFunLike.coe
(completedGroupAlgebraOpenFiniteQuotientTransition_id R G K)
map_comp := by
intro K L M hKL hLM
exact congrArg DFunLike.coe
(completedGroupAlgebraOpenFiniteQuotientTransition_comp R G hKL hLM)The two-parameter inverse system \(K = (I, U) \mapsto (R/I)[G/U]\) for the kernel-neighborhood topology.
abbrev CompletedGroupAlgebraOpenFiniteQuotientLimit
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
Type (max u v) :=
(completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimitThe two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\) appearing in Ribes--Zalesskii Section 5.3.
abbrev completedGroupAlgebraOpenFiniteQuotientLimitProjection
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
CompletedGroupAlgebraOpenFiniteQuotientLimit R G →
CompletedGroupAlgebraOpenFiniteQuotientStage R G K :=
(completedGroupAlgebraOpenFiniteQuotientSystem R G).projection KThe projection from the two-parameter limit to one quotient \((R/I)[G/U]\).