CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/System.lean
1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/System.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
23open ProCGroups.InverseSystems
24open ProCGroups.Completion
26universe u v
28variable (R : Type u) [CommRing R] [TopologicalSpace R]
29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31/-- The two-parameter inverse system `K = (I,U) ↦ (R/I)[G/U]` for the
32kernel-neighborhood topology. -/
34 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
35 [TopologicalSpace G] [IsTopologicalGroup G] :
37 (I := CompletedGroupAlgebraOpenQuotientIndex R G) where
39 topologicalSpace := completedGroupAlgebraOpenFiniteQuotientStageTopology R G
40 map := fun {K L} hKL => completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
41 continuous_map := by
42 intro K L hKL
43 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
45 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G L) :=
47 haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G L) :=
49 exact continuous_of_discreteTopology
50 map_id := by
51 intro K
52 exact congrArg DFunLike.coe
54 map_comp := by
55 intro K L M hKL hLM
56 exact congrArg DFunLike.coe
57 (completedGroupAlgebraOpenFiniteQuotientTransition_comp R G hKL hLM)
59/-- The two-parameter inverse limit appearing in RZ §5.3,
60`lim_{I,U} (R/I)[G/U]`. -/
62 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
63 [TopologicalSpace G] [IsTopologicalGroup G] :
64 Type (max u v) :=
65 (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit
67/-- Projection from the two-parameter limit to one quotient `(R/I)[G/U]`. -/
69 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
70 [TopologicalSpace G] [IsTopologicalGroup G]
71 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
74 (completedGroupAlgebraOpenFiniteQuotientSystem R G).projection K
76end