Source: ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Ring
1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Carrier
3/-!
4# Completed Group Algebra / Basic / All Finite / Ring Maps
6The carrier and its algebraic structures come from the single generic inverse-limit construction.
7This module adds the stagewise coefficient-change map and the coefficient algebra map. Generic
8ring-homomorphism lemmas apply directly to the canonical bundled projections.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v w
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
27/-- The all-finite completed-group-algebra coefficient-change map, obtained from the unique
28inverse-limit lift of the stagewise coefficient maps. -/
29def completedGroupAlgebraCoeffMap
30 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
31 (f : R →+* S) :
32 CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraCarrier S G where
33 toFun x :=
34 (completedGroupAlgebraCompatibleFamilyEquiv (R := S) (G := G)).symm
35 ((completedGroupAlgebraSystem S G).inverseLimitLift
36 (fun U x =>
37 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
38 (completedGroupAlgebraProjection R G U x))
39 (by
40 intro U V hUV
41 funext x
42 have hcompat := congrFun
43 (congrArg DFunLike.coe
44 (completedGroupAlgebraStageCoeffMap_compatible
45 (R := R) (G := G) S f hUV))
46 (completedGroupAlgebraProjection R G V x)
47 calc
48 completedGroupAlgebraTransition S G hUV
49 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V
50 (completedGroupAlgebraProjection R G V x))
51 =
52 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
53 (completedGroupAlgebraTransition R G hUV
54 (completedGroupAlgebraProjection R G V x)) := hcompat.symm
55 _ =
56 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
57 (completedGroupAlgebraProjection R G U x) := by
58 rw [completedGroupAlgebraProjection_compatible]) x)
59 map_zero' := by
60 apply completedGroupAlgebra_ext (R := S) (G := G)
61 intro U
62 exact map_zero (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
63 map_one' := by
64 apply completedGroupAlgebra_ext (R := S) (G := G)
65 intro U
66 exact map_one (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
67 map_add' x y := by
68 apply completedGroupAlgebra_ext (R := S) (G := G)
69 intro U
70 exact map_add (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
71 (completedGroupAlgebraProjection R G U x)
72 (completedGroupAlgebraProjection R G U y)
73 map_mul' x y := by
74 apply completedGroupAlgebra_ext (R := S) (G := G)
75 intro U
76 exact map_mul (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
77 (completedGroupAlgebraProjection R G U x)
78 (completedGroupAlgebraProjection R G U y)
80/-- Projection commutes with stagewise coefficient change. -/
81@[simp]
82theorem completedGroupAlgebraProjection_coeffMap
83 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
84 (f : R →+* S) (U : CompletedGroupAlgebraIndex G)
85 (x : CompletedGroupAlgebraCarrier R G) :
86 completedGroupAlgebraProjection S G U
87 (completedGroupAlgebraCoeffMap (R := R) (G := G) S f x) =
88 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
89 (completedGroupAlgebraProjection R G U x) :=
90 rfl
92omit [TopologicalSpace R] [IsTopologicalRing R] in
93/-- Transition maps preserve scalar elements from the coefficient ring. -/
94theorem completedGroupAlgebraTransition_algebraMap
95 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (r : R) :
96 completedGroupAlgebraTransition R G hUV
97 (algebraMap R (CompletedGroupAlgebraStage R G V) r) =
98 algebraMap R (CompletedGroupAlgebraStage R G U) r := by
99 simp only [completedGroupAlgebraTransition, MonoidAlgebra.coe_algebraMap,
100 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
101 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single, map_one]
103/-- The coefficient-ring map is the inverse-limit lift of the finite-stage algebra maps. -/
104def completedGroupAlgebraAlgebraMap
105 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
106 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
107 R →+* CompletedGroupAlgebraCarrier R G where
108 toFun r :=
109 (completedGroupAlgebraCompatibleFamilyEquiv (R := R) (G := G)).symm
110 ((completedGroupAlgebraSystem R G).inverseLimitLift
111 (fun U r => algebraMap R (CompletedGroupAlgebraStage R G U) r)
112 (by
113 intro U V hUV
114 funext r
115 exact completedGroupAlgebraTransition_algebraMap
116 (R := R) (G := G) hUV r) r)
117 map_zero' := by
118 apply completedGroupAlgebra_ext (R := R) (G := G)
119 intro U
120 exact map_zero (algebraMap R (CompletedGroupAlgebraStage R G U))
121 map_one' := by
122 apply completedGroupAlgebra_ext (R := R) (G := G)
123 intro U
124 exact map_one (algebraMap R (CompletedGroupAlgebraStage R G U))
125 map_add' r s := by
126 apply completedGroupAlgebra_ext (R := R) (G := G)
127 intro U
128 exact map_add (algebraMap R (CompletedGroupAlgebraStage R G U)) r s
129 map_mul' r s := by
130 apply completedGroupAlgebra_ext (R := R) (G := G)
131 intro U
132 exact map_mul (algebraMap R (CompletedGroupAlgebraStage R G U)) r s
134/-- The completed group algebra is an algebra over its coefficient ring. -/
135instance instAlgebraCompletedGroupAlgebra :
136 Algebra R (CompletedGroupAlgebraCarrier R G) where
137 algebraMap := completedGroupAlgebraAlgebraMap (R := R) (G := G)
138 commutes' := by
139 intro r x
140 apply completedGroupAlgebra_ext (R := R) (G := G)
141 intro U
142 exact Algebra.commutes r (completedGroupAlgebraProjection R G U x)
143 smul_def' := by
144 intro r x
145 apply completedGroupAlgebra_ext (R := R) (G := G)
146 intro U
147 change r • completedGroupAlgebraProjection R G U x =
148 algebraMap R (CompletedGroupAlgebraStage R G U) r *
149 completedGroupAlgebraProjection R G U x
150 rw [Algebra.smul_def]
152end
154end CompletedGroupAlgebra