Supported summands of a bifunctor totalization #
A term of Mathlib's bifunctor totalization is the coproduct of its summands over the fiber of the total index map. When all but one or two summands are zero, the term identifies with the remaining summand or their binary biproduct. The comparisons below use the existing totalization inclusions and desc maps. Their characteristic equations compute the supported inclusions and the inverse maps.
noncomputable def
HomologicalComplex.mapBifunctorSingleSummandIso
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(j : J)
(h : c₁.π c₂ c (p₀, q₀) = j)
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j → ¬(p = p₀ ∧ q = q₀) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
:
A totalization term with only one potentially nonzero summand is that summand.
Instances For
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorSingleSummandIso_hom
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(j : J)
(h : c₁.π c₂ c (p₀, q₀) = j)
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j → ¬(p = p₀ ∧ q = q₀) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c p₀ q₀ j h)
(K₁.mapBifunctorSingleSummandIso K₂ F c p₀ q₀ j h hzero).hom = CategoryTheory.CategoryStruct.id ((F.obj (K₁.X p₀)).obj (K₂.X q₀))
The unique supported inclusion is the inverse of the single-summand comparison.
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorSingleSummandIso_hom_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(j : J)
(h : c₁.π c₂ c (p₀, q₀) = j)
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j → ¬(p = p₀ ∧ q = q₀) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
{Z : D}
(h✝ : (F.obj (K₁.X p₀)).obj (K₂.X q₀) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c p₀ q₀ j h)
(CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorSingleSummandIso K₂ F c p₀ q₀ j h hzero).hom h✝) = h✝
The unique supported inclusion is the inverse of the single-summand comparison.
@[simp]
theorem
HomologicalComplex.mapBifunctorSingleSummandIso_inv
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(j : J)
(h : c₁.π c₂ c (p₀, q₀) = j)
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j → ¬(p = p₀ ∧ q = q₀) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
:
The inverse of the single-summand comparison is the totalization inclusion.
noncomputable def
HomologicalComplex.mapBifunctorTwoSummandIso
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(p₁ : I₁)
(q₁ : I₂)
(j : J)
[CategoryTheory.Limits.HasBinaryBiproduct ((F.obj (K₁.X p₀)).obj (K₂.X q₀)) ((F.obj (K₁.X p₁)).obj (K₂.X q₁))]
(h₀ : c₁.π c₂ c (p₀, q₀) = j)
(h₁ : c₁.π c₂ c (p₁, q₁) = j)
(hne : (p₁, q₁) ≠ (p₀, q₀))
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j →
¬(p = p₀ ∧ q = q₀ ∨ p = p₁ ∧ q = q₁) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
:
A totalization term with two potentially nonzero summands is their binary biproduct.
Instances For
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorTwoSummandIso_hom_left
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(p₁ : I₁)
(q₁ : I₂)
(j : J)
[CategoryTheory.Limits.HasBinaryBiproduct ((F.obj (K₁.X p₀)).obj (K₂.X q₀)) ((F.obj (K₁.X p₁)).obj (K₂.X q₁))]
(h₀ : c₁.π c₂ c (p₀, q₀) = j)
(h₁ : c₁.π c₂ c (p₁, q₁) = j)
(hne : (p₁, q₁) ≠ (p₀, q₀))
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j →
¬(p = p₀ ∧ q = q₀ ∨ p = p₁ ∧ q = q₁) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c p₀ q₀ j h₀)
(K₁.mapBifunctorTwoSummandIso K₂ F c p₀ q₀ p₁ q₁ j h₀ h₁ hne hzero).hom = CategoryTheory.Limits.biprod.inl
The first supported inclusion computes as the first biproduct inclusion.
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorTwoSummandIso_hom_left_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(p₁ : I₁)
(q₁ : I₂)
(j : J)
[CategoryTheory.Limits.HasBinaryBiproduct ((F.obj (K₁.X p₀)).obj (K₂.X q₀)) ((F.obj (K₁.X p₁)).obj (K₂.X q₁))]
(h₀ : c₁.π c₂ c (p₀, q₀) = j)
(h₁ : c₁.π c₂ c (p₁, q₁) = j)
(hne : (p₁, q₁) ≠ (p₀, q₀))
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j →
¬(p = p₀ ∧ q = q₀ ∨ p = p₁ ∧ q = q₁) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
{Z : D}
(h : (F.obj (K₁.X p₀)).obj (K₂.X q₀) ⊞ (F.obj (K₁.X p₁)).obj (K₂.X q₁) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c p₀ q₀ j h₀)
(CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorTwoSummandIso K₂ F c p₀ q₀ p₁ q₁ j h₀ h₁ hne hzero).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
The first supported inclusion computes as the first biproduct inclusion.
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorTwoSummandIso_hom_right
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(p₁ : I₁)
(q₁ : I₂)
(j : J)
[CategoryTheory.Limits.HasBinaryBiproduct ((F.obj (K₁.X p₀)).obj (K₂.X q₀)) ((F.obj (K₁.X p₁)).obj (K₂.X q₁))]
(h₀ : c₁.π c₂ c (p₀, q₀) = j)
(h₁ : c₁.π c₂ c (p₁, q₁) = j)
(hne : (p₁, q₁) ≠ (p₀, q₀))
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j →
¬(p = p₀ ∧ q = q₀ ∨ p = p₁ ∧ q = q₁) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c p₁ q₁ j h₁)
(K₁.mapBifunctorTwoSummandIso K₂ F c p₀ q₀ p₁ q₁ j h₀ h₁ hne hzero).hom = CategoryTheory.Limits.biprod.inr
The second supported inclusion computes as the second biproduct inclusion.
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorTwoSummandIso_hom_right_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(p₁ : I₁)
(q₁ : I₂)
(j : J)
[CategoryTheory.Limits.HasBinaryBiproduct ((F.obj (K₁.X p₀)).obj (K₂.X q₀)) ((F.obj (K₁.X p₁)).obj (K₂.X q₁))]
(h₀ : c₁.π c₂ c (p₀, q₀) = j)
(h₁ : c₁.π c₂ c (p₁, q₁) = j)
(hne : (p₁, q₁) ≠ (p₀, q₀))
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j →
¬(p = p₀ ∧ q = q₀ ∨ p = p₁ ∧ q = q₁) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
{Z : D}
(h : (F.obj (K₁.X p₀)).obj (K₂.X q₀) ⊞ (F.obj (K₁.X p₁)).obj (K₂.X q₁) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c p₁ q₁ j h₁)
(CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorTwoSummandIso K₂ F c p₀ q₀ p₁ q₁ j h₀ h₁ hne hzero).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
The second supported inclusion computes as the second biproduct inclusion.
@[simp]
theorem
HomologicalComplex.mapBifunctorTwoSummandIso_inv
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[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.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(p₀ : I₁)
(q₀ : I₂)
(p₁ : I₁)
(q₁ : I₂)
(j : J)
[CategoryTheory.Limits.HasBinaryBiproduct ((F.obj (K₁.X p₀)).obj (K₂.X q₀)) ((F.obj (K₁.X p₁)).obj (K₂.X q₁))]
(h₀ : c₁.π c₂ c (p₀, q₀) = j)
(h₁ : c₁.π c₂ c (p₁, q₁) = j)
(hne : (p₁, q₁) ≠ (p₀, q₀))
(hzero :
∀ (p : I₁) (q : I₂),
c₁.π c₂ c (p, q) = j →
¬(p = p₀ ∧ q = q₀ ∨ p = p₁ ∧ q = q₁) → CategoryTheory.Limits.IsZero ((F.obj (K₁.X p)).obj (K₂.X q)))
:
(K₁.mapBifunctorTwoSummandIso K₂ F c p₀ q₀ p₁ q₁ j h₀ h₁ hne hzero).inv = CategoryTheory.Limits.biprod.desc (K₁.ιMapBifunctor K₂ F c p₀ q₀ j h₀) (K₁.ιMapBifunctor K₂ F c p₁ q₁ j h₁)
The inverse two-summand comparison is the desc map of the supported inclusions.