Theorems · Definition · category theory

HomologicalComplex.Hom.noConfusion

{P : Sort u_2} →
  {ι : Type u_1} →
    {V : Type u} →
      {inst : CategoryTheory.Category.{v, u} V} →
        {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} →
          {c : ComplexShape ι} →
            {A B : HomologicalComplex V c} →
              {t : A.Hom B} →
                {ι' : Type u_1} →
                  {V' : Type u} →
                    {inst' : CategoryTheory.Category.{v, u} V'} →
                      {inst'_1 : CategoryTheory.Limits.HasZeroMorphisms V'} →
                        {c' : ComplexShape ι'} →
                          {A' B' : HomologicalComplex V' c'} →
                            {t' : A'.Hom B'} →
                              ι = ι' →
                                V = V' →
                                  inst ≍ inst' →
                                    inst_1 ≍ inst'_1 →
                                      c ≍ c' → A ≍ A' → B ≍ B' → t ≍ t' → HomologicalComplex.Hom.noConfusionType P t t'

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms