Theorems · Theorem · category theory

CategoryTheory.Free.lift_map_single

∀ (R : Type u_1) [inst : CommRing R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {D : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (r : R),
  ((CategoryTheory.Free.lift R F).map fun₀ | f => r) = r • F.map f

Defined in

Mathlib.Algebra.Category.ModuleCat.Adjunctions

Cited by

0 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Linear