Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.System
1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients
3/-!
4# Completed Group Algebra / Open Finite Quotient Topology / Open Finite Limit / System
6This module defines the two-parameter open-finite quotient system and its named inverse-limit
7carrier. The compatible-family representation is exposed only by an explicit equivalence and the
8canonical projection/compatibility/extensionality API.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v
24variable (R : Type u) [CommRing R] [TopologicalSpace R]
25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27/--
28The two-parameter inverse system \(K = (I, U) \mapsto (R/I)[G/U]\) for the kernel-neighborhood
29topology.
30-/
31def completedGroupAlgebraOpenFiniteQuotientSystem
32 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
33 [TopologicalSpace G] [IsTopologicalGroup G] :
35 (I := CompletedGroupAlgebraOpenQuotientIndex R G) where
36 X := CompletedGroupAlgebraOpenQuotientStage R G
37 topologicalSpace := completedGroupAlgebraOpenFiniteQuotientStageTopology R G
38 map := fun {K L} hKL => completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
39 continuous_map := by
40 intro K L hKL
41 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
42 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
43 letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G L) :=
44 completedGroupAlgebraOpenFiniteQuotientStageTopology R G L
45 haveI : DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G L) :=
46 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G L
47 exact continuous_of_discreteTopology
48 map_id := by
49 intro K
50 exact congrArg DFunLike.coe
51 (completedGroupAlgebraOpenFiniteQuotientTransition_id R G K)
52 map_comp := by
53 intro K L M hKL hLM
54 exact congrArg DFunLike.coe
55 (completedGroupAlgebraOpenFiniteQuotientTransition_comp R G hKL hLM)
57/-- The two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\), kept opaque from
58its concrete compatible-family realization. -/
59def CompletedGroupAlgebraOpenFiniteQuotientLimit
60 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
61 [TopologicalSpace G] [IsTopologicalGroup G] :
62 Type (max u v) :=
63 (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit
65/-- The two-parameter completion carries its inverse-limit topology. -/
66instance instTopologicalSpaceCompletedGroupAlgebraOpenFiniteQuotientLimit :
67 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
68 inferInstanceAs
69 (TopologicalSpace
70 (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit)
72/-- Explicit exchange between the named two-parameter carrier and its compatible-family model. -/
73def completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv :
74 CompletedGroupAlgebraOpenFiniteQuotientLimit R G ≃
75 (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit :=
76 Equiv.refl _
78local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
79 Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
80 change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
81 infer_instance
83/-- The open-finite quotient tower is a ring-valued inverse system. -/
84instance instIsRingSystemCompletedGroupAlgebraOpenFiniteQuotientSystem :
85 IsRingSystem (completedGroupAlgebraOpenFiniteQuotientSystem R G) where
86 map_zero := by
87 intro K L hKL
88 exact map_zero (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)
89 map_one := by
90 intro K L hKL
91 exact map_one (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)
92 map_add := by
93 intro K L hKL x y
94 exact map_add (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) x y
95 map_mul := by
96 intro K L hKL x y
97 exact map_mul (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) x y
99/-- The two-parameter completion inherits its ring structure from the generic inverse limit. -/
100instance instRingCompletedGroupAlgebraOpenFiniteQuotientLimit :
101 Ring (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
102 inferInstanceAs
103 (Ring (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit)
105/-- The canonical projection to one quotient \((R/I)[G/U]\), bundled at its source as a ring
106homomorphism. -/
107def completedGroupAlgebraOpenFiniteQuotientLimitProjection
108 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
109 [TopologicalSpace G] [IsTopologicalGroup G]
110 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
111 CompletedGroupAlgebraOpenFiniteQuotientLimit R G →+*
112 CompletedGroupAlgebraOpenQuotientStage R G K := by
113 change (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit →+*
114 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K
115 exact projectionRingHom
116 (S := completedGroupAlgebraOpenFiniteQuotientSystem R G) K
118/-- The open-finite quotient projections satisfy the two-parameter transition equations. -/
119theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_compatible
120 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L)
121 (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
122 completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
123 (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G L x) =
124 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x := by
125 change (completedGroupAlgebraOpenFiniteQuotientSystem R G).map hKL
126 ((completedGroupAlgebraOpenFiniteQuotientSystem R G).projection L x) =
127 (completedGroupAlgebraOpenFiniteQuotientSystem R G).projection K x
128 exact (completedGroupAlgebraOpenFiniteQuotientSystem R G).projection_compatible
129 x K L hKL
131/-- Two open-finite quotient completed elements are equal when all bundled coordinates agree. -/
132@[ext]
133theorem completedGroupAlgebraOpenFiniteQuotientLimit_ext
134 {x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G}
135 (h : ∀ K, completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x =
136 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K y) :
137 x = y := by
138 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
139 intro K
140 exact h K
142end
144end CompletedGroupAlgebra