Source: ProCGroups.CompletedGroupAlgebra.Basic.InClass.System
1import ProCGroups.CompletedGroupAlgebra.Basic.InClass.Stage
3/-!
4# Completed Group Algebra / Basic / Within a Class / System
6This module assembles the \(C\)-indexed stages into a topological inverse system and supplies the
7single `IsRingSystem` witness from which the completed carrier inherits its ring structure.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
20universe u v w
22variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
23variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
26/--
27The \(C\)-indexed inverse system \(U\mapsto R[G/U]\). The hypothesis says that \(C\) really is a
28finite quotient class, so every stage carries the finite-product topology.
29-/
30def completedGroupAlgebraSystemInClass
31 (C : ProCGroups.FiniteGroupClass.{v})
32 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
34 ProCGroups.InverseSystems.InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
35 X := CompletedGroupAlgebraStageInClass C R G
36 topologicalSpace := fun U => by
37 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
38 finite_completedGroupAlgebraQuotientInClass G C U
39 exact finiteGroupAlgebraTopology R (CompletedGroupAlgebraQuotientInClass G C U)
40 map := fun {U V} hUV => completedGroupAlgebraTransitionInClass C R G hUV
41 continuous_map := by
42 intro U V hUV
43 letI : Finite (CompletedGroupAlgebraQuotientInClass G C V) :=
44 finite_completedGroupAlgebraQuotientInClass G C V
45 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
46 finite_completedGroupAlgebraQuotientInClass G C U
47 exact finiteGroupAlgebra_mapDomainRingHom_continuous R
48 (CompletedGroupAlgebraQuotientInClass G C V) (CompletedGroupAlgebraQuotientInClass G C U)
49 (OpenNormalSubgroupInClass.map
50 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
51 map_id := by
52 intro U
53 funext x
54 exact congrFun
55 (congrArg DFunLike.coe
56 (completedGroupAlgebraTransitionInClass_id (R := R) (G := G) C U)) x
57 map_comp := by
58 intro U V W hUV hVW
59 funext x
60 exact congrFun
61 (congrArg DFunLike.coe
62 (completedGroupAlgebraTransitionInClass_comp (R := R) (G := G) C hUV hVW)) x
64local instance
65 (C : ProCGroups.FiniteGroupClass.{v})
66 (U : CompletedGroupAlgebraIndexInClass G C) :
67 Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
68 change Ring (CompletedGroupAlgebraStageInClass C R G U)
69 infer_instance
71/--
72The inverse system of finite-stage group algebras inherits a ring structure from the compatible
73finite-stage rings.
74-/
75instance instIsRingSystemCompletedGroupAlgebraSystemInClass
76 (C : ProCGroups.FiniteGroupClass.{v}) :
77 IsRingSystem (completedGroupAlgebraSystemInClass C R G) where
78 map_zero := by
79 intro U V hUV
80 exact map_zero (completedGroupAlgebraTransitionInClass C R G hUV)
81 map_one := by
82 intro U V hUV
83 exact map_one (completedGroupAlgebraTransitionInClass C R G hUV)
84 map_add := by
85 intro U V hUV x y
86 exact map_add (completedGroupAlgebraTransitionInClass C R G hUV) x y
87 map_mul := by
88 intro U V hUV x y
89 exact map_mul (completedGroupAlgebraTransitionInClass C R G hUV) x y
92end
94end CompletedGroupAlgebra