Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.AddCommGroup
3/-!
4# Fox differential: coefficient rings — mod-\(n\) completed group algebra — system — completion map
6The principal declarations in this module are:
8- `toModNCompletedGroupAlgebra`
9 The canonical map \((\mathbb{Z}/n\mathbb{Z})[G] \to \varprojlim_U (\mathbb{Z}/n\mathbb{Z})[G/U]\).
10- `modNCompletedGroupAlgebraStageMap_compatibleMaps`
11 The mod-\(n\) completed group-algebra stage maps are compatible with transition maps and
12 coordinate projections.
13- `modNCompletedGroupAlgebraProjection_toCompleted`
14 The finite-stage projection to the completed mod-\(n\) group algebra is given by the corresponding
15 coordinate formula.
16-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups.InverseSystems
23open ProCGroups.ProC
25universe u
28variable (n : ℕ) [Fact (0 < n)]
29variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31omit [Fact (0 < n)] in
32/--
33The mod-\(n\) completed group-algebra stage maps are compatible with transition maps and
34coordinate projections.
35-/
36theorem modNCompletedGroupAlgebraStageMap_compatibleMaps :
37 (modNCompletedGroupAlgebraSystem n G).CompatibleMaps
38 (fun U => modNCompletedGroupAlgebraStageMap n G U) := by
39 intro U V hUV
40 funext x
41 exact congrFun
42 (congrArg DFunLike.coe
43 (modNCompletedGroupAlgebraStageMap_compatible (n := n) (G := G) (U := U) (V := V) hUV))
44 x
46/--
47The canonical map \((\mathbb{Z}/n\mathbb{Z})[G] \to \varprojlim_U
48(\mathbb{Z}/n\mathbb{Z})[G/U]\).
49-/
50def toModNCompletedGroupAlgebra :
51 ModNCompletedGroupRing n G → ModNCompletedGroupAlgebra n G := by
52 letI : TopologicalSpace (ModNCompletedGroupRing n G) := ⊥
53 exact
54 (modNCompletedGroupAlgebraSystem n G).inverseLimitLift
55 (fun U => modNCompletedGroupAlgebraStageMap n G U)
56 (modNCompletedGroupAlgebraStageMap_compatibleMaps (n := n) (G := G))
58omit [Fact (0 < n)] in
59/--
60The finite-stage projection to the completed mod-\(n\) group algebra is given by the
61corresponding coordinate formula.
62-/
63@[simp]
64theorem modNCompletedGroupAlgebraProjection_toCompleted
65 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x : ModNCompletedGroupRing
66 n G) :
67 modNCompletedGroupAlgebraProjection n G U (toModNCompletedGroupAlgebra n G x) =
68 modNCompletedGroupAlgebraStageMap n G U x := by
69 rfl
71end
73end FoxDifferential