Documentation

Mathlib.Algebra.Homology.BifunctorShift

Behavior of the action of a bifunctor on cochain complexes with respect to shifts #

In this file, given cochain complexes K₁ : CochainComplex C₁ ℤ, K₂ : CochainComplex C₂ ℤ and a functor F : C₁ ⥤ C₂ ⥤ D, we define an isomorphism of cochain complexes in D:

In the lemma CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, we obtain that the two ways to deduce an isomorphism mapBifunctor (K₁⟦x⟧) (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦x + y⟧ differ by the sign (x * y).negOnePow.

@[reducible, inline]
abbrev CochainComplex.HasMapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] :

The condition that ((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂ has a total cochain complex.

Equations
Instances For
    @[reducible, inline]
    noncomputable abbrev CochainComplex.mapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] [K₁.HasMapBifunctor K₂ F] :

    Given K₁ : CochainComplex C₁ ℤ, K₂ : CochainComplex C₂ ℤ, a bifunctor F : C₁ ⥤ C₂ ⥤ D, this mapBifunctor K₁ K₂ F : CochainComplex D ℤ is the total complex of the bicomplex obtained by applying F to K₁ and K₂.

    Equations
    Instances For
      @[reducible, inline]
      noncomputable abbrev CochainComplex.ιMapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] [K₁.HasMapBifunctor K₂ F] (n₁ : ) (n₂ : ) (n : ) (h : n₁ + n₂ = n) :
      (F.obj (K₁.X n₁)).obj (K₂.X n₂) (K₁.mapBifunctor K₂ F).X n

      The inclusion of a summand (F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n of the total cochain complex when n₁ + n₂ = n.

      Equations
      Instances For
        @[simp]
        theorem CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ) (i : ) :
        ∀ (x_1 : ), ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).inv.f i).f x_1 = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))
        @[simp]
        theorem CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ) (i : ) :
        ∀ (x_1 : ), ((K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom.f i).f x_1 = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X (i + x))).obj (K₂.X x_1))
        def CochainComplex.mapBifunctorHomologicalComplexShift₁Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ) :
        ((F.mapBifunctorHomologicalComplex (ComplexShape.up ) (ComplexShape.up )).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up )) x).obj K₁)).obj K₂ (HomologicalComplex₂.shiftFunctor₁ D x).obj (((F.mapBifunctorHomologicalComplex (ComplexShape.up ) (ComplexShape.up )).obj K₁).obj K₂)

        Auxiliary definition for mapBifunctorShift₁Iso.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          instance CochainComplex.instHasMapBifunctorObjIntShiftFunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ) [K₁.HasMapBifunctor K₂ F] :
          ((CategoryTheory.shiftFunctor (CochainComplex C₁ ) x).obj K₁).HasMapBifunctor K₂ F
          Equations
          • =
          noncomputable def CochainComplex.mapBifunctorShift₁Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ) [K₁.HasMapBifunctor K₂ F] :
          ((CategoryTheory.shiftFunctor (CochainComplex C₁ ) x).obj K₁).mapBifunctor K₂ F (CategoryTheory.shiftFunctor (CochainComplex D ) x).obj (K₁.mapBifunctor K₂ F)

          The canonical isomorphism mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧. This isomorphism does not involve signs.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ) (i : ) (i : ) :
            ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).inv.f i✝).f i = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X i✝)).obj (K₂.X (i + y)))
            @[simp]
            theorem CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ) (i : ) (i : ) :
            ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom.f i✝).f i = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X i✝)).obj (K₂.X (i + y)))
            def CochainComplex.mapBifunctorHomologicalComplexShift₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ) :
            ((F.mapBifunctorHomologicalComplex (ComplexShape.up ) (ComplexShape.up )).obj K₁).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up )) y).obj K₂) (HomologicalComplex₂.shiftFunctor₂ D y).obj (((F.mapBifunctorHomologicalComplex (ComplexShape.up ) (ComplexShape.up )).obj K₁).obj K₂)

            Auxiliary definition for mapBifunctorShift₂Iso.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              instance CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1 {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ) [K₁.HasMapBifunctor K₂ F] :
              K₁.HasMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ) y).obj K₂) F
              Equations
              • =
              noncomputable def CochainComplex.mapBifunctorShift₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ) [K₁.HasMapBifunctor K₂ F] :
              K₁.mapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ) y).obj K₂) F (CategoryTheory.shiftFunctor (CochainComplex D ) y).obj (K₁.mapBifunctor K₂ F)

              The canonical isomorphism mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧. This isomorphism involves signs: on the summand (F.obj (K₁.X p)).obj (K₂.X q), it is given by the multiplication by (p * y).negOnePow.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_4, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ) (K₂ : CochainComplex C₂ ) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (x : ) (y : ) [K₁.HasMapBifunctor K₂ F] :
                K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ) y).obj K₂) F x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) = (x * y).negOnePow ((CategoryTheory.shiftFunctor (CochainComplex C₁ ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex D ) x y).app (K₁.mapBifunctor K₂ F)