instSMulIntHomObjTopCommRingCatForget₂

English

Integer-scalar action on morphisms is defined via the underlying integer action on the hom-objects.

Русский

Действие целочисленных скаляров на морфизмы задаётся через действие целых чисел на гом-объектах.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; f \\in \\mathrm{Hom}(X, (forget\\_2 TopCommRingCat TopCat).obj(R)),\\quad n \\cdot f := \\text{ofHom}(n \\cdot f.hom).$$$

Lean4

instance : SMul ℤ (X ⟶ (forget₂ TopCommRingCat TopCat).obj R) where smul n f := ofHom (n • f.hom)

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