Two-term support sequences under cochain bifunctor totalization

The high term of a two-term cochain complex is a subcomplex, and the low term is its quotient. A zero-preserving bifunctor carries this support sequence to a natural short exact sequence after cochain totalization. The proof compares each degree with its two supported summands. Splittings are degreewise data; they do not assert that the sequence splits as cochain complexes.

Single-row comparisons identify the endpoint functors with shifted row actions. Specified changes of endpoint functors transport both the short exactness and the degreewise splitting through an isomorphism of short complexes. Only the chosen left complex and its two single-row endpoints need totalizations. Row comparisons and short-complex constructions require a preadditive target; degreewise splittings also require binary biproducts. Abelian hypotheses enter only the short-exactness theorem.

Attribution

The single-row component comparison, inverse, differential calculation and Hom.isoOfComponents construction adapt CategoryTheory.Functor.mapBifunctorLeftUnitor in TauCeti.Algebra.Homology.Bifunctor.Unitor to a row in arbitrary cochain degree. That formalization adapts Mathlib's CategoryTheory.GradedObject.mapBifunctorLeftUnitor and HomologicalComplex.leftUnitor, both due to Joël Riou. The original sources are Mathlib.CategoryTheory.GradedObject.Unitor and Mathlib.Algebra.Homology.Monoidal. The totalization primitives are also Joël Riou's Mathlib bifunctor construction.

structure TauCeti.TwoTermSupport (C₁ : Type u_1) [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] : Type (max u_1 v_1)

A cochain complex with two distinct supported rows, its chosen endpoint identifications, and vanishing differentials required for the high inclusion and low projection.

• K : CochainComplex C₁ ℤ

  The supported cochain complex.

• a : ℤ

  The degree of the low term.

• b : ℤ

  The degree of the high term.

• A : C₁

  The chosen low-term object.

• B : C₁

  The chosen high-term object.

• low : self.K.X self.a ≅ self.A

  Identify the actual low term.

• high : self.K.X self.b ≅ self.B

  Identify the actual high term.

• ne : self.a ≠ self.b

  The two supported degrees are distinct.

• outgoing (j : ℤ) : self.K.d self.b j = 0

  All differentials out of the high term vanish.

• support (j : ℤ) : j ≠ self.a → j ≠ self.b → CategoryTheory.Limits.IsZero (self.K.X j)

  Every other term is zero.

theorem TauCeti.TwoTermSupport.incoming {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] (s : TwoTermSupport C₁) (j : ℤ) : s.K.d j s.a = 0

All differentials into the low term vanish: a differential into the low term starts at the high term, where every differential vanishes, or at a zero term.

noncomputable def TauCeti.TwoTermSupport.ι {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : (HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B ⟶ s.K

The supported high term includes as a single-row subcomplex.

noncomputable def TauCeti.TwoTermSupport.π {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : s.K ⟶ (HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A

The supported low term is the single-row quotient complex.

@[simp]

theorem TauCeti.TwoTermSupport.ι_f {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : s.ι.f s.b = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) s.b s.B).hom s.high.inv

The high-row inclusion is the supplied high-term identification at its supported degree.

theorem TauCeti.TwoTermSupport.ι_f_assoc {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) {Z : C₁} (h : s.K.X s.b ⟶ Z) : CategoryTheory.CategoryStruct.comp (s.ι.f s.b) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) s.b s.B).hom (CategoryTheory.CategoryStruct.comp s.high.inv h)

The high-row inclusion is the supplied high-term identification at its supported degree.

@[simp]

theorem TauCeti.TwoTermSupport.π_f {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : s.π.f s.a = CategoryTheory.CategoryStruct.comp s.low.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) s.a s.A).inv

The low-row projection is the supplied low-term identification at its supported degree.

theorem TauCeti.TwoTermSupport.π_f_assoc {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) {Z : C₁} (h : ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).X s.a ⟶ Z) : CategoryTheory.CategoryStruct.comp (s.π.f s.a) h = CategoryTheory.CategoryStruct.comp s.low.hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) s.a s.A).inv h)

The low-row projection is the supplied low-term identification at its supported degree.

noncomputable def TauCeti.TwoTermSupport.shortComplex {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : CategoryTheory.ShortComplex (CochainComplex C₁ ℤ)

The high-row inclusion and low-row projection form a short complex.

@[simp]

theorem TauCeti.TwoTermSupport.shortComplex_X₁ {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : s.shortComplex.X₁ = (HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B

@[simp]

theorem TauCeti.TwoTermSupport.shortComplex_X₂ {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : s.shortComplex.X₂ = s.K

@[simp]

theorem TauCeti.TwoTermSupport.shortComplex_X₃ {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : s.shortComplex.X₃ = (HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A

@[simp]

theorem TauCeti.TwoTermSupport.shortComplex_f {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : CategoryTheory.CategoryStruct.comp s.shortComplex.f (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) s.ι

After identifying the endpoints, the support short-complex inclusion is the high map.

@[simp]

theorem TauCeti.TwoTermSupport.shortComplex_f_assoc {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) {Z : CochainComplex C₁ ℤ} (h : s.K ⟶ Z) : CategoryTheory.CategoryStruct.comp s.shortComplex.f (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp s.ι h)

After identifying the endpoints, the support short-complex inclusion is the high map.

@[simp]

theorem TauCeti.TwoTermSupport.shortComplex_g {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) : CategoryTheory.CategoryStruct.comp s.shortComplex.g (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) s.π

After identifying the endpoints, the support short-complex projection is the low map.

@[simp]

theorem TauCeti.TwoTermSupport.shortComplex_g_assoc {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroObject C₁] (s : TwoTermSupport C₁) {Z : CochainComplex C₁ ℤ} (h : (HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A ⟶ Z) : CategoryTheory.CategoryStruct.comp s.shortComplex.g (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp s.π h)

After identifying the endpoints, the support short-complex projection is the low map.

noncomputable def CategoryTheory.Functor.mapBifunctorSingleRowNatIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) (a : ℤ) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A) ≅ ((F.obj A).mapHomologicalComplex (ComplexShape.up ℤ)).comp (shiftFunctor (CochainComplex D ℤ) (-a))

Totalization against a single supported row is the corresponding shifted row functor.

noncomputable def CategoryTheory.Functor.mapBifunctorSingleRowZeroNatIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A) ≅ (F.obj A).mapHomologicalComplex (ComplexShape.up ℤ)

A row supported in cochain degree zero has the unshifted row functor.

@[simp]

theorem CategoryTheory.Functor.mapBifunctorSingleRowNatIso_inv_app_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) (a : ℤ) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) : ((F.mapBifunctorSingleRowNatIso A a).inv.app N).f j = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) a A).inv).app (N.X (j + -a))) (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) a (j + -a) j ⋯)

The inverse row comparison includes its supported totalization summand.

theorem CategoryTheory.Functor.mapBifunctorSingleRowNatIso_inv_app_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) (a : ℤ) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) {Z : D} (h : (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).mapBifunctor N F (ComplexShape.up ℤ)).X j ⟶ Z) : CategoryStruct.comp (((F.mapBifunctorSingleRowNatIso A a).inv.app N).f j) h = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) a A).inv).app (N.X (j + -a))) (CategoryStruct.comp (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) a (j + -a) j ⋯) h)

The inverse row comparison includes its supported totalization summand.

@[simp]

theorem CategoryTheory.Functor.ι_mapBifunctorSingleRowNatIso_hom_app_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) (a : ℤ) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) : CategoryStruct.comp (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) a (j + -a) j ⋯) (((F.mapBifunctorSingleRowNatIso A a).hom.app N).f j) = (F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) a A).hom).app (N.X (j + -a))

The row comparison sends the supported inclusion to the row-object identification.

@[simp]

theorem CategoryTheory.Functor.ι_mapBifunctorSingleRowNatIso_hom_app_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) (a : ℤ) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) {Z : D} (h : ((F.obj A).mapHomologicalComplex (ComplexShape.up ℤ)).obj N⟦-a⟧.X j ⟶ Z) : CategoryStruct.comp (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) a).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) a (j + -a) j ⋯) (CategoryStruct.comp (((F.mapBifunctorSingleRowNatIso A a).hom.app N).f j) h) = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) a A).hom).app (N.X (j + -a))) h

The row comparison sends the supported inclusion to the row-object identification.

@[simp]

theorem CategoryTheory.Functor.mapBifunctorSingleRowZeroNatIso_inv_app_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) : ((F.mapBifunctorSingleRowZeroNatIso A).inv.app N).f j = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 A).inv).app (N.X j)) (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) 0 j j ⋯)

The inverse degree-zero comparison includes the unshifted supported summand.

theorem CategoryTheory.Functor.mapBifunctorSingleRowZeroNatIso_inv_app_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) {Z : D} (h : (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).mapBifunctor N F (ComplexShape.up ℤ)).X j ⟶ Z) : CategoryStruct.comp (((F.mapBifunctorSingleRowZeroNatIso A).inv.app N).f j) h = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 A).inv).app (N.X j)) (CategoryStruct.comp (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) 0 j j ⋯) h)

The inverse degree-zero comparison includes the unshifted supported summand.

@[simp]

theorem CategoryTheory.Functor.ι_mapBifunctorSingleRowZeroNatIso_hom_app_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) : CategoryStruct.comp (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) 0 j j ⋯) (((F.mapBifunctorSingleRowZeroNatIso A).hom.app N).f j) = (F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 A).hom).app (N.X j)

The degree-zero comparison sends its inclusion to the unshifted row identification.

@[simp]

theorem CategoryTheory.Functor.ι_mapBifunctorSingleRowZeroNatIso_hom_app_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (A : C₁) [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).HasMapBifunctor N F (ComplexShape.up ℤ)] (N : CochainComplex C₂ ℤ) (j : ℤ) {Z : D} (h : (((F.obj A).mapHomologicalComplex (ComplexShape.up ℤ)).obj N).X j ⟶ Z) : CategoryStruct.comp (((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj A).ιMapBifunctor N F (ComplexShape.up ℤ) 0 j j ⋯) (CategoryStruct.comp (((F.mapBifunctorSingleRowZeroNatIso A).hom.app N).f j) h) = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 A).hom).app (N.X j)) h

The degree-zero comparison sends its inclusion to the unshifted row identification.

noncomputable def CategoryTheory.Functor.mapTwoTermSupport {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] : ShortComplex (Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ))

Apply totalization to the supported short complex, using only its three left complexes.

noncomputable def CategoryTheory.Functor.mapTwoTermSupportDegreewiseIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] (N : CochainComplex C₂ ℤ) (j : ℤ) : ((F.mapTwoTermSupport s).map ((evaluation (CochainComplex C₂ ℤ) (CochainComplex D ℤ)).obj N)).map (HomologicalComplex.eval D (ComplexShape.up ℤ) j) ≅ { X₁ := (F.obj s.B).obj (N.X (j + -s.b)), X₂ := (F.obj s.B).obj (N.X (j + -s.b)) ⊞ (F.obj s.A).obj (N.X (j + -s.a)), X₃ := (F.obj s.A).obj (N.X (j + -s.a)), f := Limits.biprod.inl, g := Limits.biprod.snd, zero := ⋯ }

In each cochain degree the mapped support sequence is the canonical biproduct sequence.

noncomputable def CategoryTheory.Functor.mapTwoTermSupportDegreewiseSplitting {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] (N : CochainComplex C₂ ℤ) (j : ℤ) : (((F.mapTwoTermSupport s).map ((evaluation (CochainComplex C₂ ℤ) (CochainComplex D ℤ)).obj N)).map (HomologicalComplex.eval D (ComplexShape.up ℤ) j)).Splitting

The mapped support sequence has its canonical splitting in each cochain degree.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupport_X₁ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] : (F.mapTwoTermSupport s).X₁ = F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B)

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupport_X₂ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] : (F.mapTwoTermSupport s).X₂ = F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.K

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupport_X₃ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] : (F.mapTwoTermSupport s).X₃ = F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A)

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupport_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] : CategoryStruct.comp (F.mapTwoTermSupport s).f (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.ι)

The mapped support inclusion is the totalization of the supplied high-row map.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupport_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {Z : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (h : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.K ⟶ Z) : CategoryStruct.comp (F.mapTwoTermSupport s).f (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.ι) h)

The mapped support inclusion is the totalization of the supplied high-row map.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupport_g {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] : CategoryStruct.comp (F.mapTwoTermSupport s).g (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.π)

The mapped support projection is the totalization of the supplied low-row map.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupport_g_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {Z : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (h : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ⟶ Z) : CategoryStruct.comp (F.mapTwoTermSupport s).g (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.π) h)

The mapped support projection is the totalization of the supplied low-row map.

noncomputable def CategoryTheory.Functor.mapTwoTermSupportReframed {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : ShortComplex (Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ))

Replace the two endpoint functors using specified natural isomorphisms.

noncomputable def CategoryTheory.Functor.mapTwoTermSupportReframedIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : F.mapTwoTermSupport s ≅ F.mapTwoTermSupportReframed s u₁ u₃

The endpoint replacement is isomorphic to the mapped support short complex.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_X₁ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : (F.mapTwoTermSupportReframed s u₁ u₃).X₁ = E₁

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_X₂ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : (F.mapTwoTermSupportReframed s u₁ u₃).X₂ = F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.K

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_X₃ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : (F.mapTwoTermSupportReframed s u₁ u₃).X₃ = E₃

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_f {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : CategoryStruct.comp (F.mapTwoTermSupportReframed s u₁ u₃).f (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp u₁.inv (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.ι))

The reframed inclusion is the high-row totalization precomposed with its endpoint change.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_f_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) {Z : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (h : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.K ⟶ Z) : CategoryStruct.comp (F.mapTwoTermSupportReframed s u₁ u₃).f (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp u₁.inv (CategoryStruct.comp (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.ι) h))

The reframed inclusion is the high-row totalization precomposed with its endpoint change.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_g {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : CategoryStruct.comp (F.mapTwoTermSupportReframed s u₁ u₃).g (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.π) u₃.hom)

The reframed projection is the low-row totalization followed by its endpoint change.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_g_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) {Z : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (h : E₃ ⟶ Z) : CategoryStruct.comp (F.mapTwoTermSupportReframed s u₁ u₃).g (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (F.mapBifunctorLeftMap (ComplexShape.up ℤ) (ComplexShape.up ℤ) s.π) (CategoryStruct.comp u₃.hom h))

The reframed projection is the low-row totalization followed by its endpoint change.

noncomputable def CategoryTheory.Functor.mapTwoTermSupportReframedDegreewiseSplitting {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) (N : CochainComplex C₂ ℤ) (j : ℤ) : (((F.mapTwoTermSupportReframed s u₁ u₃).map ((evaluation (CochainComplex C₂ ℤ) (CochainComplex D ℤ)).obj N)).map (HomologicalComplex.eval D (ComplexShape.up ℤ) j)).Splitting

Transport the canonical degreewise splitting through the endpoint-change isomorphism.

noncomputable def CategoryTheory.Functor.mapTwoTermSupportReframedDegreewiseIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) (N : CochainComplex C₂ ℤ) (j : ℤ) : ((F.mapTwoTermSupportReframed s u₁ u₃).X₂.obj N).X j ≅ ((F.mapTwoTermSupportReframed s u₁ u₃).X₁.obj N).X j ⊞ ((F.mapTwoTermSupportReframed s u₁ u₃).X₃.obj N).X j

The reframed totalization term is the biproduct of its two public endpoint terms.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_f_degreewiseIso_hom {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) (N : CochainComplex C₂ ℤ) (j : ℤ) : CategoryStruct.comp (((F.mapTwoTermSupportReframed s u₁ u₃).f.app N).f j) (F.mapTwoTermSupportReframedDegreewiseIso s u₁ u₃ N j).hom = Limits.biprod.inl

The reframed inclusion is the first inclusion under its degreewise comparison.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_f_degreewiseIso_hom_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) (N : CochainComplex C₂ ℤ) (j : ℤ) {Z : D} (h : ((F.mapTwoTermSupportReframed s u₁ u₃).X₁.obj N).X j ⊞ ((F.mapTwoTermSupportReframed s u₁ u₃).X₃.obj N).X j ⟶ Z) : CategoryStruct.comp (((F.mapTwoTermSupportReframed s u₁ u₃).f.app N).f j) (CategoryStruct.comp (F.mapTwoTermSupportReframedDegreewiseIso s u₁ u₃ N j).hom h) = CategoryStruct.comp Limits.biprod.inl h

The reframed inclusion is the first inclusion under its degreewise comparison.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_degreewiseIso_hom_snd {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) (N : CochainComplex C₂ ℤ) (j : ℤ) : CategoryStruct.comp (F.mapTwoTermSupportReframedDegreewiseIso s u₁ u₃ N j).hom Limits.biprod.snd = ((F.mapTwoTermSupportReframed s u₁ u₃).g.app N).f j

The reframed projection is the second projection under its degreewise comparison.

@[simp]

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_degreewiseIso_hom_snd_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroMorphisms C₂] [Preadditive D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] [Limits.HasZeroObject C₁] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] [Limits.HasBinaryBiproducts D] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) (N : CochainComplex C₂ ℤ) (j : ℤ) {Z : D} (h : ((F.mapTwoTermSupportReframed s u₁ u₃).X₃.obj N).X j ⟶ Z) : CategoryStruct.comp (F.mapTwoTermSupportReframedDegreewiseIso s u₁ u₃ N j).hom (CategoryStruct.comp Limits.biprod.snd h) = CategoryStruct.comp (((F.mapTwoTermSupportReframed s u₁ u₃).g.app N).f j) h

The reframed projection is the second projection under its degreewise comparison.

theorem CategoryTheory.Functor.mapTwoTermSupport_shortExact {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroObject C₁] [Limits.HasZeroMorphisms C₂] [Abelian D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] : (F.mapTwoTermSupport s).ShortExact

The mapped support short complex is short exact in the functor category.

theorem CategoryTheory.Functor.mapTwoTermSupportReframed_shortExact {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} D] [Limits.HasZeroMorphisms C₁] [Limits.HasZeroObject C₁] [Limits.HasZeroMorphisms C₂] [Abelian D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (A : C₁), (F.obj A).PreservesZeroMorphisms] (s : TauCeti.TwoTermSupport C₁) [∀ (N : CochainComplex C₂ ℤ), HomologicalComplex.HasMapBifunctor s.K N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B).HasMapBifunctor N F (ComplexShape.up ℤ)] [∀ (N : CochainComplex C₂ ℤ), ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A).HasMapBifunctor N F (ComplexShape.up ℤ)] {E₁ E₃ : Functor (CochainComplex C₂ ℤ) (CochainComplex D ℤ)} (u₁ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.b).obj s.B) ≅ E₁) (u₃ : F.mapBifunctorLeft (ComplexShape.up ℤ) (ComplexShape.up ℤ) ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) s.a).obj s.A) ≅ E₃) : (F.mapTwoTermSupportReframed s u₁ u₃).ShortExact

The endpoint replacement of the mapped support short complex is short exact.