leftComp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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