feat(analysis/normed/group/SemiNormedGroup/completion): add SemiNorme…

…dGroup.Completion (#9788)

From LTE.

src/analysis/normed/group/SemiNormedGroup/completion.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2021 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca, Johan Commelin
+-/
+import analysis.normed.group.SemiNormedGroup
+import category_theory.preadditive.additive_functor
+import analysis.normed.group.hom_completion
+
+/-!
+# Completions of normed groups
+
+This file contains an API for completions of seminormed groups (basic facts about
+objects and morphisms).
+
+## Main definitions
+
+- `SemiNormedGroup.Completion : SemiNormedGroup ⥤ SemiNormedGroup` : the completion of a
+  seminormed group (defined as a functor on `SemiNormedGroup` to itself).
+- `SemiNormedGroup.Completion.lift (f : V ⟶ W) : (Completion.obj V ⟶ W)` : a normed group hom
+  from `V` to complete `W` extends ("lifts") to a seminormed group hom from the completion of
+  `V` to `W`.
+
+## Projects
+
+1. Construct the category of complete seminormed groups, say `CompleteSemiNormedGroup`
+  and promote the `Completion` functor below to a functor landing in this category.
+2. Prove that the functor `Completion : SemiNormedGroup ⥤ CompleteSemiNormedGroup`
+  is left adjoint to the forgetful functor.
+
+-/
+
+noncomputable theory
+
+universe u
+
+namespace SemiNormedGroup
+open uniform_space opposite category_theory normed_group_hom
+
+/-- The completion of a seminormed group, as an endofunctor on `SemiNormedGroup`. -/
+@[simps]
+def Completion : SemiNormedGroup.{u} ⥤ SemiNormedGroup.{u} :=
+{ obj := λ V, SemiNormedGroup.of (completion V),
+  map := λ V W f, f.completion,
+  map_id' := λ V, completion_id,
+  map_comp' := λ U V W f g, (completion_comp f g).symm }
+
+instance Completion_complete_space {V : SemiNormedGroup} : complete_space (Completion.obj V) :=
+completion.complete_space _
+
+/-- The canonical morphism from a seminormed group `V` to its completion. -/
+@[simps]
+def Completion.incl {V : SemiNormedGroup} : V ⟶ Completion.obj V :=
+{ to_fun := λ v, (v : completion V),
+  map_add' := completion.coe_add,
+  bound' := ⟨1, λ v, by simp⟩ }
+
+lemma Completion.norm_incl_eq {V : SemiNormedGroup} {v : V} : ∥Completion.incl v∥ = ∥v∥ := by simp
+
+lemma Completion.map_norm_noninc {V W : SemiNormedGroup} {f : V ⟶ W} (hf : f.norm_noninc) :
+  (Completion.map f).norm_noninc :=
+normed_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.2 $
+  (normed_group_hom.norm_completion f).le.trans $
+  normed_group_hom.norm_noninc.norm_noninc_iff_norm_le_one.1 hf
+
+/-- Given a normed group hom `V ⟶ W`, this defines the associated morphism
+from the completion of `V` to the completion of `W`.
+The difference from the definition obtained from the functoriality of completion is in that the
+map sending a morphism `f` to the associated morphism of completions is itself additive. -/
+def Completion.map_hom (V W : SemiNormedGroup.{u}) :
+  (V ⟶ W) →+ (Completion.obj V ⟶ Completion.obj W) :=
+add_monoid_hom.mk' (category_theory.functor.map Completion) $ λ f g,
+  f.completion_add g
+
+@[simp] lemma Completion.map_zero (V W : SemiNormedGroup) : Completion.map (0 : V ⟶ W) = 0 :=
+(Completion.map_hom V W).map_zero
+
+instance : preadditive SemiNormedGroup.{u} :=
+{ hom_group := λ P Q, infer_instance,
+  add_comp' := by { intros, ext,
+    simp only [normed_group_hom.add_apply, category_theory.comp_apply, normed_group_hom.map_add] },
+  comp_add' := by { intros, ext,
+    simp only [normed_group_hom.add_apply, category_theory.comp_apply, normed_group_hom.map_add] } }
+
+instance : functor.additive Completion :=
+{ map_zero' := Completion.map_zero,
+  map_add' := λ X Y, (Completion.map_hom _ _).map_add }
+
+/-- Given a normed group hom `f : V → W` with `W` complete, this provides a lift of `f` to
+the completion of `V`. The lemmas `lift_unique` and `lift_comp_incl` provide the api for the
+universal property of the completion. -/
+def Completion.lift {V W : SemiNormedGroup} [complete_space W] [separated_space W] (f : V ⟶ W) :
+  Completion.obj V ⟶ W :=
+{ to_fun := f.extension,
+  map_add' := f.extension.to_add_monoid_hom.map_add',
+  bound' := f.extension.bound' }
+
+lemma Completion.lift_comp_incl {V W : SemiNormedGroup} [complete_space W] [separated_space W]
+  (f : V ⟶ W) : Completion.incl ≫ (Completion.lift f) = f :=
+by { ext, apply normed_group_hom.extension_coe }
+
+lemma Completion.lift_unique {V W : SemiNormedGroup} [complete_space W] [separated_space W]
+  (f : V ⟶ W) (g : Completion.obj V ⟶ W) : Completion.incl ≫ g = f → g = Completion.lift f :=
+λ h, (normed_group_hom.extension_unique _ (λ v, ((ext_iff.1 h) v).symm)).symm
+
+end SemiNormedGroup

src/analysis/normed/group/hom_completion.lean

@@ -41,12 +41,16 @@ The vertical maps in the above diagrams are also normed group homs constructed i
   kernel of `f`.
 * `normed_group_hom.ker_completion`: the kernel of `f.completion` is the closure of the image of the
   kernel of `f` under an assumption that `f` is quantitatively surjective onto its image.
+* `normed_group_hom.extension` : if `H` is complete, the extension of `f : normed_group_hom G H`
+  to a `normed_group_hom (completion G) H`.
 -/
 
 noncomputable theory
 
 open set normed_group_hom uniform_space
 
+section completion
+
 variables {G : Type*} [semi_normed_group G]
 variables {H : Type*} [semi_normed_group H]
 variables {K : Type*} [semi_normed_group K]
@@ -226,3 +230,41 @@ begin
   { rw ← f.completion.is_closed_ker.closure_eq,
     exact closure_mono f.ker_le_ker_completion }
 end
+
+end completion
+
+section extension
+
+variables {G : Type*} [semi_normed_group G]
+variables {H : Type*} [semi_normed_group H] [separated_space H] [complete_space H]
+
+/-- If `H` is complete, the extension of `f : normed_group_hom G H` to a
+`normed_group_hom (completion G) H`. -/
+def normed_group_hom.extension (f : normed_group_hom G H) : normed_group_hom (completion G) H :=
+{ bound' := begin
+    refine ⟨∥f∥, λ v, completion.induction_on v (is_closed_le _ _) (λ a, _)⟩,
+    { exact continuous.comp continuous_norm completion.continuous_extension },
+    { exact continuous.mul continuous_const continuous_norm },
+    { rw [completion.norm_coe, add_monoid_hom.to_fun_eq_coe, add_monoid_hom.extension_coe],
+      exact le_op_norm f a }
+  end,
+  ..f.to_add_monoid_hom.extension f.continuous }
+
+lemma normed_group_hom.extension_def (f : normed_group_hom G H) (v : G) :
+  f.extension v = completion.extension f v := rfl
+
+@[simp] lemma normed_group_hom.extension_coe (f : normed_group_hom G H) (v : G) :
+  f.extension v = f v := add_monoid_hom.extension_coe _ f.continuous _
+
+lemma normed_group_hom.extension_coe_to_fun (f : normed_group_hom G H) :
+  (f.extension : (completion G) → H) = completion.extension f := rfl
+
+lemma normed_group_hom.extension_unique (f : normed_group_hom G H)
+  {g : normed_group_hom (completion G) H} (hg : ∀ v, f v = g v) : f.extension = g :=
+begin
+  ext v,
+  rw [normed_group_hom.extension_coe_to_fun, completion.extension_unique f.uniform_continuous
+    g.uniform_continuous (λ a, hg a)]
+end
+
+end extension