Yamaguchi Lean 4 Library
ProCGroups/InverseSystems/StagewiseIso.lean
ProCGroups/InverseSystems/StagewiseIso/Source

ProCGroups/InverseSystems/StagewiseIso.lean

1import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
2import ProCGroups.Topologies.ContinuousMulEquiv
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/InverseSystems/StagewiseIso.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Stagewise isomorphisms of inverse systems
15This file packages compatible stagewise continuous group isomorphisms and the
16induced continuous multiplicative equivalence on concrete inverse limits.
17-/
19open scoped Topology
21namespace ProCGroups
22namespace InverseSystems
24universe u v
26namespace InverseSystem
28variable {I : Type u} [Preorder I]
29variable (S T : InverseSystem.{u, v} (I := I))
30variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
32variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
34/-- A compatible stagewise continuous group isomorphism between two concrete
35inverse systems. -/
36structure InverseSystemIso where
37 stageEquiv : ∀ i, S.X i ≃ₜ* T.X i
38 comm : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
39 stageEquiv i (S.map hij x) = T.map hij (stageEquiv j x)
43variable {S T}
45/-- The forward morphism of inverse systems associated to a stagewise
46isomorphism. -/
47def toMorphism (E : InverseSystemIso S T) : S.Morphism T where
48 map i := E.stageEquiv i
49 continuous_map i := (E.stageEquiv i).continuous_toFun
50 comm := by
51 intro i j hij
52 funext x
53 exact (E.comm hij x).symm
55/-- The inverse morphism of inverse systems associated to a stagewise
56isomorphism. -/
57def invMorphism (E : InverseSystemIso S T) : T.Morphism S where
58 map i := (E.stageEquiv i).symm
59 continuous_map i := (E.stageEquiv i).continuous_invFun
60 comm := by
61 intro i j hij
62 funext x
63 apply (E.stageEquiv i).injective
64 simpa using E.comm hij ((E.stageEquiv j).symm x)
66/-- The forward continuous homomorphism on inverse limits induced by a
67stagewise isomorphism. -/
68noncomputable def toContinuousMonoidHom (E : InverseSystemIso S T) :
69 S.inverseLimit →ₜ* T.inverseLimit where
70 toMonoidHom :=
71 { toFun := S.limMap E.toMorphism
72 map_one' := by
73 apply T.ext
74 intro i
75 change T.projection i (S.limMap E.toMorphism 1) = T.projection i 1
76 rw [S.π_limMap_apply (Θ := E.toMorphism)]
77 change (E.stageEquiv i) (1 : S.X i) = (1 : T.X i)
78 exact (E.stageEquiv i).toMulEquiv.map_one
79 map_mul' := by
80 intro x y
81 apply T.ext
82 intro i
83 change T.projection i (S.limMap E.toMorphism (x * y)) =
84 T.projection i (S.limMap E.toMorphism x * S.limMap E.toMorphism y)
85 rw [S.π_limMap_apply (Θ := E.toMorphism)]
86 rw [projection_mul (S := T), S.π_limMap_apply (Θ := E.toMorphism),
87 S.π_limMap_apply (Θ := E.toMorphism)]
88 change (E.stageEquiv i) (S.projection i x * S.projection i y) =
89 (E.stageEquiv i) (S.projection i x) * (E.stageEquiv i) (S.projection i y)
90 exact (E.stageEquiv i).toMulEquiv.map_mul (S.projection i x) (S.projection i y) }
91 continuous_toFun := S.continuous_limMap E.toMorphism
93/-- The inverse continuous homomorphism on inverse limits induced by a
94stagewise isomorphism. -/
95noncomputable def invContinuousMonoidHom (E : InverseSystemIso S T) :
96 T.inverseLimit →ₜ* S.inverseLimit where
97 toMonoidHom :=
98 { toFun := T.limMap E.invMorphism
99 map_one' := by
100 apply S.ext
101 intro i
102 change S.projection i (T.limMap E.invMorphism 1) = S.projection i 1
103 rw [T.π_limMap_apply (Θ := E.invMorphism)]
104 change (E.stageEquiv i).symm (1 : T.X i) = (1 : S.X i)
105 exact (E.stageEquiv i).symm.toMulEquiv.map_one
106 map_mul' := by
107 intro x y
108 apply S.ext
109 intro i
110 change S.projection i (T.limMap E.invMorphism (x * y)) =
111 S.projection i (T.limMap E.invMorphism x * T.limMap E.invMorphism y)
112 rw [T.π_limMap_apply (Θ := E.invMorphism)]
113 rw [projection_mul (S := S), T.π_limMap_apply (Θ := E.invMorphism),
114 T.π_limMap_apply (Θ := E.invMorphism)]
115 change (E.stageEquiv i).symm (T.projection i x * T.projection i y) =
116 (E.stageEquiv i).symm (T.projection i x) * (E.stageEquiv i).symm (T.projection i y)
117 exact (E.stageEquiv i).symm.toMulEquiv.map_mul (T.projection i x) (T.projection i y) }
118 continuous_toFun := T.continuous_limMap E.invMorphism
120/-- Compatible stagewise continuous group isomorphisms induce a continuous
121multiplicative equivalence on concrete inverse limits. -/
123 S.inverseLimit ≃ₜ* T.inverseLimit :=
125 E.toContinuousMonoidHom
126 E.invContinuousMonoidHom
127 (by
128 intro x
129 apply S.ext
130 intro i
131 change S.projection i
132 (T.limMap E.invMorphism (S.limMap E.toMorphism x)) = S.projection i x
133 rw [T.π_limMap_apply (Θ := E.invMorphism),
134 S.π_limMap_apply (Θ := E.toMorphism)]
135 simp only [invMorphism, toMorphism, projection_apply, ContinuousMulEquiv.symm_apply_apply])
136 (by
137 intro x
138 apply T.ext
139 intro i
140 change T.projection i
141 (S.limMap E.toMorphism (T.limMap E.invMorphism x)) = T.projection i x
142 rw [S.π_limMap_apply (Θ := E.toMorphism),
143 T.π_limMap_apply (Θ := E.invMorphism)]
144 simp only [toMorphism, invMorphism, projection_apply, ContinuousMulEquiv.apply_symm_apply])
146omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)] in
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
157 (E : InverseSystemIso S T) (i : I) (x : T.inverseLimit) :
158 S.projection i (E.inverseLimitContinuousMulEquiv.symm x) =
159 (E.stageEquiv i).symm (T.projection i x) := by
160 change S.projection i (T.limMap E.invMorphism x) =
161 (E.stageEquiv i).symm (T.projection i x)
162 exact T.π_limMap_apply E.invMorphism i x
168end InverseSystems
169end ProCGroups