Theorems · Definition · category theory

CategoryTheory.Triangulated.TStructure.Heart.noConfusionType

Sort u_1 →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Preadditive C] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                {t : CategoryTheory.Triangulated.TStructure C} →
                  {H : Type u'} →
                    [inst_6 : CategoryTheory.Category.{v', u'} H] →
                      [inst_7 : CategoryTheory.Preadditive H] →
                        t.Heart H →
                          {C' : Type u} →
                            [inst' : CategoryTheory.Category.{v, u} C'] →
                              [inst'_1 : CategoryTheory.Preadditive C'] →
                                [inst'_2 : CategoryTheory.Limits.HasZeroObject C'] →
                                  [inst'_3 : CategoryTheory.HasShift C' ℤ] →
                                    [inst'_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C' n).Additive] →
                                      [inst'_5 : CategoryTheory.Pretriangulated C'] →
                                        {t' : CategoryTheory.Triangulated.TStructure C'} →
                                          {H' : Type u'} →
                                            [inst'_6 : CategoryTheory.Category.{v', u'} H'] →
                                              [inst'_7 : CategoryTheory.Preadditive H'] → t'.Heart H' → Sort u_1

Defined in: Mathlib.CategoryTheory.Triangulated.TStructure.Heart
Cited by: 0 results in Mathlib
Foundations: Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Preadditive CategoryTheory.Limits.HasZeroObject CategoryTheory.HasShift CategoryTheory.Functor.Additive CategoryTheory.Pretriangulated CategoryTheory.Category CategoryTheory.Preadditive CategoryTheory.Category CategoryTheory.Preadditive CategoryTheory.Limits.HasZeroObject CategoryTheory.HasShift CategoryTheory.Functor.Additive CategoryTheory.Pretriangulated CategoryTheory.Category CategoryTheory.Preadditive

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functorproof · cited by 16,252
CategoryTheory.Preadditivestatement and proof · cited by 3,309
CategoryTheory.shiftFunctorstatement and proof · cited by 1,553
CategoryTheory.HasShiftstatement and proof · cited by 1,527
CategoryTheory.Limits.HasZeroObjectstatement and proof · cited by 1,298
CategoryTheory.Functor.Additivestatement and proof · cited by 1,179
CategoryTheory.Pretriangulatedstatement and proof · cited by 669
CategoryTheory.Functor.Fullproof · cited by 341
CategoryTheory.Triangulated.TStructurestatement and proof · cited by 318
CategoryTheory.Functor.Faithfulproof · cited by 313
CategoryTheory.Functor.essImageproof · cited by 82

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Triangulated.TStructure.Heart.noConfusionstatement · cited by 0