CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/CanonicalMap.lean
1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Topology
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/CanonicalMap.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 abstract group-algebra map onto an open finite quotient stage is surjective. -/
33 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
34 [TopologicalSpace G] [IsTopologicalGroup G]
35 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
36 Function.Surjective (groupAlgebraOpenFiniteQuotientMap R G K) :=
37 groupAlgebraFiniteQuotientMap_surjective (R := R) (G := G)
38 ((OrderDual.ofDual K.1).1 : Ideal R) K.2
40/-- The abstract group-algebra maps to open finite quotient stages are compatible. -/
42 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
43 [TopologicalSpace G] [IsTopologicalGroup G] :
45 (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
46 groupAlgebraOpenFiniteQuotientMap R G K) := by
47 intro K L hKL
48 funext x
49 exact congrFun
50 (congrArg DFunLike.coe
52 x
54/-- The canonical map from `[R G]` to the two-parameter limit `lim_{I,U}(R/I)[G/U]`. -/
56 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
57 [TopologicalSpace G] [IsTopologicalGroup G]
58 (x : MonoidAlgebra R G) :
60 ⟨fun K => groupAlgebraOpenFiniteQuotientMap R G K x, by
61 intro K L hKL
62 exact congrFun
63 (congrArg DFunLike.coe
65 x⟩
67/-- Projecting the canonical map to the open finite quotient limit recovers the stage quotient map. -/
68@[simp]
70 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
71 [TopologicalSpace G] [IsTopologicalGroup G]
72 (K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : MonoidAlgebra R G) :
75 groupAlgebraOpenFiniteQuotientMap R G K x :=
76 rfl
78/-- The canonical map from `[R G]` to the two-parameter limit, as a ring homomorphism. -/
80 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
81 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
82 MonoidAlgebra R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
83 toFun := toCompletedGroupAlgebraOpenFiniteQuotientLimit R G
84 map_zero' := by
85 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
86 intro K
87 exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)
88 map_one' := by
89 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
90 intro K
91 exact map_one (groupAlgebraOpenFiniteQuotientMap R G K)
92 map_add' x y := by
93 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
94 intro K
95 exact map_add (groupAlgebraOpenFiniteQuotientMap R G K) x y
96 map_mul' x y := by
97 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
98 intro K
99 exact map_mul (groupAlgebraOpenFiniteQuotientMap R G K) x y
101/-- The canonical ring homomorphism to the open finite quotient limit has the expected function. -/
102@[simp]
104 [IsTopologicalRing R]
105 (x : MonoidAlgebra R G) :
108 rfl
110/-- Projection after the canonical ring homomorphism is the corresponding open finite quotient map. -/
111@[simp]
113 [IsTopologicalRing R]
114 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
117 groupAlgebraOpenFiniteQuotientMap R G K := by
118 apply RingHom.ext
119 intro x
120 rfl
122/-- The canonical map to the open finite quotient limit is continuous for the kernel topology. -/
124 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
125 [TopologicalSpace G] [IsTopologicalGroup G] :
126 letI : TopologicalSpace (MonoidAlgebra R G) :=
128 Continuous (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
129 letI : TopologicalSpace (MonoidAlgebra R G) :=
131 let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
132 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
133 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
134 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
135 have hprod : Continuous (groupAlgebraOpenFiniteQuotientProductMap R G) :=
137 change Continuous fun x : MonoidAlgebra R G =>
138 (⟨groupAlgebraOpenFiniteQuotientProductMap R G x, _⟩ :
140 exact Continuous.subtype_mk hprod fun x => (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x).2
142/-- The abstract group algebra has dense image in the two-parameter kernel-neighborhood limit
143`lim_{I,U}(R/I)[G/U]`. -/
145 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
146 [TopologicalSpace G] [IsTopologicalGroup G]
147 [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
148 DenseRange (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
149 let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
150 letI : TopologicalSpace (MonoidAlgebra R G) := ⊥
151 have hdir :
152 Directed (α := CompletedGroupAlgebraOpenQuotientIndex R G) (· ≤ ·) fun K => K :=
154 have hdense :
155 DenseRange
156 (S.inverseLimitLift
157 (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
160 S.denseRange_lift
161 (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
164 (fun K => groupAlgebraOpenFiniteQuotientMap_surjective R G K)
165 hdir
166 simpa [S, toCompletedGroupAlgebraOpenFiniteQuotientLimit] using hdense
168end