Source: ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
1import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Map
3/-!
4# Completed Group Algebra / All Finite Functoriality / Group-Like
6This module records the action of the all-finite functorial map on canonical group-like elements.
7-/
9open scoped Topology
11namespace CompletedGroupAlgebra
13noncomputable section
15open ProCGroups
16open ProCGroups.ProC
17open ProCGroups.InverseSystems
18open ProCGroups.Completion
20universe u v w
22variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
23variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
26/-- A group element maps to its image in the completed group algebra. -/
27def completedGroupAlgebraOf (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
28 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29 (g : G) : CompletedGroupAlgebraCarrier R G :=
30 toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g)
32/-- Projection of a completed group-like element to a finite quotient stage. -/
33@[simp]
34theorem completedGroupAlgebraProjection_of
35 (U : CompletedGroupAlgebraIndex G) (g : G) :
36 completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g) =
37 MonoidAlgebra.single (openNormalSubgroupInClassProj
38 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 := by
39 rw [completedGroupAlgebraOf, completedGroupAlgebraProjection_toCompletedGroupAlgebra,
40 completedGroupAlgebraStageMap_of]
42/-- The completed group-like element attached to \(1\) is the unit. -/
43@[simp]
44theorem completedGroupAlgebraOf_one :
45 completedGroupAlgebraOf R G 1 = (1 : CompletedGroupAlgebraCarrier R G) := by
46 apply completedGroupAlgebra_ext (R := R) (G := G)
47 intro U
48 rw [completedGroupAlgebraProjection_of, map_one]
49 change MonoidAlgebra.single
50 (openNormalSubgroupInClassProj
51 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U 1) (1 : R) = 1
52 rfl
54/-- Completed group-like elements multiply according to the group law. -/
55@[simp]
56theorem completedGroupAlgebraOf_mul (g h : G) :
57 completedGroupAlgebraOf R G (g * h) =
58 completedGroupAlgebraOf R G g * completedGroupAlgebraOf R G h := by
59 change toCompletedGroupAlgebra R G (MonoidAlgebra.of R G (g * h)) =
60 toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g) *
61 toCompletedGroupAlgebra R G (MonoidAlgebra.of R G h)
62 rw [map_mul (MonoidAlgebra.of R G) g h]
63 have happ (x : MonoidAlgebra R G) :
64 toCompletedGroupAlgebraRingHom R G x = toCompletedGroupAlgebra R G x := rfl
65 have hmul := map_mul (toCompletedGroupAlgebraRingHom R G)
66 (MonoidAlgebra.of R G g) (MonoidAlgebra.of R G h)
67 rw [happ, happ, happ] at hmul
68 exact hmul
70/-- The finite-stage group-like map \(G\to R[G/U]\) is continuous. -/
71theorem continuous_completedGroupAlgebraStageMap_of
72 (U : CompletedGroupAlgebraIndex G) :
73 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
74 (completedGroupAlgebraSystem R G).topologicalSpace U
75 Continuous fun g : G =>
76 completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) := by
77 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
78 (completedGroupAlgebraSystem R G).topologicalSpace U
79 letI : DiscreteTopology (CompletedGroupAlgebraQuotient G U) :=
80 QuotientGroup.discreteTopology
82 (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
83 have hbasis :
84 @Continuous (CompletedGroupAlgebraQuotient G U)
85 (CompletedGroupAlgebraStage R G U) inferInstance
86 ((completedGroupAlgebraSystem R G).topologicalSpace U)
87 (fun q => MonoidAlgebra.single q (1 : R)) :=
88 continuous_of_discreteTopology
89 have hproj :
90 Continuous fun g : G =>
91 openNormalSubgroupInClassProj
92 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g := by
93 change Continuous
94 (QuotientGroup.mk'
95 (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
96 exact continuous_quotient_mk'
97 have hcont := hbasis.comp hproj
98 change @Continuous G (CompletedGroupAlgebraStage R G U) (‹TopologicalSpace G›)
99 ((completedGroupAlgebraSystem R G).topologicalSpace U)
100 (fun g => MonoidAlgebra.single
101 (openNormalSubgroupInClassProj
102 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) (1 : R)) at hcont
103 convert hcont using 1
104 funext g
105 exact completedGroupAlgebraStageMap_of (R := R) (G := G) U g
107/-- The completed group-like map \(G \to \widehat{R[G]}\) is continuous. -/
108theorem continuous_completedGroupAlgebraOf :
109 Continuous (completedGroupAlgebraOf R G) := by
110 let S := completedGroupAlgebraSystem R G
111 letI : ∀ U, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
112 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
113 let π : ∀ U : CompletedGroupAlgebraIndex G,
114 G → CompletedGroupAlgebraStage R G U :=
115 fun U g => completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g)
116 have hπ : ∀ U, Continuous (π U) := by
117 intro U
118 exact continuous_completedGroupAlgebraStageMap_of (R := R) (G := G) U
119 have hcompat : S.CompatibleMaps π := by
120 intro U V hUV
121 funext g
122 exact congrFun
123 (congrArg DFunLike.coe
124 (completedGroupAlgebraStageMap_compatible
125 (R := R) (G := G) hUV))
126 (MonoidAlgebra.of R G g)
127 change Continuous (S.inverseLimitLift π hcompat)
128 exact S.continuous_inverseLimitLift π hπ hcompat
130/--
131The completed functorial map sends the group-like element attached to \(g\) to that of
132\(\varphi(g)\).
133-/
134theorem completedGroupAlgebraMap_of
135 (φ : G →* H) (hφ : Continuous φ) (g : G) :
136 completedGroupAlgebraMap (G := G) (H := H) R φ hφ (completedGroupAlgebraOf R G g) =
137 completedGroupAlgebraOf R H (φ g) := by
138 have h := congrFun
139 (congrArg DFunLike.coe
140 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := H)
141 φ hφ))
142 (MonoidAlgebra.of R G g)
143 simpa [completedGroupAlgebraOf, toCompletedGroupAlgebraRingHom,
144 finiteGroupAlgebra_mapDomainRingHom_of] using h
146/-- The algebra-hom completed functorial map sends group-like elements to their images. -/
147@[simp]
148theorem completedGroupAlgebraMapAlgHom_of
149 (φ : G →* H) (hφ : Continuous φ) (g : G) :
150 completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ
151 (completedGroupAlgebraOf R G g) =
152 completedGroupAlgebraOf R H (φ g) :=
153 completedGroupAlgebraMap_of (R := R) (G := G) (H := H) φ hφ g
154end
156end CompletedGroupAlgebra