Theorems · Definition · category theory

ChainComplex.linearYonedaObj

{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 α] →
            ChainComplex C α →
              (A : Type u_4) → [inst_4 : Ring A] → [CategoryTheory.Linear A C] → C → CochainComplex (ModuleCat A) α

Given a chain complex X and an object Y, this is the cochain complex which in degree i consists of the module of morphisms X.X i ⟶ Y.

Defined in

Mathlib.CategoryTheory.Abelian.Ext

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianAddRightCancelSemigroupOneRingCategoryTheory.Linear