English
Let X and Y be topological R-modules and f: X →L[R] Y a continuous linear map. Then the morphism in the category TopModuleCat determined by f has the same linear part, i.e. its hom component equals f.
Русский
Пусть X и Y — топологические R-модули и f: X →L[R] Y — непрерывный линейный отображатель. Тогда соответствующий этому отображению морфизм в категории TopModuleCat имеет ту же линейную часть, то есть компоненту Hom равен f.
LaTeX
$$$ (\operatorname{ofHom}(f)).\\hom = f $$$
Lean4
@[simp]
theorem hom_ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X]
[ContinuousSMul R X] [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y]
(f : X →L[R] Y) : (ofHom f).hom = f :=
rfl
