CompletedGroupAlgebra/Basic/AllFinite/Projections.lean
1import CompletedGroupAlgebra.Basic.AllFinite.Ring
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/AllFinite/Projections.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Linear and algebraic projections
14This module records the finite-stage projections of the all-finite completed group algebra and their compatibility with the transition maps.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
26open ProCGroups.Completion
28universe u v w
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33/-- The coefficient-ring map `R -> [[RG]]` is continuous. -/
35 Continuous (algebraMap R (Carrier R G)) := by
36 letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
37 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
38 have hval : Continuous fun r : R =>
39 fun U : CompletedGroupAlgebraIndex G =>
40 (show CompletedGroupAlgebraStage R G U from
41 (algebraMap R (Carrier R G) r).1 U) := by
42 change Continuous fun r : R =>
43 fun U : CompletedGroupAlgebraIndex G =>
44 algebraMap R (CompletedGroupAlgebraStage R G U) r
45 apply continuous_pi
46 intro U
48 exact Continuous.subtype_mk hval fun r => (algebraMap R (Carrier R G) r).2
50/-- The canonical projection to a finite stage, as an `R`-linear map. -/
51def completedGroupAlgebraProjectionLinearMap (R : Type u) (G : Type v) [CommRing R]
52 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
53 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
54 Carrier R G →ₗ[R] CompletedGroupAlgebraStage R G U where
55 toFun := completedGroupAlgebraProjection R G U
56 map_add' := completedGroupAlgebraProjection_add (R := R) (G := G) U
57 map_smul' := completedGroupAlgebraProjection_smul (R := R) (G := G) U
59/-- The finite-stage projection, as a continuous `R`-linear map. -/
60def completedGroupAlgebraProjectionContinuousLinearMap (R : Type u) (G : Type v)
61 [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
62 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
63 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
64 (completedGroupAlgebraSystem R G).topologicalSpace U
65 Carrier R G →L[R] CompletedGroupAlgebraStage R G U := by
66 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
67 (completedGroupAlgebraSystem R G).topologicalSpace U
68 exact
69 { toLinearMap := completedGroupAlgebraProjectionLinearMap R G U
70 cont := (completedGroupAlgebraSystem R G).continuous_projection U }
72/-- The canonical projection to a finite stage, as a ring homomorphism. -/
73def completedGroupAlgebraProjectionRingHom (R : Type u) (G : Type v) [CommRing R]
74 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
75 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
76 Carrier R G →+* CompletedGroupAlgebraStage R G U where
77 toFun := completedGroupAlgebraProjection R G U
78 map_zero' := completedGroupAlgebraProjection_zero (R := R) (G := G) U
79 map_one' := completedGroupAlgebraProjection_one (R := R) (G := G) U
80 map_add' := completedGroupAlgebraProjection_add (R := R) (G := G) U
81 map_mul' := completedGroupAlgebraProjection_mul (R := R) (G := G) U
83/-- The canonical projection to a finite stage, as an `R`-algebra homomorphism. -/
84def completedGroupAlgebraProjectionAlgHom (R : Type u) (G : Type v) [CommRing R]
85 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
86 [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
87 Carrier R G →ₐ[R] CompletedGroupAlgebraStage R G U where
88 toRingHom := completedGroupAlgebraProjectionRingHom R G U
89 commutes' := by
90 intro r
91 rfl
93end