CompletedGroupAlgebra/Basic/InClass/Projection.lean
1import CompletedGroupAlgebra.Basic.InClass.LimitAlgebra
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/InClass/Projection.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Class-Indexed Completed Group Algebras
14Finite-class-indexed inverse systems and inverse limits for completed group algebras.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
27universe u v w
29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33/-- Projection from a `C`-indexed completed group algebra to a finite stage. -/
34abbrev completedGroupAlgebraProjectionInClass
35 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
36 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
37 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
38 (U : CompletedGroupAlgebraIndexInClass G C) :
39 CompletedGroupAlgebraInClass C hC R G → CompletedGroupAlgebraStageInClass C R G U :=
40 (completedGroupAlgebraSystemInClass C hC R G).projection U
42/-- Projection of a coefficient element to a finite stage is the stage algebra map. -/
43@[simp]
45 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
46 (U : CompletedGroupAlgebraIndexInClass G C) (r : R) :
47 completedGroupAlgebraProjectionInClass C hC R G U
48 (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C hC r) =
49 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r :=
50 rfl
52/-- Projection of a coefficient-changed element is coefficient change of the projection. -/
53@[simp]
55 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
56 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
57 (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C)
58 (x : CompletedGroupAlgebraInClass C hC R G) :
59 completedGroupAlgebraProjectionInClass C hC S G U
60 (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C hC S f x) =
61 completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
62 (completedGroupAlgebraProjectionInClass C hC R G U x) :=
63 rfl
65/-- Projection from a `C`-indexed completed group algebra to a finite stage, as a ring
66homomorphism. -/
68 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
69 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
70 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
71 (U : CompletedGroupAlgebraIndexInClass G C) :
72 CompletedGroupAlgebraInClass C hC R G →+* CompletedGroupAlgebraStageInClass C R G U :=
73 projectionRingHom (S := completedGroupAlgebraSystemInClass C hC R G) U
75/-- The ring-hom projection agrees with the underlying stage projection. -/
76@[simp]
78 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
79 (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
80 completedGroupAlgebraProjectionRingHomInClass C hC R G U x =
81 completedGroupAlgebraProjectionInClass C hC R G U x :=
82 rfl
84/-- Projection from a `C`-indexed completed group algebra to a finite stage, as an algebra
85homomorphism. -/
87 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
88 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
89 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
90 (U : CompletedGroupAlgebraIndexInClass G C) :
91 CompletedGroupAlgebraInClass C hC R G →ₐ[R] CompletedGroupAlgebraStageInClass C R G U where
92 toRingHom := completedGroupAlgebraProjectionRingHomInClass C hC R G U
93 commutes' := by
94 intro r
95 rfl
97/-- The algebra-hom projection agrees with the underlying stage projection. -/
98@[simp]
100 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
101 (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
102 completedGroupAlgebraProjectionAlgHomInClass C hC R G U x =
103 completedGroupAlgebraProjectionInClass C hC R G U x :=
104 rfl
106/-- Projection from a `C`-indexed completed group algebra to a finite stage, as an `R`-linear
107map. -/
109 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
110 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
111 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
112 (U : CompletedGroupAlgebraIndexInClass G C) :
113 CompletedGroupAlgebraInClass C hC R G →ₗ[R] CompletedGroupAlgebraStageInClass C R G U where
114 toFun := completedGroupAlgebraProjectionInClass C hC R G U
115 map_add' := by
116 intro x y
117 rfl
118 map_smul' := by
119 intro r x
120 rfl
122/-- The linear-map projection agrees with the underlying stage projection. -/
123@[simp]
125 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
126 (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
127 completedGroupAlgebraProjectionLinearMapInClass C hC R G U x =
128 completedGroupAlgebraProjectionInClass C hC R G U x :=
129 rfl
131/-- The finite-stage projections are compatible with the `C`-indexed transition maps. -/
133 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
134 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
135 (x : CompletedGroupAlgebraInClass C hC R G) :
136 completedGroupAlgebraTransitionInClass C R G hUV
137 (completedGroupAlgebraProjectionInClass C hC R G V x) =
138 completedGroupAlgebraProjectionInClass C hC R G U x :=
139 x.2 U V hUV
141/-- Composing a stage projection with a transition map gives the coarser stage projection. -/
142@[simp]
144 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
145 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
146 (completedGroupAlgebraTransitionInClass C R G hUV).comp
147 (completedGroupAlgebraProjectionRingHomInClass C hC R G V) =
148 completedGroupAlgebraProjectionRingHomInClass C hC R G U := by
149 apply RingHom.ext
150 intro x
151 exact completedGroupAlgebraProjectionInClass_compatible (R := R) (G := G) C hC hUV x
153/-- Continuity of the projection from the `C`-indexed completed group algebra to a stage. -/
155 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
156 (U : CompletedGroupAlgebraIndexInClass G C) :
157 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
158 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
159 Continuous (completedGroupAlgebraProjectionInClass C hC R G U) := by
160 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
161 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
162 exact (completedGroupAlgebraSystemInClass C hC R G).continuous_projection U
164/-- Projection from a `C`-indexed completed group algebra to a finite stage, as a continuous
165`R`-linear map. -/
167 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
168 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
169 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
170 (U : CompletedGroupAlgebraIndexInClass G C) :
171 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
172 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
173 CompletedGroupAlgebraInClass C hC R G →L[R] CompletedGroupAlgebraStageInClass C R G U := by
174 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
175 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
176 exact
177 { toLinearMap := completedGroupAlgebraProjectionLinearMapInClass C hC R G U
178 cont := (completedGroupAlgebraSystemInClass C hC R G).continuous_projection U }
180/-- The continuous linear projection agrees with the underlying stage projection. -/
181@[simp]
183 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
184 (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
185 completedGroupAlgebraProjectionContinuousLinearMapInClass C hC R G U x =
186 completedGroupAlgebraProjectionInClass C hC R G U x :=
187 rfl
190end