Source: ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Projections
1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Ring
3/-!
4# Completed Group Algebra / Basic / All Finite / Projections
6This module bundles the canonical all-finite stage projections and proves continuity of the
7coefficient map through the inverse-limit lifting property.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
19open ProCGroups.Completion
21universe u v
23variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
26/-- The coefficient-ring map \(R \to \widehat{R[G]}\) is continuous. -/
27theorem continuous_completedGroupAlgebra_algebraMap :
28 Continuous (algebraMap R (CompletedGroupAlgebraCarrier R G)) := by
29 let S := completedGroupAlgebraSystem R G
30 letI : ∀ U, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
31 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
32 let π : ∀ U : CompletedGroupAlgebraIndex G,
33 R → CompletedGroupAlgebraStage R G U :=
34 fun U r => algebraMap R (CompletedGroupAlgebraStage R G U) r
35 have hπ : ∀ U, Continuous (π U) := by
36 intro U
37 exact finiteGroupAlgebra_algebraMap_continuous R
38 (CompletedGroupAlgebraQuotient G U)
39 have hcompat : S.CompatibleMaps π := by
40 intro U V hUV
41 funext r
42 exact completedGroupAlgebraTransition_algebraMap
43 (R := R) (G := G) hUV r
44 change Continuous (S.inverseLimitLift π hcompat)
45 exact S.continuous_inverseLimitLift π hπ hcompat
47/-- The canonical projection to a finite stage is bundled as an \(R\)-algebra homomorphism. -/
48def completedGroupAlgebraProjectionAlgHom (R : Type u) (G : Type v) [CommRing R]
49 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
50 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
51 CompletedGroupAlgebraCarrier R G →ₐ[R] CompletedGroupAlgebraStage R G U where
52 toRingHom := completedGroupAlgebraProjection R G U
53 commutes' := by
54 intro r
55 rfl
57/-- The canonical projection to a finite stage, viewed as an \(R\)-linear map. -/
58def completedGroupAlgebraProjectionLinearMap (R : Type u) (G : Type v) [CommRing R]
59 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
60 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
61 CompletedGroupAlgebraCarrier R G →ₗ[R] CompletedGroupAlgebraStage R G U :=
62 (completedGroupAlgebraProjectionAlgHom R G U).toLinearMap
64/-- The finite-stage projection, as a continuous \(R\)-linear map. -/
65def completedGroupAlgebraProjectionContinuousLinearMap (R : Type u) (G : Type v)
66 [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
67 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
68 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
69 (completedGroupAlgebraSystem R G).topologicalSpace U
70 CompletedGroupAlgebraCarrier R G →L[R] CompletedGroupAlgebraStage R G U := by
71 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
72 (completedGroupAlgebraSystem R G).topologicalSpace U
73 exact
74 { toLinearMap := completedGroupAlgebraProjectionLinearMap R G U
75 cont := (completedGroupAlgebraSystem R G).continuous_projection U }
77end
79end CompletedGroupAlgebra