Theorems · Definition · category theory

HomologicalComplex.dgoEquivHomologicalComplexUnitIso

{β : Type u_1} →
  [inst : AddCommGroup β] →
    (b : β) →
      (V : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            CategoryTheory.Functor.id (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) ≅
              (HomologicalComplex.dgoToHomologicalComplex b V).comp (HomologicalComplex.homologicalComplexToDGO b V)

The unit isomorphism for dgoEquivHomologicalComplex.

Defined in

Mathlib.Algebra.Homology.DifferentialObject

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroupCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms