Source: ProCGroups.CompletedGroupAlgebra.Basic.InClass.Projection
1import ProCGroups.CompletedGroupAlgebra.Basic.InClass.LimitAlgebra
3/-!
4# Completed Group Algebra / Basic / Within a Class / Projection
6This module bundles the canonical \(C\)-indexed finite-stage projection as ring, algebra, linear,
7and continuous linear maps. The underlying projection and compatibility theorem are defined with
8the opaque carrier in `LimitAlgebra`.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
21universe u v w
23variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
27/-- Projection of a coefficient element to a finite stage is the stage algebra map. -/
28@[simp]
29theorem completedGroupAlgebraProjectionInClass_algebraMap
30 (C : ProCGroups.FiniteGroupClass.{v})
31 (U : CompletedGroupAlgebraIndexInClass G C) (r : R) :
32 completedGroupAlgebraProjectionInClass C R G U
33 (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C r) =
34 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r :=
35 rfl
37/-- Projection of a coefficient-changed element is coefficient change of the projection. -/
38@[simp]
39theorem completedGroupAlgebraProjectionInClass_coeffMap
40 (C : ProCGroups.FiniteGroupClass.{v})
41 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
42 (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C)
43 (x : CompletedGroupAlgebraInClass C R G) :
44 completedGroupAlgebraProjectionInClass C S G U
45 (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C S f x) =
46 completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
47 (completedGroupAlgebraProjectionInClass C R G U x) :=
48 rfl
50/--
51The projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as an
52algebra homomorphism.
53-/
54def completedGroupAlgebraProjectionAlgHomInClass
55 (C : ProCGroups.FiniteGroupClass.{v})
56 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
57 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
58 (U : CompletedGroupAlgebraIndexInClass G C) :
59 CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraStageInClass C R G U where
60 toRingHom := completedGroupAlgebraProjectionInClass C R G U
61 commutes' := by
62 intro r
63 rfl
65/-- The projection from a \(C\)-indexed completed group algebra to a finite stage, viewed as an
66\(R\)-linear map. -/
67def completedGroupAlgebraProjectionLinearMapInClass
68 (C : ProCGroups.FiniteGroupClass.{v})
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 R G →ₗ[R] CompletedGroupAlgebraStageInClass C R G U :=
73 (completedGroupAlgebraProjectionAlgHomInClass C R G U).toLinearMap
75/-- Composing a stage projection with a transition map gives the coarser stage projection. -/
76@[simp]
77theorem completedGroupAlgebraTransitionInClass_comp_projection
78 (C : ProCGroups.FiniteGroupClass.{v})
79 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
80 (completedGroupAlgebraTransitionInClass C R G hUV).comp
81 (completedGroupAlgebraProjectionInClass C R G V) =
82 completedGroupAlgebraProjectionInClass C R G U := by
83 apply RingHom.ext
84 intro x
85 exact completedGroupAlgebraProjectionInClass_compatible (R := R) (G := G) C hUV x
87/-- Continuity of the projection from the \(C\)-indexed completed group algebra to a stage. -/
88theorem continuous_completedGroupAlgebraProjectionInClass
89 (C : ProCGroups.FiniteGroupClass.{v})
90 (U : CompletedGroupAlgebraIndexInClass G C) :
91 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
92 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
93 Continuous (completedGroupAlgebraProjectionInClass C R G U) := by
94 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
95 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
96 exact (completedGroupAlgebraSystemInClass C R G).continuous_projection U
98/--
99The projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as a
100continuous \(R\)-linear map.
101-/
102def completedGroupAlgebraProjectionContinuousLinearMapInClass
103 (C : ProCGroups.FiniteGroupClass.{v})
104 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
105 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
106 (U : CompletedGroupAlgebraIndexInClass G C) :
107 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
108 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
109 CompletedGroupAlgebraInClass C R G →L[R] CompletedGroupAlgebraStageInClass C R G U := by
110 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
111 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
112 exact
113 { toLinearMap := completedGroupAlgebraProjectionLinearMapInClass C R G U
114 cont := (completedGroupAlgebraSystemInClass C R G).continuous_projection U }
116end
118end CompletedGroupAlgebra