feat(analysis/normed_space): SemiNormedGroup.has_zero_object (#7740)

From LTE.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/analysis/normed_space/SemiNormedGroup.lean

@@ -37,12 +37,25 @@ instance (M : SemiNormedGroup) : semi_normed_group M := M.str
 
 @[simp] lemma coe_of (V : Type u) [semi_normed_group V] : (SemiNormedGroup.of V : Type u) = V := rfl
 @[simp] lemma coe_id (V : SemiNormedGroup) : ⇑(𝟙 V) = id := rfl
+@[simp] lemma coe_comp {M N K : SemiNormedGroup} (f : M ⟶ N) (g : N ⟶ K) :
+  ((f ≫ g) : M → K) = g ∘ f := rfl
 
 instance : has_zero SemiNormedGroup := ⟨of punit⟩
 instance : inhabited SemiNormedGroup := ⟨0⟩
 
 instance : limits.has_zero_morphisms.{u (u+1)} SemiNormedGroup := {}
 
+@[simp] lemma zero_apply {V W : SemiNormedGroup} (x : V) : (0 : V ⟶ W) x = 0 := rfl
+
+instance has_zero_object : limits.has_zero_object SemiNormedGroup.{u} :=
+{ zero := 0,
+  unique_to := λ X,
+  { default := 0,
+    uniq := λ a, by { ext ⟨⟩, exact a.map_zero, }, },
+  unique_from := λ X,
+  { default := 0,
+    uniq := λ f, by ext } }
+
 end SemiNormedGroup
 
 /--
@@ -112,6 +125,15 @@ instance : limits.has_zero_morphisms.{u (u+1)} SemiNormedGroup₁ :=
 
 @[simp] lemma zero_apply {V W : SemiNormedGroup₁} (x : V) : (0 : V ⟶ W) x = 0 := rfl
 
+instance has_zero_object : limits.has_zero_object SemiNormedGroup₁.{u} :=
+{ zero := 0,
+  unique_to := λ X,
+  { default := 0,
+    uniq := λ a, by { ext ⟨⟩, exact a.1.map_zero, }, },
+  unique_from := λ X,
+  { default := 0,
+    uniq := λ f, by ext } }
+
 lemma iso_isometry {V W : SemiNormedGroup₁} (i : V ≅ W) :
   isometry i.hom :=
 begin