instModuleHom — Mathlib

English

For a topological S-module S, the Hom-set (TopModuleCat S)(X,Y) carries the S-module structure given by smul r f := ofHom (r • f.hom).

Русский

Для топологического S-модуля S множество гомоморфизмов (TopModuleCat S)(X,Y) приобретает структуру S-модуля: smul r f := ofHom (r • f.hom).

LaTeX

$$$ r \cdot f := \operatorname{ofHom}(r \cdot f.\\hom) $$$

Lean4

instance {X Y : TopModuleCat S} : Module S (X ⟶ Y)
    where
  smul r f := ofHom (r • f.hom)
  __ := Equiv.module _ CategoryTheory.ConcreteCategory.homEquiv

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