Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.GroupLike
1import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Maps
3/-!
4# Completed Group Algebra / Functoriality Within a Class / Group-Like
6This module constructs the \(C\)-indexed completed group-like map through the canonical dense map,
7and characterizes it by finite-stage projections, multiplication, and continuity.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
19open ProCGroups.Completion
21universe u v
23variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27/-- A group element maps to its image in the \(C\)-indexed completed group algebra. -/
28def completedGroupAlgebraOfInClass
29 (C : ProCGroups.FiniteGroupClass.{v})
30 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
31 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32 (g : G) : CompletedGroupAlgebraInClass C R G :=
33 toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g)
35/-- Projection of a class-indexed completed group-like element to a finite quotient stage. -/
36@[simp]
37theorem completedGroupAlgebraProjectionInClass_of
38 (C : ProCGroups.FiniteGroupClass.{v})
39 (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
40 completedGroupAlgebraProjectionInClass C R G U
41 (completedGroupAlgebraOfInClass C R G g) =
42 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by
43 rw [completedGroupAlgebraOfInClass,
44 completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass,
45 completedGroupAlgebraStageMapInClass_of]
47/-- The class-indexed completed group-like element attached to one is the unit. -/
48@[simp]
49theorem completedGroupAlgebraOfInClass_one
50 (C : ProCGroups.FiniteGroupClass.{v}) :
51 completedGroupAlgebraOfInClass C R G 1 =
52 (1 : CompletedGroupAlgebraInClass C R G) := by
53 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
54 intro U
55 rw [completedGroupAlgebraProjectionInClass_of]
56 change MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U 1)
57 (1 : R) =
58 completedGroupAlgebraProjectionInClass C R G U
59 (1 : CompletedGroupAlgebraInClass C R G)
60 rw [map_one]
61 change MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U 1)
62 (1 : R) = 1
63 rfl
65/-- Class-indexed completed group-like elements multiply according to the group law. -/
66@[simp 900]
67theorem completedGroupAlgebraOfInClass_mul
68 (C : ProCGroups.FiniteGroupClass.{v})
69 (g h : G) :
70 completedGroupAlgebraOfInClass C R G (g * h) =
71 completedGroupAlgebraOfInClass C R G g *
72 completedGroupAlgebraOfInClass C R G h := by
73 change toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G (g * h)) =
74 toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g) *
75 toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G h)
76 rw [map_mul (MonoidAlgebra.of R G) g h]
77 have happ (x : MonoidAlgebra R G) :
78 toCompletedGroupAlgebraInClassRingHom C R G x =
79 toCompletedGroupAlgebraInClass C R G x := rfl
80 have hmul := map_mul (toCompletedGroupAlgebraInClassRingHom C R G)
81 (MonoidAlgebra.of R G g) (MonoidAlgebra.of R G h)
82 rw [happ, happ, happ] at hmul
83 exact hmul
85/-- The class-indexed finite-stage group-like map is continuous. -/
86theorem continuous_completedGroupAlgebraStageMapInClass_of
87 (C : ProCGroups.FiniteGroupClass.{v})
88 (U : CompletedGroupAlgebraIndexInClass G C) :
89 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
90 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
91 Continuous fun g : G => completedGroupAlgebraStageMapInClass C R G U
92 (MonoidAlgebra.of R G g) := by
93 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
94 finite_completedGroupAlgebraQuotientInClass G C U
95 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
96 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
97 letI : DiscreteTopology (CompletedGroupAlgebraQuotientInClass G C U) :=
98 QuotientGroup.discreteTopology
99 (ProCGroups.openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 :
100 OpenNormalSubgroup G))
101 have hbasis :
102 @Continuous (CompletedGroupAlgebraQuotientInClass G C U)
103 (CompletedGroupAlgebraStageInClass C R G U) inferInstance
104 ((completedGroupAlgebraSystemInClass C R G).topologicalSpace U)
105 (fun q => MonoidAlgebra.single q (1 : R)) :=
106 continuous_of_discreteTopology
107 have hproj :
108 Continuous fun g : G => openNormalSubgroupInClassProj (C := C) (G := G) U g := by
109 change Continuous
110 (QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
111 exact continuous_quotient_mk'
112 have hcont := hbasis.comp hproj
113 change @Continuous G (CompletedGroupAlgebraStageInClass C R G U) (‹TopologicalSpace G›)
114 ((completedGroupAlgebraSystemInClass C R G).topologicalSpace U)
115 (fun g => MonoidAlgebra.single
116 (openNormalSubgroupInClassProj (C := C) (G := G) U g) (1 : R)) at hcont
117 convert hcont using 1
118 funext g
119 exact completedGroupAlgebraStageMapInClass_of (R := R) (G := G) C U g
121/-- The class-indexed completed group-like map is continuous. -/
122theorem continuous_completedGroupAlgebraOfInClass
123 (C : ProCGroups.FiniteGroupClass.{v}) :
124 Continuous (completedGroupAlgebraOfInClass C R G) := by
125 let S := completedGroupAlgebraSystemInClass C R G
126 letI : ∀ U, TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
127 fun U => (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
128 let π : ∀ U : CompletedGroupAlgebraIndexInClass G C,
129 G → CompletedGroupAlgebraStageInClass C R G U :=
130 fun U g =>
131 completedGroupAlgebraStageMapInClass C R G U
132 (MonoidAlgebra.of R G g)
133 have hπ : ∀ U, Continuous (π U) := by
134 intro U
135 exact continuous_completedGroupAlgebraStageMapInClass_of
136 (R := R) (G := G) C U
137 have hcompat : S.CompatibleMaps π := by
138 intro U V hUV
139 funext g
140 exact congrFun
141 (congrArg DFunLike.coe
142 (completedGroupAlgebraStageMapInClass_compatible
143 (R := R) (G := G) C hUV))
144 (MonoidAlgebra.of R G g)
145 change Continuous (S.inverseLimitLift π hcompat)
146 exact S.continuous_inverseLimitLift π hπ hcompat
148end
150end CompletedGroupAlgebra