Source: ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Topology
1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Projections
3/-!
4# Completed Group Algebra / Basic / All Finite / Topology
6This module transports the finite-stage topological ring and scalar-action structures through the
7single all-finite inverse limit, and records its compactness and separation properties.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
19open ProCGroups.Completion
21universe u v
23variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
26local instance (U : CompletedGroupAlgebraIndex G) :
27 Ring ((completedGroupAlgebraSystem R G).X U) := by
28 change Ring (CompletedGroupAlgebraStage R G U)
29 infer_instance
31local instance (U : CompletedGroupAlgebraIndex G) :
32 Module R ((completedGroupAlgebraSystem R G).X U) := by
33 change Module R (CompletedGroupAlgebraStage R G U)
34 infer_instance
36/-- Each finite stage \(R[G/U]\) is a topological ring for its product topology. -/
37theorem completedGroupAlgebraStage_isTopologicalRing (U : CompletedGroupAlgebraIndex G) :
38 IsTopologicalRing ((completedGroupAlgebraSystem R G).X U) := by
39 dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
40 exact finiteGroupAlgebra_isTopologicalRing R (CompletedGroupAlgebraQuotient G U)
42/-- Each stage of the all-finite system has its finite product topological-ring structure. -/
43instance instIsTopologicalRingCompletedGroupAlgebraSystemX
44 (U : CompletedGroupAlgebraIndex G) :
45 IsTopologicalRing ((completedGroupAlgebraSystem R G).X U) :=
46 completedGroupAlgebraStage_isTopologicalRing (R := R) (G := G) U
48/-- Scalar multiplication is continuous because it is continuous at every finite stage. -/
49instance instContinuousSMulCompletedGroupAlgebra :
50 ContinuousSMul R (CompletedGroupAlgebraCarrier R G) := by
51 letI : ∀ U : CompletedGroupAlgebraIndex G,
52 ContinuousSMul R ((completedGroupAlgebraSystem R G).X U) := fun U => by
53 dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
54 exact finiteGroupAlgebra_continuousSMul R (CompletedGroupAlgebraQuotient G U)
55 exact inferInstanceAs
56 (ContinuousSMul R (completedGroupAlgebraSystem R G).inverseLimit)
58/-- The completed group algebra inherits its topological-ring structure from the generic
59ring-valued inverse limit. -/
60instance instIsTopologicalRingCompletedGroupAlgebra :
61 IsTopologicalRing (CompletedGroupAlgebraCarrier R G) := by
62 exact inferInstanceAs
63 (IsTopologicalRing (completedGroupAlgebraSystem R G).inverseLimit)
65/-- The completed group algebra is compact for compact Hausdorff coefficients. -/
66theorem completedGroupAlgebra_compactSpace [CompactSpace R] [T2Space R] :
67 CompactSpace (CompletedGroupAlgebraCarrier R G) := by
68 letI : ∀ U : CompletedGroupAlgebraIndex G,
69 CompactSpace ((completedGroupAlgebraSystem R G).X U) := fun U =>
70 by
71 dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
72 exact finiteGroupAlgebra_compactSpace R (CompletedGroupAlgebraQuotient G U)
73 letI : ∀ U : CompletedGroupAlgebraIndex G,
74 T2Space ((completedGroupAlgebraSystem R G).X U) := fun U =>
75 by
76 dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
77 exact finiteGroupAlgebra_t2Space R (CompletedGroupAlgebraQuotient G U)
78 change CompactSpace (completedGroupAlgebraSystem R G).inverseLimit
79 infer_instance
81/-- The completed group algebra is Hausdorff for Hausdorff coefficients. -/
82theorem completedGroupAlgebra_t2Space [T2Space R] :
83 T2Space (CompletedGroupAlgebraCarrier R G) := by
84 letI : ∀ U : CompletedGroupAlgebraIndex G,
85 T2Space ((completedGroupAlgebraSystem R G).X U) := fun U =>
86 by
87 dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
88 exact finiteGroupAlgebra_t2Space R (CompletedGroupAlgebraQuotient G U)
89 exact (completedGroupAlgebraSystem R G).t2Space_inverseLimit
91/-- The completed group algebra is totally disconnected for totally disconnected coefficients. -/
92theorem completedGroupAlgebra_totallyDisconnectedSpace [TotallyDisconnectedSpace R] :
93 TotallyDisconnectedSpace (CompletedGroupAlgebraCarrier R G) := by
94 letI : ∀ U : CompletedGroupAlgebraIndex G,
95 TotallyDisconnectedSpace ((completedGroupAlgebraSystem R G).X U) := fun U =>
96 by
97 dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
98 exact finiteGroupAlgebra_totallyDisconnectedSpace R
99 (CompletedGroupAlgebraQuotient G U)
100 exact (completedGroupAlgebraSystem R G).totallyDisconnectedSpace_inverseLimit
102end
104end CompletedGroupAlgebra