instSMulNatHomObjTopCommRingCatForget₂

English

Natural-number scalar multiplication acts on morphisms by lifting the action through the underlying hom-objects.

Русский

Действие по умножению на натуральное число распространяется на морфизмы через соответствующие основания гом-объектов.

LaTeX

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

Lean4

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

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