Documentation

Mathlib.Algebra.Homology.HomologicalBicomplex

Bicomplexes #

Given a category C with zero morphisms and two complex shapes c₁ : ComplexShape I₁ and c₂ : ComplexShape I₂, we define the type of bicomplexes HomologicalComplex₂ C c₁ c₂ as an abbreviation for HomologicalComplex (HomologicalComplex C c₂) c₁. In particular, if K : HomologicalComplex₂ C c₁ c₂, then for each i₁ : I₁, K.X i₁ is a column of K.

In this file, we obtain the equivalence of categories HomologicalComplex₂.flipEquivalence : HomologicalComplex₂ C c₁ c₂ ≌ HomologicalComplex₂ C c₂ c₁ which is obtained by exchanging the horizontal and vertical directions.

source
@[inline, reducible]
abbrev HomologicalComplex₂ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
Type (max (max (max (max u_1 u_4) u_3) u_2) u_3 u_4)

Given a category C and two complex shapes c₁ and c₂ on types I₁ and I₂, the associated type of bicomplexes HomologicalComplex₂ C c₁ c₂ is K : HomologicalComplex (HomologicalComplex C c₂) c₁. Then, the object in position ⟨i₁, i₂⟩ can be obtained as (K.X i₁).X i₂.

Equations
Instances For
    source
    def HomologicalComplex₂.toGradedObject {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) :
    CategoryTheory.GradedObject (I₁ × I₂) C

    The graded object indexed by I₁ × I₂ induced by a bicomplex.

    Equations
    Instances For
      source
      theorem HomologicalComplex₂.shape_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ : I₁) (i₁' : I₁) (h : ¬c₁.Rel i₁ i₁') (i₂ : I₂) :
      (K.d i₁ i₁').f i₂ = 0
      source
      @[simp]
      theorem HomologicalComplex₂.d_f_comp_d_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ : I₁) (i₁' : I₁) (i₁'' : I₁) (i₂ : I₂) {Z : C} (h : (K.X i₁'').X i₂ ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((K.d i₁' i₁'').f i₂) h) = CategoryTheory.CategoryStruct.comp 0 h
      source
      @[simp]
      theorem HomologicalComplex₂.d_f_comp_d_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ : I₁) (i₁' : I₁) (i₁'' : I₁) (i₂ : I₂) :
      CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((K.d i₁' i₁'').f i₂) = 0
      source
      theorem HomologicalComplex₂.d_comm_assoc {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ : I₁) (i₁' : I₁) (i₂ : I₂) (i₂' : I₂) {Z : C} (h : (K.X i₁').X i₂' ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((K.X i₁').d i₂ i₂') h) = CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂') h)
      source
      theorem HomologicalComplex₂.d_comm {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ : I₁) (i₁' : I₁) (i₂ : I₂) (i₂' : I₂) :
      CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((K.X i₁').d i₂ i₂') = CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') ((K.d i₁ i₁').f i₂')
      source
      @[simp]
      theorem HomologicalComplex₂.comm_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (f : K ⟶ L) (i₁ : I₁) (i₁' : I₁) (i₂ : I₂) {Z : C} (h : (L.X i₁').X i₂ ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((f.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp ((L.d i₁ i₁').f i₂) h) = CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((f.f i₁').f i₂) h)
      source
      @[simp]
      theorem HomologicalComplex₂.comm_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (f : K ⟶ L) (i₁ : I₁) (i₁' : I₁) (i₂ : I₂) :
      CategoryTheory.CategoryStruct.comp ((f.f i₁).f i₂) ((L.d i₁ i₁').f i₂) = CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((f.f i₁').f i₂)
      source
      @[simp]
      theorem HomologicalComplex₂.flip_d_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i : I₂) (i' : I₂) (j : I₁) :
      ((HomologicalComplex₂.flip K).d i i').f j = (K.X j).d i i'
      source
      @[simp]
      theorem HomologicalComplex₂.flip_X_d {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i : I₂) (j : I₁) (j' : I₁) :
      ((HomologicalComplex₂.flip K).X i).d j j' = (K.d j j').f i
      source
      @[simp]
      theorem HomologicalComplex₂.flip_X_X {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i : I₂) (j : I₁) :
      ((HomologicalComplex₂.flip K).X i).X j = (K.X j).X i
      source
      def HomologicalComplex₂.flip {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) :
      HomologicalComplex₂ C c₂ c₁

      Flip a complex of complexes over the diagonal, exchanging the horizontal and vertical directions.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem HomologicalComplex₂.flipFunctor_map_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (f : K ⟶ L) (i : I₂) (j : I₁) :
        (((HomologicalComplex₂.flipFunctor C c₁ c₂).toPrefunctor.map f).f i).f j = (f.f j).f i
        source
        @[simp]
        theorem HomologicalComplex₂.flipFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂) :
        (HomologicalComplex₂.flipFunctor C c₁ c₂).toPrefunctor.obj K = HomologicalComplex₂.flip K
        source
        def HomologicalComplex₂.flipFunctor (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
        CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (HomologicalComplex₂ C c₂ c₁)

        Flipping a complex of complexes over the diagonal, as a functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₁ c₂) (i : I₁) (i : I₂) :
          (((HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂).hom.app X).f i✝).f i = CategoryTheory.CategoryStruct.id ((X.X i✝).X i)
          source
          @[simp]
          theorem HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₁ c₂) (i : I₁) (i : I₂) :
          (((HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂).inv.app X).f i✝).f i = CategoryTheory.CategoryStruct.id ((X.X i✝).X i)
          source
          def HomologicalComplex₂.flipEquivalenceUnitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
          CategoryTheory.Functor.id (HomologicalComplex₂ C c₁ c₂) ≅ CategoryTheory.Functor.comp (HomologicalComplex₂.flipFunctor C c₁ c₂) (HomologicalComplex₂.flipFunctor C c₂ c₁)

          Auxiliary definition for HomologicalComplex₂.flipEquivalence.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₂ c₁) (i : I₂) (i : I₁) :
            (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).hom.app X).f i✝).f i = CategoryTheory.CategoryStruct.id ((X.X i✝).X i)
            source
            @[simp]
            theorem HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₂ c₁) (i : I₂) (i : I₁) :
            (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).inv.app X).f i✝).f i = CategoryTheory.CategoryStruct.id ((X.X i✝).X i)
            source
            def HomologicalComplex₂.flipEquivalenceCounitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
            CategoryTheory.Functor.comp (HomologicalComplex₂.flipFunctor C c₂ c₁) (HomologicalComplex₂.flipFunctor C c₁ c₂) ≅ CategoryTheory.Functor.id (HomologicalComplex₂ C c₂ c₁)

            Auxiliary definition for HomologicalComplex₂.flipEquivalence.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem HomologicalComplex₂.flipEquivalence_unitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
              (HomologicalComplex₂.flipEquivalence C c₁ c₂).unitIso = HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂
              source
              @[simp]
              theorem HomologicalComplex₂.flipEquivalence_inverse (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
              (HomologicalComplex₂.flipEquivalence C c₁ c₂).inverse = HomologicalComplex₂.flipFunctor C c₂ c₁
              source
              @[simp]
              theorem HomologicalComplex₂.flipEquivalence_functor (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
              (HomologicalComplex₂.flipEquivalence C c₁ c₂).functor = HomologicalComplex₂.flipFunctor C c₁ c₂
              source
              @[simp]
              theorem HomologicalComplex₂.flipEquivalence_counitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
              (HomologicalComplex₂.flipEquivalence C c₁ c₂).counitIso = HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂
              source
              def HomologicalComplex₂.flipEquivalence (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) :
              HomologicalComplex₂ C c₁ c₂ ≌ HomologicalComplex₂ C c₂ c₁

              Flipping a complex of complexes over the diagonal, as an equivalence of categories.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For