rightComp — Mathlib

English

For fixed X and morphisms g: Y → Z, the map f ↦ f ≫ g is an R-linear map from X ⟶ Y to X ⟶ Z.

Русский

Для фиксированного X и морфизма g: Y → Z отображение f ↦ f ∘ g линейно над R из Hom(X,Y) в Hom(X,Z).

LaTeX

$$$\\text{rightComp}(X)(g): (X\\to Y) \\to_{R} (X\\to Z)\\;\\text{ is }R\\text{-linear}.$$$

Lean4

/-- Composition by a fixed right argument as an `R`-linear map. -/
@[simps]
def rightComp (X : C) {Y Z : C} (g : Y ⟶ Z) : (X ⟶ Y) →ₗ[R] X ⟶ Z
    where
  toFun f := f ≫ g
  map_add' := by simp
  map_smul' := by simp

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