smulOfRingMorphism — Mathlib

English

Given a ring morphism φ: R →+* CatCenter C, the morphisms X → Y in C carry an R-module structure via a • f := φ(a).app X ≫ f.

Русский

Пусть φ: R →+* CatCenter C – гомоморфизм кольца, тогда морфизмы X → Y в C образуют R-модуль со следующим действием: a • f = φ(a).app X ∘ f.

LaTeX

$$$smul\ a\ f := (\phi\ a).app X \circ f$$$

Lean4

/-- The scalar multiplication by `R` on the type `X ⟶ Y` of morphisms in
a category `C` equipped with a ring morphism `R →+* CatCenter C`. -/
def smulOfRingMorphism : SMul R (X ⟶ Y) where smul a f := (φ a).app X ≫ f

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