mapHom

Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion

URI: https://scilib.ai/kg/mathlib#SemiNormedGrp.completion.mapHom

Lean4

/-- 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 mapHom (V W : SemiNormedGrp.{u}) : (V ⟶ W) →+ (completion.obj V ⟶ completion.obj W) :=
  @AddMonoidHom.mk' _ _ (_) (_) completion.map fun f g => SemiNormedGrp.hom_ext (f.hom.completion_add g.hom)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru