Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Topology
1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.System
3/-!
4# Completed Group Algebra / Open Finite Quotient Topology / Open Finite Limit / Topology
6This module transports the discrete topological-ring structures of the open-finite quotient stages
7through the single two-parameter inverse limit, and records compactness and separation results.
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]
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
27 Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
28 change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
29 infer_instance
31/-- Each two-parameter finite quotient stage is a topological ring for its discrete topology. -/
32theorem completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing
33 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
34 [TopologicalSpace G] [IsTopologicalGroup G]
35 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
36 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
37 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
38 IsTopologicalRing (CompletedGroupAlgebraOpenQuotientStage R G K) := by
39 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
40 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
41 haveI : DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G K) :=
42 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
43 infer_instance
45/-- Each open-finite quotient stage is finite for compact topological coefficients. -/
46theorem completedGroupAlgebraOpenFiniteQuotientStage_fintype
47 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
48 [TopologicalSpace G] [IsTopologicalGroup G] [IsTopologicalRing R] [CompactSpace R]
49 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
50 Nonempty (Fintype (CompletedGroupAlgebraOpenQuotientStage R G K)) := by
51 classical
52 let I : Ideal R := (OrderDual.ofDual K.1).1
53 have hIopen : IsOpen (I : Set R) := (OrderDual.ofDual K.1).2
54 rcases finite_quotient_of_openIdeal R I hIopen with ⟨hIfin⟩
55 letI : Fintype (R ⧸ I) := hIfin
56 letI : Fintype (CompletedGroupAlgebraQuotient G K.2) :=
57 Fintype.ofFinite (CompletedGroupAlgebraQuotient G K.2)
58 exact ⟨Fintype.ofEquiv
59 (CompletedGroupAlgebraQuotient G K.2 → R ⧸ I)
60 (Finsupp.equivFunOnFinite.symm.trans
61 (MonoidAlgebra.coeffEquiv
62 (R := R ⧸ I) (M := CompletedGroupAlgebraQuotient G K.2)).symm)⟩
64/-- Each open-finite quotient stage has its discrete topological-ring structure. -/
65instance instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientSystemX
66 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
67 IsTopologicalRing
68 ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
69 completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing
70 (R := R) (G := G) K
72/-- The open-finite quotient limit inherits its topological-ring structure from the generic
73ring-valued inverse limit. -/
74instance instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit :
75 IsTopologicalRing (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
76 exact inferInstanceAs
77 (IsTopologicalRing
78 (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit)
80/-- The open-finite quotient limit is compact for compact topological coefficients. -/
81theorem completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace
82 [IsTopologicalRing R] [CompactSpace R] :
83 CompactSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
84 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
85 CompactSpace ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K => by
86 letI : Fintype ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
87 Classical.choice (completedGroupAlgebraOpenFiniteQuotientStage_fintype R G K)
88 letI : DiscreteTopology ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
89 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
90 infer_instance
91 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
92 T2Space ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K => by
93 letI : DiscreteTopology ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
94 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
95 infer_instance
96 change CompactSpace
97 (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit
98 infer_instance
100/-- The open-finite quotient limit is Hausdorff. -/
101theorem completedGroupAlgebraOpenFiniteQuotientLimit_t2Space :
102 T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
103 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
104 T2Space ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K => by
105 letI : DiscreteTopology ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
106 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
107 infer_instance
108 exact (completedGroupAlgebraOpenFiniteQuotientSystem R G).t2Space_inverseLimit
110/-- The open-finite quotient limit is totally disconnected. -/
111theorem completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace :
112 TotallyDisconnectedSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
113 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
114 TotallyDisconnectedSpace ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>
115 by
116 letI : DiscreteTopology ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
117 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
118 infer_instance
119 exact (completedGroupAlgebraOpenFiniteQuotientSystem R G).totallyDisconnectedSpace_inverseLimit
121end
123end CompletedGroupAlgebra