Theorems · Theorem · category theory

ChainComplex.linearYonedaObj_d

∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : CategoryTheory.Abelian C] {α : Type u_3}
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] (X : ChainComplex C α) (A : Type u_4) [inst_4 : Ring A]
  [inst_5 : CategoryTheory.Linear A C] (Y : C) (i j : α),
  (X.linearYonedaObj A Y).d i j = ModuleCat.ofHom (CategoryTheory.Linear.leftComp A Y (X.d j i))

Defined in

Mathlib.CategoryTheory.Abelian.Ext

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianAddRightCancelSemigroupOneRingCategoryTheory.Linear