Skip to content

Commit 306e54f

Browse files
ocfnashocfnash
committed
feat: port Topology.Algebra.GroupCompletion (#2637)
1 parent cf97ef3 commit 306e54f

File tree

3 files changed

+315
-3
lines changed

3 files changed

+315
-3
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1246,6 +1246,7 @@ import Mathlib.Topology.Algebra.Constructions
12461246
import Mathlib.Topology.Algebra.Field
12471247
import Mathlib.Topology.Algebra.Group.Basic
12481248
import Mathlib.Topology.Algebra.Group.Compact
1249+
import Mathlib.Topology.Algebra.GroupCompletion
12491250
import Mathlib.Topology.Algebra.GroupWithZero
12501251
import Mathlib.Topology.Algebra.InfiniteSum.Basic
12511252
import Mathlib.Topology.Algebra.InfiniteSum.Order

‎Mathlib/Topology/Algebra/GroupCompletion.lean‎

Lines changed: 306 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,306 @@
1+
/-
2+
Copyright (c) 2018 Patrick Massot. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Patrick Massot, Johannes Hölzl
5+
6+
! This file was ported from Lean 3 source module topology.algebra.group_completion
7+
! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Topology.Algebra.UniformGroup
12+
import Mathlib.Topology.Algebra.UniformMulAction
13+
import Mathlib.Topology.UniformSpace.Completion
14+
15+
/-!
16+
# Completion of topological groups:
17+
18+
This files endows the completion of a topological abelian group with a group structure.
19+
More precisely the instance `UniformSpace.Completion.instAddGroup` builds an abelian group structure
20+
on the completion of an abelian group endowed with a compatible uniform structure.
21+
Then the instance `UniformSpace.Completion.instUniformAddGroup` proves this group structure is
22+
compatible with the completed uniform structure. The compatibility condition is `UniformAddGroup`.
23+
24+
## Main declarations:
25+
26+
Beyond the instances explained above (that don't have to be explicitly invoked),
27+
the main constructions deal with continuous group morphisms.
28+
29+
* `AddMonoidHom.extension`: extends a continuous group morphism from `G`
30+
to a complete separated group `H` to `Completion G`.
31+
* `AddMonoidHom.completion`: promotes a continuous group morphism
32+
from `G` to `H` into a continuous group morphism
33+
from `Completion G` to `Completion H`.
34+
-/
35+
36+
37+
noncomputable section
38+
39+
variable {M R α β : Type _}
40+
41+
section Group
42+
43+
open UniformSpace CauchyFilter Filter Set
44+
45+
variable [UniformSpace α]
46+
47+
instance [Zero α] : Zero (Completion α) :=
48+
⟨(0 : α)⟩
49+
50+
instance [Neg α] : Neg (Completion α) :=
51+
⟨Completion.map (fun a ↦ -a : α → α)⟩
52+
53+
instance [Add α] : Add (Completion α) :=
54+
⟨Completion.map₂ (· + ·)⟩
55+
56+
instance [Sub α] : Sub (Completion α) :=
57+
⟨Completion.map₂ Sub.sub⟩
58+
59+
@[norm_cast]
60+
theorem UniformSpace.Completion.coe_zero [Zero α] : ((0 : α) : Completion α) = 0 :=
61+
rfl
62+
#align uniform_space.completion.coe_zero UniformSpace.Completion.coe_zero
63+
64+
end Group
65+
66+
namespace UniformSpace.Completion
67+
68+
open UniformSpace
69+
70+
section Zero
71+
72+
instance [UniformSpace α] [MonoidWithZero M] [Zero α] [MulActionWithZero M α]
73+
[UniformContinuousConstSMul M α] : MulActionWithZero M (Completion α) :=
74+
{ (inferInstance : MulAction M $ Completion α) with
75+
smul := (· • ·)
76+
smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
77+
zero_smul :=
78+
ext' (continuous_const_smul _) continuous_const fun a ↦ by
79+
rw [← coe_smul, zero_smul, coe_zero] }
80+
81+
end Zero
82+
83+
section UniformAddGroup
84+
85+
variable [UniformSpace α] [AddGroup α] [UniformAddGroup α]
86+
87+
@[norm_cast]
88+
theorem coe_neg (a : α) : ((-a : α) : Completion α) = -a :=
89+
(map_coe uniformContinuous_neg a).symm
90+
#align uniform_space.completion.coe_neg UniformSpace.Completion.coe_neg
91+
92+
@[norm_cast]
93+
theorem coe_sub (a b : α) : ((a - b : α) : Completion α) = a - b :=
94+
(map₂_coe_coe a b Sub.sub uniformContinuous_sub).symm
95+
#align uniform_space.completion.coe_sub UniformSpace.Completion.coe_sub
96+
97+
@[norm_cast]
98+
theorem coe_add (a b : α) : ((a + b : α) : Completion α) = a + b :=
99+
(map₂_coe_coe a b (· + ·) uniformContinuous_add).symm
100+
#align uniform_space.completion.coe_add UniformSpace.Completion.coe_add
101+
102+
instance : AddMonoid (Completion α) :=
103+
{ (inferInstance : Zero $ Completion α),
104+
(inferInstance : Add $ Completion α) with
105+
zero_add := fun a ↦
106+
Completion.induction_on a
107+
(isClosed_eq (continuous_map₂ continuous_const continuous_id) continuous_id) fun a ↦
108+
show 0 + (a : Completion α) = a by rw [← coe_zero, ← coe_add, zero_add]
109+
add_zero := fun a ↦
110+
Completion.induction_on a
111+
(isClosed_eq (continuous_map₂ continuous_id continuous_const) continuous_id) fun a ↦
112+
show (a : Completion α) + 0 = a by rw [← coe_zero, ← coe_add, add_zero]
113+
add_assoc := fun a b c ↦
114+
Completion.induction_on₃ a b c
115+
(isClosed_eq
116+
(continuous_map₂ (continuous_map₂ continuous_fst (continuous_fst.comp continuous_snd))
117+
(continuous_snd.comp continuous_snd))
118+
(continuous_map₂ continuous_fst
119+
(continuous_map₂ (continuous_fst.comp continuous_snd)
120+
(continuous_snd.comp continuous_snd))))
121+
fun a b c ↦
122+
show (a : Completion α) + b + c = a + (b + c) by repeat' rw_mod_cast [add_assoc]
123+
nsmul := (· • ·)
124+
nsmul_zero := fun a ↦
125+
Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
126+
show 0 • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
127+
nsmul_succ := fun n a ↦
128+
Completion.induction_on a
129+
(isClosed_eq continuous_map <| continuous_map₂ continuous_id continuous_map) fun a ↦
130+
show (n + 1) • (a : Completion α) = (a : Completion α) + n • (a : Completion α) by
131+
rw [← coe_smul, succ_nsmul, coe_add, coe_smul] }
132+
133+
instance : SubNegMonoid (Completion α) :=
134+
{ (inferInstance : AddMonoid $ Completion α),
135+
(inferInstance : Neg $ Completion α),
136+
(inferInstance : Sub $ Completion α) with
137+
sub_eq_add_neg := fun a b ↦
138+
Completion.induction_on₂ a b
139+
(isClosed_eq (continuous_map₂ continuous_fst continuous_snd)
140+
(continuous_map₂ continuous_fst (Completion.continuous_map.comp continuous_snd)))
141+
fun a b ↦ by exact_mod_cast congr_arg ((↑) : α → Completion α) (sub_eq_add_neg a b)
142+
zsmul := (· • ·)
143+
zsmul_zero' := fun a ↦
144+
Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
145+
show (0 : ℤ) • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
146+
zsmul_succ' := fun n a ↦
147+
Completion.induction_on a
148+
(isClosed_eq continuous_map <| continuous_map₂ continuous_id continuous_map) fun a ↦
149+
show Int.ofNat n.succ • (a : Completion α) = _ by
150+
rw [← coe_smul, show Int.ofNat n.succ • a = a + Int.ofNat n • a from
151+
SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
152+
zsmul_neg' := fun n a ↦
153+
Completion.induction_on a
154+
(isClosed_eq continuous_map <| Completion.continuous_map.comp continuous_map) fun a ↦
155+
show (Int.negSucc n) • (a : Completion α) = _ by
156+
rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
157+
SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul] }
158+
159+
instance instAddGroup : AddGroup (Completion α) :=
160+
{ (inferInstance : SubNegMonoid $ Completion α) with
161+
add_left_neg := fun a ↦
162+
Completion.induction_on a
163+
(isClosed_eq (continuous_map₂ Completion.continuous_map continuous_id) continuous_const)
164+
fun a ↦
165+
show -(a : Completion α) + a = 0
166+
by
167+
rw_mod_cast [add_left_neg]
168+
rfl }
169+
170+
instance instUniformAddGroup : UniformAddGroup (Completion α) :=
171+
⟨uniformContinuous_map₂ Sub.sub⟩
172+
173+
instance {M} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] :
174+
DistribMulAction M (Completion α) :=
175+
{ (inferInstance : MulAction M $ Completion α) with
176+
smul := (· • ·)
177+
smul_add := fun r x y ↦
178+
induction_on₂ x y
179+
(isClosed_eq ((continuous_fst.add continuous_snd).const_smul _)
180+
((continuous_fst.const_smul _).add (continuous_snd.const_smul _)))
181+
fun a b ↦ by simp only [← coe_add, ← coe_smul, smul_add]
182+
smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, smul_zero r] }
183+
184+
/-- The map from a group to its completion as a group hom. -/
185+
@[simps]
186+
def toCompl : α →+ Completion α where
187+
toFun := (↑)
188+
map_add' := coe_add
189+
map_zero' := coe_zero
190+
#align uniform_space.completion.to_compl UniformSpace.Completion.toCompl
191+
192+
theorem continuous_toCompl : Continuous (toCompl : α → Completion α) :=
193+
continuous_coe α
194+
#align uniform_space.completion.continuous_to_compl UniformSpace.Completion.continuous_toCompl
195+
196+
variable (α)
197+
198+
theorem denseInducing_toCompl : DenseInducing (toCompl : α → Completion α) :=
199+
denseInducing_coe
200+
#align uniform_space.completion.dense_inducing_to_compl UniformSpace.Completion.denseInducing_toCompl
201+
202+
variable {α}
203+
204+
end UniformAddGroup
205+
206+
section UniformAddCommGroup
207+
208+
variable [UniformSpace α] [AddCommGroup α] [UniformAddGroup α]
209+
210+
instance : AddCommGroup (Completion α) :=
211+
{ (inferInstance : AddGroup $ Completion α) with
212+
add_comm := fun a b ↦
213+
Completion.induction_on₂ a b
214+
(isClosed_eq (continuous_map₂ continuous_fst continuous_snd)
215+
(continuous_map₂ continuous_snd continuous_fst))
216+
fun x y ↦ by
217+
change (x : Completion α) + ↑y = ↑y + ↑x
218+
rw [← coe_add, ← coe_add, add_comm] }
219+
220+
instance [Semiring R] [Module R α] [UniformContinuousConstSMul R α] : Module R (Completion α) :=
221+
{ (inferInstance : DistribMulAction R $ Completion α),
222+
(inferInstance : MulActionWithZero R $ Completion α) with
223+
smul := (· • ·)
224+
add_smul := fun a b ↦
225+
ext' (continuous_const_smul _) ((continuous_const_smul _).add (continuous_const_smul _))
226+
fun x ↦ by
227+
rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul] }
228+
229+
end UniformAddCommGroup
230+
231+
end UniformSpace.Completion
232+
233+
section AddMonoidHom
234+
235+
variable [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β]
236+
[UniformAddGroup β]
237+
238+
open UniformSpace UniformSpace.Completion
239+
240+
/-- Extension to the completion of a continuous group hom. -/
241+
def AddMonoidHom.extension [CompleteSpace β] [SeparatedSpace β] (f : α →+ β) (hf : Continuous f) :
242+
Completion α →+ β :=
243+
have hf : UniformContinuous f := uniformContinuous_addMonoidHom_of_continuous hf
244+
{ toFun := Completion.extension f
245+
map_zero' := by rw [← coe_zero, extension_coe hf, f.map_zero]
246+
map_add' := fun a b ↦
247+
Completion.induction_on₂ a b
248+
(isClosed_eq (continuous_extension.comp continuous_add)
249+
((continuous_extension.comp continuous_fst).add
250+
(continuous_extension.comp continuous_snd)))
251+
fun a b ↦
252+
show Completion.extension f _ = Completion.extension f _ + Completion.extension f _ by
253+
rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add] }
254+
#align add_monoid_hom.extension AddMonoidHom.extension
255+
256+
theorem AddMonoidHom.extension_coe [CompleteSpace β] [SeparatedSpace β] (f : α →+ β)
257+
(hf : Continuous f) (a : α) : f.extension hf a = f a :=
258+
UniformSpace.Completion.extension_coe (uniformContinuous_addMonoidHom_of_continuous hf) a
259+
#align add_monoid_hom.extension_coe AddMonoidHom.extension_coe
260+
261+
@[continuity]
262+
theorem AddMonoidHom.continuous_extension [CompleteSpace β] [SeparatedSpace β] (f : α →+ β)
263+
(hf : Continuous f) : Continuous (f.extension hf) :=
264+
UniformSpace.Completion.continuous_extension
265+
#align add_monoid_hom.continuous_extension AddMonoidHom.continuous_extension
266+
267+
/-- Completion of a continuous group hom, as a group hom. -/
268+
def AddMonoidHom.completion (f : α →+ β) (hf : Continuous f) : Completion α →+ Completion β :=
269+
(toCompl.comp f).extension (continuous_toCompl.comp hf)
270+
#align add_monoid_hom.completion AddMonoidHom.completion
271+
272+
@[continuity]
273+
theorem AddMonoidHom.continuous_completion (f : α →+ β) (hf : Continuous f) :
274+
Continuous (AddMonoidHom.completion f hf : Completion α → Completion β) :=
275+
continuous_map
276+
#align add_monoid_hom.continuous_completion AddMonoidHom.continuous_completion
277+
278+
theorem AddMonoidHom.completion_coe (f : α →+ β) (hf : Continuous f) (a : α) :
279+
AddMonoidHom.completion f hf a = f a :=
280+
map_coe (uniformContinuous_addMonoidHom_of_continuous hf) a
281+
#align add_monoid_hom.completion_coe AddMonoidHom.completion_coe
282+
283+
theorem AddMonoidHom.completion_zero :
284+
AddMonoidHom.completion (0 : α →+ β) continuous_const = 0 := by
285+
ext x
286+
refine Completion.induction_on x ?_ ?_
287+
· apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
288+
simp [continuous_const]
289+
· intro a
290+
simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]
291+
#align add_monoid_hom.completion_zero AddMonoidHom.completion_zero
292+
293+
theorem AddMonoidHom.completion_add {γ : Type _} [AddCommGroup γ] [UniformSpace γ]
294+
[UniformAddGroup γ] (f g : α →+ γ) (hf : Continuous f) (hg : Continuous g) :
295+
AddMonoidHom.completion (f + g) (hf.add hg) =
296+
AddMonoidHom.completion f hf + AddMonoidHom.completion g hg := by
297+
have hfg := hf.add hg
298+
ext x
299+
refine Completion.induction_on x ?_ ?_
300+
· exact isClosed_eq ((f + g).continuous_completion hfg)
301+
((f.continuous_completion hf).add (g.continuous_completion hg))
302+
· intro a
303+
simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]
304+
#align add_monoid_hom.completion_add AddMonoidHom.completion_add
305+
306+
end AddMonoidHom

‎Mathlib/Topology/UniformSpace/Completion.lean‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -383,9 +383,14 @@ instance : SeparatedSpace (Completion α) :=
383383
instance : T3Space (Completion α) :=
384384
separated_t3
385385

386+
/-- The map from a uniform space to its completion.
387+
388+
porting note: this was added to create a target for the `@[coe]` attribute. -/
389+
@[coe] def coe' : α → Completion α := Quotient.mk' ∘ pureCauchy
390+
386391
/-- Automatic coercion from `α` to its completion. Not always injective. -/
387-
instance : CoeTC α (Completion α) :=
388-
⟨Quotient.mk' ∘ pureCauchy⟩
392+
instance : Coe α (Completion α) :=
393+
⟨coe' α⟩
389394

390395
-- note [use has_coe_t]
391396
protected theorem coe_eq : ((↑) : α → Completion α) = Quotient.mk' ∘ pureCauchy :=
@@ -637,7 +642,7 @@ def completionSeparationQuotientEquiv (α : Type u) [UniformSpace α] :
637642
rintro ⟨a⟩
638643
-- porting note: had to insert rewrites to switch between Quot.mk, Quotient.mk, Quotient.mk'
639644
rw [← Quotient.mk,extension_coe (SeparationQuotient.uniformContinuous_lift _),
640-
SeparationQuotient.lift_mk (uniformContinuous_coe α), UniformSpace.Completion.coe_eq, map_coe]
645+
SeparationQuotient.lift_mk (uniformContinuous_coe α), map_coe]
641646
. rfl
642647
. exact uniformContinuous_quotient_mk
643648
· intro a

0 commit comments

Comments
 (0)