comp — Mathlib

English

Composition is a bilinear map in its two arguments.

Русский

Составление морфизмов является билинейной операцией по двум аргументам.

LaTeX

$$$\\operatorname{comp}: \\mathrm{Hom}(X,Y) \\times \\mathrm{Hom}(Y,Z) \\to \\mathrm{Hom}(X,Z)$ is bilinear over the base semiring.$$

Lean4

/-- Composition as a bilinear map. -/
@[simps]
def comp (X Y Z : C) : (X ⟶ Y) →ₗ[S] (Y ⟶ Z) →ₗ[S] X ⟶ Z
    where
  toFun f := leftComp S Z f
  map_add' := by
    intros
    ext
    simp
  map_smul' := by
    intros
    ext
    simp

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