Theorems · Definition · category theory

HomologicalComplex.extend

{ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                HomologicalComplex C c → c.Embedding c' → HomologicalComplex C c'

Given K : HomologicalComplex C c and e : c.Embedding c', this is the extension of K in HomologicalComplex C c': it is zero in the degrees that are not in the image of e.f.

Defined in

Mathlib.Algebra.Homology.Embedding.Extend

Cited by

115 results in Mathlib

Foundations

Depth 17 from the axioms, rests on 141 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasZeroMorphisms