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
      def HomologicalComplex₂.toGradedObjectMap {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₂} (φ : K ⟶ L) :
      HomologicalComplex₂.toGradedObject K ⟶ HomologicalComplex₂.toGradedObject L

      The morphism of graded objects induced by a morphism of bicomplexes.

      Equations
      Instances For
        source
        @[simp]
        theorem HomologicalComplex₂.toGradedObjectMap_apply {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₂} (φ : K ⟶ L) (i₁ : I₁) (i₂ : I₂) :
        HomologicalComplex₂.toGradedObjectMap φ (i₁, i₂) = (φ.f i₁).f i₂
        source
        @[simp]
        theorem HomologicalComplex₂.toGradedObjectFunctor_map (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 Y : HomologicalComplex₂ C c₁ c₂} (φ : X ⟶ Y) (i : I₁ × I₂), (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).map φ i = HomologicalComplex₂.toGradedObjectMap φ i
        source
        @[simp]
        theorem HomologicalComplex₂.toGradedObjectFunctor_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₂.toGradedObjectFunctor C c₁ c₂).obj K = HomologicalComplex₂.toGradedObject K
        source
        def HomologicalComplex₂.toGradedObjectFunctor (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₂) (CategoryTheory.GradedObject (I₁ × I₂) C)

        The functor which sends a bicomplex to its associated graded object.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance HomologicalComplex₂.instFaithfulHomologicalComplex₂InstCategoryHomologicalComplexHomologicalComplexInstCategoryHomologicalComplexInstHasZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexGradedObjectProdCategoryOfGradedObjectsToGradedObjectFunctor {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.Faithful (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂)
          Equations
          • ⋯ = ⋯
          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_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
          @[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
          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_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₂).obj K = HomologicalComplex₂.flip K
            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₂).map f).f i).f j = (f.f j).f i
            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_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
              @[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
              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_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
                @[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
                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_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_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
                  @[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_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
                  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