Source: ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Carrier
1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Stage
3/-!
4# Completed Group Algebra / Basic / All Finite / Carrier
6This module defines the all-finite completed group algebra as a named inverse-limit carrier.
7Its compatible-family realization is available only through the explicit equivalence, coordinate
8projection, compatibility, and extensionality API below. Ring and module structures are inherited
9once from the generic inverse-limit construction.
10-/
12open scoped Topology
14namespace CompletedGroupAlgebra
16noncomputable section
18open ProCGroups
19open ProCGroups.ProC
20open ProCGroups.InverseSystems
21open ProCGroups.Completion
23universe u v
25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
28/-- The all-finite completed group algebra
29\(\widehat{R[G]}=\varprojlim_U R[G/U]\), kept opaque from its compatible-family model. -/
30def CompletedGroupAlgebraCarrier (R : Type u) (G : Type v) [CommRing R]
31 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
32 [IsTopologicalGroup G] : Type (max u v) :=
33 (completedGroupAlgebraSystem R G).inverseLimit
35/-- The completed group algebra carries the inverse-limit topology of its finite stages. -/
36instance instTopologicalSpaceCompletedGroupAlgebraCarrier :
37 TopologicalSpace (CompletedGroupAlgebraCarrier R G) :=
38 inferInstanceAs (TopologicalSpace (completedGroupAlgebraSystem R G).inverseLimit)
40/-- Explicit exchange between the named completed carrier and the concrete compatible-family
41realization. Ordinary code should use finite-stage projections instead. -/
42def completedGroupAlgebraCompatibleFamilyEquiv
43 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
44 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
45 CompletedGroupAlgebraCarrier R G ≃
46 (completedGroupAlgebraSystem R G).inverseLimit :=
47 Equiv.refl _
49local instance (U : CompletedGroupAlgebraIndex G) :
50 Ring ((completedGroupAlgebraSystem R G).X U) := by
51 change Ring (CompletedGroupAlgebraStage R G U)
52 infer_instance
54local instance (U : CompletedGroupAlgebraIndex G) :
55 Module R ((completedGroupAlgebraSystem R G).X U) := by
56 change Module R (CompletedGroupAlgebraStage R G U)
57 infer_instance
59/-- The all-finite tower is a ring-valued inverse system. -/
60instance instIsRingSystemCompletedGroupAlgebraSystem :
61 IsRingSystem (completedGroupAlgebraSystem R G) where
62 map_zero := by
63 intro U V hUV
64 exact map_zero (completedGroupAlgebraTransition R G hUV)
65 map_one := by
66 intro U V hUV
67 exact map_one (completedGroupAlgebraTransition R G hUV)
68 map_add := by
69 intro U V hUV x y
70 exact map_add (completedGroupAlgebraTransition R G hUV) x y
71 map_mul := by
72 intro U V hUV x y
73 exact map_mul (completedGroupAlgebraTransition R G hUV) x y
75/-- The ring structure is inherited once from the generic ring inverse limit. -/
76instance instRingCompletedGroupAlgebra :
77 Ring (CompletedGroupAlgebraCarrier R G) := by
78 change Ring (completedGroupAlgebraSystem R G).inverseLimit
79 infer_instance
81/-- The canonical finite-stage projection, bundled at its source as a ring homomorphism. -/
82def completedGroupAlgebraProjection
83 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
84 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
85 (U : CompletedGroupAlgebraIndex G) :
86 CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraStage R G U := by
87 change (completedGroupAlgebraSystem R G).inverseLimit →+*
88 (completedGroupAlgebraSystem R G).X U
89 exact projectionRingHom (S := completedGroupAlgebraSystem R G) U
91/-- The canonical projections satisfy the inverse-system compatibility equations. -/
92@[simp]
93theorem completedGroupAlgebraProjection_compatible
94 (x : CompletedGroupAlgebraCarrier R G)
95 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
96 completedGroupAlgebraTransition R G hUV
97 (completedGroupAlgebraProjection R G V x) =
98 completedGroupAlgebraProjection R G U x :=
99 by
100 change (completedGroupAlgebraSystem R G).map hUV
101 ((completedGroupAlgebraSystem R G).projection V x) =
102 (completedGroupAlgebraSystem R G).projection U x
103 exact (completedGroupAlgebraSystem R G).projection_compatible x U V hUV
105/-- Completed elements are equal when all bundled finite-stage projections agree. -/
106@[ext]
107theorem completedGroupAlgebra_ext {x y : CompletedGroupAlgebraCarrier R G}
108 (h : ∀ U, completedGroupAlgebraProjection R G U x =
109 completedGroupAlgebraProjection R G U y) :
110 x = y := by
111 apply (completedGroupAlgebraSystem R G).ext
112 intro U
113 exact h U
115omit [TopologicalSpace R] [IsTopologicalRing R] in
116/-- Transition maps commute with coefficient scalar multiplication. -/
117theorem completedGroupAlgebraTransition_smul
118 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
119 (r : R) (x : CompletedGroupAlgebraStage R G V) :
120 completedGroupAlgebraTransition R G hUV (r • x) =
121 r • completedGroupAlgebraTransition R G hUV x := by
122 rw [Algebra.smul_def, Algebra.smul_def, map_mul]
123 congr 1
124 change
125 MonoidAlgebra.mapDomain
126 (OpenNormalSubgroupInClass.map
127 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
128 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
129 (MonoidAlgebra.single 1 r) =
130 MonoidAlgebra.single 1 r
131 rw [MonoidAlgebra.mapDomain_single, map_one]
133/-- The all-finite tower is a module-valued inverse system over its coefficient ring. -/
134instance instIsModuleSystemCompletedGroupAlgebra :
135 IsModuleSystem R (completedGroupAlgebraSystem R G) where
136 map_smul := completedGroupAlgebraTransition_smul (R := R) (G := G)
138/-- The module structure is inherited once from the generic module inverse limit. -/
139instance instModuleCoeffCompletedGroupAlgebra :
140 Module R (CompletedGroupAlgebraCarrier R G) := by
141 change Module R (completedGroupAlgebraSystem R G).inverseLimit
142 infer_instance
144end
146end CompletedGroupAlgebra