smulOfRingMorphism_smul_eq — Mathlib

English

Let R be a ring and C a preadditive category equipped with a ring morphism φ: R →+* CatCenter C. Then for any objects X, Y in C and any morphism f: X ⟶ Y, the R-action on Hom_C(X, Y) is given by left whiskering with the X-component of φ(a): a • f = (φ(a)).app X ≫ f.

Русский

Пусть R — кольцо, C — преддобавительная категория, и φ: R →+* CatCenter C. Тогда для любых объектов X, Y и морфизма f: X → Y действие элемента a ∈ R на f равно композиции с компонентом φ(a) на X: a • f = (φ(a)).app X ≫ f.

LaTeX

$$$a \cdot f = ((\phi(a))_{X}) \circ f$$$

Lean4

theorem smulOfRingMorphism_smul_eq (a : R) (f : X ⟶ Y) :
    letI := smulOfRingMorphism φ X Y
    a • f = (φ a).app X ≫ f :=
  rfl

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