Theorems · Definition · category theory

CategoryTheory.Linear.leftComp

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (R : Type w) →
        [inst_2 : Semiring R] →
          [inst_3 : CategoryTheory.Linear R C] → {X Y : C} → (Z : C) → (X ⟶ Y) → (Y ⟶ Z) →ₗ[R] X ⟶ Z

Composition by a fixed left argument as an R-linear map.

Defined in

Mathlib.CategoryTheory.Linear.Basic

Cited by

7 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveSemiringCategoryTheory.Linear