Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Topology
3/-!
4# Completed Group Algebra / Open Finite Quotient Topology / Open Finite Limit / Canonical Map
6This module lifts the compatible open-finite quotient maps from the abstract group algebra to the
7named two-parameter completion, and proves its projection, continuity, and density properties.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
19open ProCGroups.Completion
21universe u v
23variable (R : Type u) [CommRing R] [TopologicalSpace R]
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26/-- The abstract group-algebra map onto an open-finite quotient stage is surjective. -/
27theorem groupAlgebraOpenFiniteQuotientMap_surjective
28 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
29 [TopologicalSpace G] [IsTopologicalGroup G]
30 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
31 Function.Surjective (groupAlgebraOpenFiniteQuotientMap R G K) :=
32 groupAlgebraFiniteQuotientMap_surjective (R := R) (G := G)
33 ((OrderDual.ofDual K.1).1 : Ideal R) K.2
35/-- The abstract group-algebra maps to open-finite quotient stages are compatible. -/
36theorem groupAlgebraOpenFiniteQuotientMap_compatibleMaps
37 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
38 [TopologicalSpace G] [IsTopologicalGroup G] :
39 (completedGroupAlgebraOpenFiniteQuotientSystem R G).CompatibleMaps
40 (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
41 groupAlgebraOpenFiniteQuotientMap R G K) := by
42 intro K L hKL
43 funext x
44 exact congrFun
45 (congrArg DFunLike.coe
46 (completedGroupAlgebraOpenFiniteQuotientTransition_comp_map R G hKL))
47 x
49/--
50The two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\) appearing in Ribes--Zalesskii
51Section 5.3.
52-/
53def toCompletedGroupAlgebraOpenFiniteQuotientLimit
54 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
55 [TopologicalSpace G] [IsTopologicalGroup G]
56 (x : MonoidAlgebra R G) :
57 CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
58 (completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv
59 (R := R) (G := G)).symm
60 ((completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimitLift
61 (fun K => groupAlgebraOpenFiniteQuotientMap R G K)
62 (groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G) x)
64/--
65Projecting the canonical map to the open-finite quotient limit recovers the stage quotient map.
66-/
67@[simp]
68theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_toLimit
69 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
70 [TopologicalSpace G] [IsTopologicalGroup G]
71 (K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : MonoidAlgebra R G) :
72 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
73 (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x) =
74 groupAlgebraOpenFiniteQuotientMap R G K x :=
75 rfl
77/-- The canonical map from \(R[G]\) to the two-parameter limit is bundled as a ring homomorphism. -/
78def toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom
79 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
80 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
81 MonoidAlgebra R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
82 toFun := toCompletedGroupAlgebraOpenFiniteQuotientLimit R G
83 map_zero' := by
84 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
85 intro K
86 exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)
87 map_one' := by
88 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
89 intro K
90 exact map_one (groupAlgebraOpenFiniteQuotientMap R G K)
91 map_add' x y := by
92 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
93 intro K
94 exact map_add (groupAlgebraOpenFiniteQuotientMap R G K) x y
95 map_mul' x y := by
96 apply completedGroupAlgebraOpenFiniteQuotientLimit_ext (R := R) (G := G)
97 intro K
98 exact map_mul (groupAlgebraOpenFiniteQuotientMap R G K) x y
100/--
101The bundled ring homomorphism has the same underlying function as the coordinatewise
102construction.
103-/
104@[simp]
105theorem toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom_apply
106 (x : MonoidAlgebra R G) :
107 toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G x =
108 toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x :=
109 rfl
111/-- Projection after the canonical ring homomorphism is the corresponding open-finite quotient
112map. -/
113@[simp]
114theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_comp_toLimit
115 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
116 (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K).comp
117 (toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G) =
118 groupAlgebraOpenFiniteQuotientMap R G K := by
119 apply RingHom.ext
120 intro x
121 rfl
123/-- The canonical map to the open-finite quotient limit is continuous for the kernel topology. -/
124theorem continuous_toCompletedGroupAlgebraOpenFiniteQuotientLimit_kernelTopology
125 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
126 [TopologicalSpace G] [IsTopologicalGroup G] :
127 letI : TopologicalSpace (MonoidAlgebra R G) :=
128 groupAlgebraOpenFiniteQuotientKernelTopology R G
129 Continuous (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
130 letI : TopologicalSpace (MonoidAlgebra R G) :=
131 groupAlgebraOpenFiniteQuotientKernelTopology R G
132 let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
133 letI : ∀ K, TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
134 fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K
135 let π : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
136 MonoidAlgebra R G → CompletedGroupAlgebraOpenQuotientStage R G K :=
137 fun K => groupAlgebraOpenFiniteQuotientMap R G K
138 have hπ : ∀ K, Continuous (π K) := by
139 intro K
140 exact continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology R G K
141 have hcompat : S.CompatibleMaps π :=
142 groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G
143 change Continuous (S.inverseLimitLift π hcompat)
144 exact S.continuous_inverseLimitLift π hπ hcompat
146/--
147The canonical map from `R[G]` has dense range in the two-parameter inverse limit
148\(\varprojlim_{I,U}(R/I)[G/U]\).
149-/
150theorem denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit
151 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
152 [TopologicalSpace G] [IsTopologicalGroup G]
153 [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
154 DenseRange (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
155 let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
156 letI : TopologicalSpace (MonoidAlgebra R G) := ⊥
157 have hdir :
158 Directed (α := CompletedGroupAlgebraOpenQuotientIndex R G) (· ≤ ·) fun K => K :=
159 directed_completedGroupAlgebraOpenQuotientIndex R G
160 have hdense :
161 DenseRange
162 (S.inverseLimitLift
163 (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
164 groupAlgebraOpenFiniteQuotientMap R G K)
165 (groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G)) :=
166 S.denseRange_lift
167 (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
168 groupAlgebraOpenFiniteQuotientMap R G K)
169 (groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G)
170 (fun K => groupAlgebraOpenFiniteQuotientMap_surjective R G K)
171 hdir
172 change DenseRange
173 (S.inverseLimitLift
174 (fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
175 groupAlgebraOpenFiniteQuotientMap R G K)
176 (groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G))
177 exact hdense
179end
181end CompletedGroupAlgebra