Source: ProCGroups.InverseSystems.StagewiseIso
1import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
2import ProCGroups.Topologies.ContinuousMulEquiv
4/-!
5# Stagewise isomorphisms and inverse-limit equivalences
7A compatible family of continuous group isomorphisms defines morphisms in both directions
8between two inverse systems. The induced maps on their inverse limits are assembled into a
9canonical continuous multiplicative equivalence.
10-/
12open scoped Topology
14namespace ProCGroups
15namespace InverseSystems
17universe u v
19namespace InverseSystem
21variable {I : Type u} [Preorder I]
22variable (S T : InverseSystem.{u, v} (I := I))
23variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
24variable [IsGroupSystem S] [IsGroupSystem T]
25variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
27/--
28A compatible family of stagewise continuous group isomorphisms between two concrete inverse
29systems.
30-/
31structure InverseSystemIso where
32 /-- A continuous group isomorphism between the source and target objects at each index. -/
33 stageEquiv : ∀ i, S.X i ≃ₜ* T.X i
34 /-- The stagewise isomorphisms intertwine the transition maps of the two systems. -/
35 comm : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
36 stageEquiv i (S.map hij x) = T.map hij (stageEquiv j x)
38namespace InverseSystemIso
40variable {S T}
42/-- A stagewise isomorphism determines the forward morphism of inverse systems. -/
43def toMorphism (E : InverseSystemIso S T) : S.Morphism T where
44 map i := E.stageEquiv i
45 continuous_map i := (E.stageEquiv i).continuous_toFun
46 comm := by
47 intro i j hij
48 funext x
49 exact (E.comm hij x).symm
51/-- A stagewise isomorphism determines the inverse morphism of inverse systems. -/
52def invMorphism (E : InverseSystemIso S T) : T.Morphism S where
53 map i := (E.stageEquiv i).symm
54 continuous_map i := (E.stageEquiv i).continuous_invFun
55 comm := by
56 intro i j hij
57 funext x
58 apply (E.stageEquiv i).injective
59 simpa using E.comm hij ((E.stageEquiv j).symm x)
61/-- The forward continuous homomorphism on inverse limits induced by a stagewise isomorphism. -/
62noncomputable def toContinuousMonoidHom (E : InverseSystemIso S T) :
63 S.inverseLimit →ₜ* T.inverseLimit where
64 toMonoidHom :=
65 { toFun := S.limMap E.toMorphism
66 map_one' := by
67 apply T.ext
68 intro i
69 change T.projection i (S.limMap E.toMorphism 1) = T.projection i 1
70 rw [S.π_limMap_apply (Θ := E.toMorphism)]
71 change (E.stageEquiv i) (1 : S.X i) = (1 : T.X i)
72 exact (E.stageEquiv i).toMulEquiv.map_one
73 map_mul' := by
74 intro x y
75 apply T.ext
76 intro i
77 change T.projection i (S.limMap E.toMorphism (x * y)) =
78 T.projection i (S.limMap E.toMorphism x * S.limMap E.toMorphism y)
79 rw [S.π_limMap_apply (Θ := E.toMorphism)]
80 rw [projection_mul (S := T), S.π_limMap_apply (Θ := E.toMorphism),
81 S.π_limMap_apply (Θ := E.toMorphism)]
82 change (E.stageEquiv i) (S.projection i x * S.projection i y) =
83 (E.stageEquiv i) (S.projection i x) * (E.stageEquiv i) (S.projection i y)
84 exact (E.stageEquiv i).toMulEquiv.map_mul (S.projection i x) (S.projection i y) }
85 continuous_toFun := S.continuous_limMap E.toMorphism
87/-- The inverse continuous homomorphism on inverse limits induced by a stagewise isomorphism. -/
88noncomputable def invContinuousMonoidHom (E : InverseSystemIso S T) :
89 T.inverseLimit →ₜ* S.inverseLimit where
90 toMonoidHom :=
91 { toFun := T.limMap E.invMorphism
92 map_one' := by
93 apply S.ext
94 intro i
95 change S.projection i (T.limMap E.invMorphism 1) = S.projection i 1
96 rw [T.π_limMap_apply (Θ := E.invMorphism)]
97 change (E.stageEquiv i).symm (1 : T.X i) = (1 : S.X i)
98 exact (E.stageEquiv i).symm.toMulEquiv.map_one
99 map_mul' := by
100 intro x y
101 apply S.ext
102 intro i
103 change S.projection i (T.limMap E.invMorphism (x * y)) =
104 S.projection i (T.limMap E.invMorphism x * T.limMap E.invMorphism y)
105 rw [T.π_limMap_apply (Θ := E.invMorphism)]
106 rw [projection_mul (S := S), T.π_limMap_apply (Θ := E.invMorphism),
107 T.π_limMap_apply (Θ := E.invMorphism)]
108 change (E.stageEquiv i).symm (T.projection i x * T.projection i y) =
109 (E.stageEquiv i).symm (T.projection i x) * (E.stageEquiv i).symm (T.projection i y)
110 exact (E.stageEquiv i).symm.toMulEquiv.map_mul (T.projection i x) (T.projection i y) }
111 continuous_toFun := T.continuous_limMap E.invMorphism
113/--
114Compatible stagewise continuous group isomorphisms induce a continuous multiplicative
115equivalence on concrete inverse limits.
116-/
117noncomputable def inverseLimitContinuousMulEquiv (E : InverseSystemIso S T) :
118 S.inverseLimit ≃ₜ* T.inverseLimit :=
119 ContinuousMulEquiv.ofHomInv
120 E.toContinuousMonoidHom
121 E.invContinuousMonoidHom
122 (by
123 intro x
124 apply S.ext
125 intro i
126 change S.projection i
127 (T.limMap E.invMorphism (S.limMap E.toMorphism x)) = S.projection i x
128 rw [T.π_limMap_apply (Θ := E.invMorphism),
129 S.π_limMap_apply (Θ := E.toMorphism)]
130 simp only [invMorphism, toMorphism, projection_apply, ContinuousMulEquiv.symm_apply_apply])
131 (by
132 intro x
133 apply T.ext
134 intro i
135 change T.projection i
136 (S.limMap E.toMorphism (T.limMap E.invMorphism x)) = T.projection i x
137 rw [S.π_limMap_apply (Θ := E.toMorphism),
138 T.π_limMap_apply (Θ := E.invMorphism)]
139 simp only [toMorphism, invMorphism, projection_apply, ContinuousMulEquiv.apply_symm_apply])
141omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)] in
142/--
143The projection inverse limit continuous multiplicative equivalence is compatible with the
144profinite topology and gives the continuous map or equivalence determined by the finite-quotient
145data.
146-/
147@[simp] theorem projection_inverseLimitContinuousMulEquiv
148 (E : InverseSystemIso S T) (i : I) (x : S.inverseLimit) :
149 T.projection i (E.inverseLimitContinuousMulEquiv x) =
150 E.stageEquiv i (S.projection i x) := by
151 change T.projection i (S.limMap E.toMorphism x) =
152 E.stageEquiv i (S.projection i x)
153 exact S.π_limMap_apply E.toMorphism i x
155omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)] in
156/--
157The inverse of the projection-induced inverse-limit continuous multiplicative equivalence is
158compatible with the profinite topology and gives the continuous map or equivalence determined by
159the finite-quotient data.
160-/
161@[simp] theorem projection_inverseLimitContinuousMulEquiv_symm
162 (E : InverseSystemIso S T) (i : I) (x : T.inverseLimit) :
163 S.projection i (E.inverseLimitContinuousMulEquiv.symm x) =
164 (E.stageEquiv i).symm (T.projection i x) := by
165 change S.projection i (T.limMap E.invMorphism x) =
166 (E.stageEquiv i).symm (T.projection i x)
167 exact T.π_limMap_apply E.invMorphism i x
169end InverseSystemIso
171end InverseSystem
173end InverseSystems
174end ProCGroups