Finite-support bifunctor maps and colimits of complex totals

Mathlib's HomologicalComplex.mapBifunctorMap is a map between direct-sum totals. When the fixed input complex has finitely supported terms, a columnwise quasi-isomorphism criterion for literal bicomplex totals applies to this map. For arbitrary compatible complex shapes, the literal total preserves a diagram-shape colimit in either varying slot when the corresponding partial bifunctor preserves it at the fixed complex's terms.

Main definitions

This module introduces no new public definitions; it studies Mathlib's existing HomologicalComplex.mapBifunctorMap, CategoryTheory.Functor.map₂HomologicalComplex, and its cochain specialization CategoryTheory.Functor.map₂CochainComplex.

Main results

• HomologicalComplex.quasiIso_mapBifunctorMap_id_left_of_finite_support_of_column_quasiIso passes quasi-isomorphic mapped columns in the second input to a quasi-isomorphism of literal totals under finite term support in the first.
• HomologicalComplex.quasiIso_mapBifunctorMap_id_right_of_finite_support_of_column_quasiIso fixes finite support in the second input and maps the first by signed flip.
• CategoryTheory.Functor.preservesColimitsOfShape_map₂HomologicalComplex_obj and CategoryTheory.Functor.preservesColimitsOfShape_map₂HomologicalComplex_flip_obj preserve a colimit in either varying slot for arbitrary compatible shapes.
• CategoryTheory.Functor.preservesColimitsOfShape_map₂CochainComplex_obj and CategoryTheory.Functor.preservesColimitsOfShape_map₂CochainComplex_flip_obj specialize these results to integer cochain totals.

Implementation notes

The fixed complex supplies the finite horizontal support strip for both bicomplexes. The finite-strip total-map criterion needs columnwise evidence only inside it; the right-slot result uses naturality of Mathlib's signed flip. For colimits, two evaluations reduce the mapped bicomplex to the partial base functor at each bidegree. The existing total-functor colimit theorem then applies under coproducts over each total-degree fiber; private natural isomorphisms identify its composite with Mathlib's literal map₂ functor in each slot. Countable coproducts suffice for the integer cochain case.

References

These results extend Mathlib's HomologicalComplex.mapBifunctorMap and use HomologicalComplex₂.totalMap_quasiIso_of_finiteStrip. The colimit results use HomologicalComplex₂.totalFunctor_preservesColimitsOfShape.

Tags

bifunctor, homological complex, cochain complex, quasi-isomorphism, finite support, colimit

theorem HomologicalComplex.quasiIso_mapBifunctorMap_id_left_of_finite_support_of_column_quasiIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X : C₁), (F.obj X).PreservesZeroMorphisms] (K : CochainComplex C₁ ℤ) {L M : CochainComplex C₂ ℤ} (f : L ⟶ M) [HasMapBifunctor K L F (ComplexShape.up ℤ)] [HasMapBifunctor K M F (ComplexShape.up ℤ)] (a b : ℤ) (hLower : ∀ p < a, CategoryTheory.Limits.IsZero (K.X p)) (hUpper : ∀ (p : ℤ), b < p → CategoryTheory.Limits.IsZero (K.X p)) (hcol : ∀ (p : ℤ), a ≤ p → p ≤ b → QuasiIso (((F.obj (K.X p)).mapHomologicalComplex (ComplexShape.up ℤ)).map f)) : QuasiIso (mapBifunctorMap (CategoryTheory.CategoryStruct.id K) f F (ComplexShape.up ℤ))

Finite term support in the first complex lets columnwise quasi-isomorphisms pass through Mathlib's literal bifunctor total map. Only columns within the support interval need quasi-isomorphism evidence. The second map is unrestricted; the bounds concern terms, not cohomology.

theorem HomologicalComplex.quasiIso_mapBifunctorMap_id_right_of_finite_support_of_column_quasiIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X : C₁), (F.obj X).PreservesZeroMorphisms] (K : CochainComplex C₂ ℤ) {L M : CochainComplex C₁ ℤ} (f : L ⟶ M) [HasMapBifunctor L K F (ComplexShape.up ℤ)] [HasMapBifunctor M K F (ComplexShape.up ℤ)] (a b : ℤ) (hLower : ∀ p < a, CategoryTheory.Limits.IsZero (K.X p)) (hUpper : ∀ (p : ℤ), b < p → CategoryTheory.Limits.IsZero (K.X p)) (hcol : ∀ (p : ℤ), a ≤ p → p ≤ b → QuasiIso (((F.flip.obj (K.X p)).mapHomologicalComplex (ComplexShape.up ℤ)).map f)) : QuasiIso (mapBifunctorMap f (CategoryTheory.CategoryStruct.id K) F (ComplexShape.up ℤ))

Signed flipping turns finite term support in the second complex into the left-slot criterion, without a symmetric monoidal structure. Only supported columns need quasi-isomorphism evidence.

theorem CategoryTheory.Functor.preservesColimitsOfShape_map₂HomologicalComplex_obj {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Limits.HasZeroMorphisms C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] [Limits.HasZeroMorphisms C₂] {D : Type u₃} [Category.{v₃, u₃} D] [Preadditive D] {J : Type w} [Category.{z, w} J] [Limits.HasColimitsOfShape J C₂] [Limits.HasColimitsOfShape J D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X : C₁), (F.obj X).PreservesZeroMorphisms] {I₁ : Type a} {I₂ : Type b} {I₁₂ : Type d} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [∀ (n : I₁₂), Limits.HasCoproductsOfShape (↑(c₁.π c₂ c₁₂ ⁻¹' {n})) D] (K : HomologicalComplex C₁ c₁) [∀ (p : I₁), Limits.PreservesColimitsOfShape J (F.obj (K.X p))] : Limits.PreservesColimitsOfShape J ((F.map₂HomologicalComplex c₁ c₂ c₁₂).obj K)

For any compatible complex shapes, fixing the first complex preserves J-colimits of the literal bifunctor total when the partial functor at each term of that complex does. The total functor uses the stated coproducts over its degree fibers; no homology exactness is required.

theorem CategoryTheory.Functor.preservesColimitsOfShape_map₂HomologicalComplex_flip_obj {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Limits.HasZeroMorphisms C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] [Limits.HasZeroMorphisms C₂] {D : Type u₃} [Category.{v₃, u₃} D] [Preadditive D] {J : Type w} [Category.{z, w} J] [Limits.HasColimitsOfShape J C₁] [Limits.HasColimitsOfShape J D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X : C₁), (F.obj X).PreservesZeroMorphisms] {I₁ : Type a} {I₂ : Type b} {I₁₂ : Type d} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [∀ (n : I₁₂), Limits.HasCoproductsOfShape (↑(c₁.π c₂ c₁₂ ⁻¹' {n})) D] (K : HomologicalComplex C₂ c₂) [∀ (q : I₂), Limits.PreservesColimitsOfShape J (F.flip.obj (K.X q))] : Limits.PreservesColimitsOfShape J ((F.map₂HomologicalComplex c₁ c₂ c₁₂).flip.obj K)

Fixing the second complex preserves J-colimits of the literal total when each partial functor at its terms does. The proof keeps the original bidegree order, evaluates twice, and transports through direct-sum totalization.

theorem CategoryTheory.Functor.preservesColimitsOfShape_map₂CochainComplex_obj {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Limits.HasZeroMorphisms C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] [Limits.HasZeroMorphisms C₂] {D : Type u₃} [Category.{v₃, u₃} D] [Preadditive D] [Limits.HasCountableCoproducts D] {J : Type w} [Category.{z, w} J] [Limits.HasColimitsOfShape J C₂] [Limits.HasColimitsOfShape J D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X : C₁), (F.obj X).PreservesZeroMorphisms] (K : CochainComplex C₁ ℤ) [∀ (p : ℤ), Limits.PreservesColimitsOfShape J (F.obj (K.X p))] : Limits.PreservesColimitsOfShape J (F.map₂CochainComplex.obj K)

The cochain specialization of CategoryTheory.Functor.preservesColimitsOfShape_map₂HomologicalComplex_obj. Countable coproducts supply every integer-diagonal total.

theorem CategoryTheory.Functor.preservesColimitsOfShape_map₂CochainComplex_flip_obj {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Limits.HasZeroMorphisms C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] [Limits.HasZeroMorphisms C₂] {D : Type u₃} [Category.{v₃, u₃} D] [Preadditive D] [Limits.HasCountableCoproducts D] {J : Type w} [Category.{z, w} J] [Limits.HasColimitsOfShape J C₁] [Limits.HasColimitsOfShape J D] (F : Functor C₁ (Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X : C₁), (F.obj X).PreservesZeroMorphisms] (K : CochainComplex C₂ ℤ) [∀ (q : ℤ), Limits.PreservesColimitsOfShape J (F.flip.obj (K.X q))] : Limits.PreservesColimitsOfShape J (F.map₂CochainComplex.flip.obj K)

The fixed-second cochain specialization retains the original bicomplex degree order and uses countable coproducts for each total diagonal.