English
The additive completion of SemiNormedGrp yields an additive functor; maps respect addition of morphisms.
Русский
Аддитивное дополнение категории SemiNormedGrp образует аддитивный функтор; отображения сохраняют сложение морфизмов.
LaTeX
$$$\text{completion} : \mathrm{SemiNormedGrp} \to \mathrm{SemiNormedGrp}$ is additive; i.e., \mathrm{completion}(f+g) = \mathrm{completion}(f) + \mathrm{completion}(g).$$$
Lean4
instance hasLimit_parallelPair {V W : SemiNormedGrp.{u}} (f g : V ⟶ W) : HasLimit (parallelPair f g) where
exists_limit :=
Nonempty.intro
{ cone := fork f g
isLimit :=
have this := fun (c : Fork f g) =>
show NormedAddGroupHom.compHom (f - g).hom c.ι.hom = 0
by
rw [hom_sub, AddMonoidHom.map_sub, AddMonoidHom.sub_apply, sub_eq_zero]
exact congr_arg Hom.hom c.condition
Fork.IsLimit.mk _ (fun c => ofHom <| NormedAddGroupHom.ker.lift (Fork.ι c).hom _ <| this c)
(fun _ => SemiNormedGrp.hom_ext <| NormedAddGroupHom.ker.incl_comp_lift _ _ (this _)) fun c g h => by ext x;
dsimp; simp_rw [← h]; rfl }
