Documentation

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

The short complexes attached to homological complexes #

In this file, we define a functor shortComplexFunctor C c i : HomologicalComplex C c ⥤ ShortComplex C. By definition, the image of a homological complex K by this functor is the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

When the homology refactor is completed (TODO @joelriou), the homology of a homological complex K in degree i shall be the homology of the short complex (shortComplexFunctor C c i).obj K, which can be abbreviated as K.sc i.

The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

Instances For

    The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

    Instances For
      @[simp]
      theorem HomologicalComplex.natIsoSc'_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₃ = (HomologicalComplex.XIsoOfEq X hk).inv
      @[simp]
      theorem HomologicalComplex.natIsoSc'_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₁ = (HomologicalComplex.XIsoOfEq X hi).hom
      @[simp]
      theorem HomologicalComplex.natIsoSc'_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₁ = (HomologicalComplex.XIsoOfEq X hi).inv
      @[simp]
      theorem HomologicalComplex.natIsoSc'_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₃ = (HomologicalComplex.XIsoOfEq X hk).hom

      The natural isomorphism shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k when c.prev j = i and c.next j = k.

      Instances For
        @[inline, reducible]

        The short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

        Instances For
          @[inline, reducible]

          The short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

          Instances For
            @[inline, reducible]
            noncomputable abbrev HomologicalComplex.isoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) :

            The canonical isomorphism K.sc j ≅ K.sc' i j k when c.prev j = i and c.next j = k.

            Instances For