single_comp_single — Mathlib

English

In the free construction on a category C, the composition of two single-morphism generators corresponds to a single-morphism on the composite with the product of scalars: single f r ≫ single g s = single (f ≫ g) (r s).

Русский

В свободной конструкции над категорией C композиция двух элементарных морфизмов соответствует одному морфизму на композицию с произведением скаляров: single f r ≫ single g s = single (f ≫ g) (r s).

LaTeX

$$$\mathrm{SingleCompSingle}: (single\ f\ r)\;\; (single\ g\ s) = single\ (f\!\circ g)\ (r\cdot s)$$$

Lean4

theorem single_comp_single {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) :
    (single f r ≫ single g s : Free.of R X ⟶ Free.of R Z) = single (f ≫ g) (r * s) := by
  dsimp [CategoryTheory.categoryFree]; simp

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