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.

source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_f (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) :
((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).f = HomologicalComplex.d K i j
source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) :
∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₁ = HomologicalComplex.Hom.f f i
source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_X₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) :
((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₂ = HomologicalComplex.X K j
source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_X₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) :
((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₁ = HomologicalComplex.X K i
source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) :
∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₂ = HomologicalComplex.Hom.f f j
source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_g (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) :
((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).g = HomologicalComplex.d K j k
source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) :
∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₃ = HomologicalComplex.Hom.f f k
source
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_obj_X₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) :
((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₃ = HomologicalComplex.X K k
source
def HomologicalComplex.shortComplexFunctor' (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) :
CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ShortComplex C)

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
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_obj_f (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) :
    ((HomologicalComplex.shortComplexFunctor C c i).obj K).f = HomologicalComplex.d K (ComplexShape.prev c i) i
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_map_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) :
    ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₃ = HomologicalComplex.Hom.f f (ComplexShape.next c i)
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_obj_X₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) :
    ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₁ = HomologicalComplex.X K (ComplexShape.prev c i)
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_obj_g (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) :
    ((HomologicalComplex.shortComplexFunctor C c i).obj K).g = HomologicalComplex.d K i (ComplexShape.next c i)
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_obj_X₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) :
    ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₃ = HomologicalComplex.X K (ComplexShape.next c i)
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_map_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) :
    ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₁ = HomologicalComplex.Hom.f f (ComplexShape.prev c i)
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_obj_X₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) :
    ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₂ = HomologicalComplex.X K i
    source
    @[simp]
    theorem HomologicalComplex.shortComplexFunctor_map_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) :
    ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₂ = HomologicalComplex.Hom.f f i
    source
    noncomputable def HomologicalComplex.shortComplexFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) :
    CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ShortComplex C)

    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
      source
      @[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).τ₂ = CategoryTheory.CategoryStruct.id (HomologicalComplex.X X j)
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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).τ₂ = CategoryTheory.CategoryStruct.id (HomologicalComplex.X X j)
      source
      @[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
      source
      noncomputable def HomologicalComplex.natIsoSc' (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) :
      HomologicalComplex.shortComplexFunctor C c j ≅ HomologicalComplex.shortComplexFunctor' C c i j k

      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
        source
        @[inline, reducible]
        abbrev HomologicalComplex.sc' {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 : ι) :
        CategoryTheory.ShortComplex C

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

        Instances For
          source
          @[inline, reducible]
          noncomputable abbrev HomologicalComplex.sc {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 : ι) :
          CategoryTheory.ShortComplex C

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

          Instances For
            source
            @[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) :
            HomologicalComplex.sc K j ≅ HomologicalComplex.sc' K i 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