The total complex of a bicomplex #
Given a preadditive category C, two complex shapes c₁ : ComplexShape I₁,
c₂ : ComplexShape I₂, a bicomplex K : HomologicalComplex₂ C c₁ c₂,
and a third complex shape c₁₂ : ComplexShape I₁₂ equipped
with [TotalComplexShape c₁ c₂ c₁₂], we construct the total complex
K.total c₁₂ : HomologicalComplex C c₁₂.
In particular, if c := ComplexShape.up ℤ and K : HomologicalComplex₂ c c, then for any
n : ℤ, (K.total c).X n identifies to the coproduct of the (K.X p).X q such that
p + q = n, and the differential on (K.total c).X n is induced by the sum of horizontal
differentials (K.X p).X q ⟶ (K.X (p + 1)).X q and (-1) ^ p times the vertical
differentials (K.X p).X q ⟶ (K.X p).X (q + 1).
@[reducible, inline]
abbrev
HomologicalComplex₂.HasTotal
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
:
A bicomplex has a total bicomplex if for any i₁₂ : I₁₂, the coproduct
of the objects (K.X i₁).X i₂ such that ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂ exists.
Equations
Instances For
theorem
HomologicalComplex₂.hasTotal_of_iso
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(e : K ≅ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[K.HasTotal c₁₂]
:
L.HasTotal c₁₂
noncomputable def
HomologicalComplex₂.d₁
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
:
The horizontal differential in the total complex on a given summand.
Equations
Instances For
noncomputable def
HomologicalComplex₂.d₂
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
:
The vertical differential in the total complex on a given summand.
Equations
Instances For
theorem
HomologicalComplex₂.d₁_eq_zero
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
(h : ¬c₁.Rel i₁ (c₁.next i₁))
:
theorem
HomologicalComplex₂.d₂_eq_zero
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
(h : ¬c₂.Rel i₂ (c₂.next i₂))
:
Lemmas in the totalAux namespace should be used only in the internals of
the construction of the total complex HomologicalComplex₂.total. Once that
definition is done, similar lemmas shall be restated, but with
terms like K.toGradedObject.ιMapObj replaced by K.ιTotal. This is done in order
to prevent API leakage from definitions involving graded objects.
theorem
HomologicalComplex₂.totalAux.d₁_eq'
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(i₁₂ : I₁₂)
:
theorem
HomologicalComplex₂.totalAux.d₁_eq
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(i₁₂ : I₁₂)
(h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂)
:
theorem
HomologicalComplex₂.totalAux.d₂_eq'
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(i₁₂ : I₁₂)
:
theorem
HomologicalComplex₂.totalAux.d₂_eq
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(i₁₂ : I₁₂)
(h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂)
:
theorem
HomologicalComplex₂.d₁_eq_zero'
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(i₁₂ : I₁₂)
(h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂)
:
theorem
HomologicalComplex₂.d₂_eq_zero'
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(i₁₂ : I₁₂)
(h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂)
:
noncomputable def
HomologicalComplex₂.D₁
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
:
The horizontal differential in the total complex.
Equations
Instances For
noncomputable def
HomologicalComplex₂.D₂
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
:
The vertical differential in the total complex.
Equations
Instances For
@[simp]
theorem
HomologicalComplex₂.totalAux.ιMapObj_D₁
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i : I₁ × I₂)
(h : c₁.π c₂ c₁₂ i = i₁₂)
:
CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') = K.d₁ c₁₂ i.1 i.2 i₁₂'
@[simp]
theorem
HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i : I₁ × I₂)
(h : c₁.π c₂ c₁₂ i = i₁₂)
{Z : C}
(h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h)
(CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i.1 i.2 i₁₂') h✝
@[simp]
theorem
HomologicalComplex₂.totalAux.ιMapObj_D₂
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i : I₁ × I₂)
(h : c₁.π c₂ c₁₂ i = i₁₂)
:
CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') = K.d₂ c₁₂ i.1 i.2 i₁₂'
@[simp]
theorem
HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i : I₁ × I₂)
(h : c₁.π c₂ c₁₂ i = i₁₂)
{Z : C}
(h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h)
(CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i.1 i.2 i₁₂') h✝
theorem
HomologicalComplex₂.D₁_shape
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂')
:
theorem
HomologicalComplex₂.D₂_shape
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂')
:
@[simp]
theorem
HomologicalComplex₂.D₁_D₁
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
:
@[simp]
theorem
HomologicalComplex₂.D₁_D₁_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
HomologicalComplex₂.D₂_D₂
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
:
@[simp]
theorem
HomologicalComplex₂.D₂_D₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
HomologicalComplex₂.D₂_D₁
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
:
CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'')
@[simp]
theorem
HomologicalComplex₂.D₂_D₁_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'')) h
theorem
HomologicalComplex₂.D₁_D₂
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
:
CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'')
theorem
HomologicalComplex₂.D₁_D₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' i₁₂'' : I₁₂)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'')) h
noncomputable def
HomologicalComplex₂.total
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
:
HomologicalComplex C c₁₂
The total complex of a bicomplex.
Equations
Instances For
theorem
HomologicalComplex₂.total_d
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
:
noncomputable def
HomologicalComplex₂.ιTotal
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
:
The inclusion of a summand in the total complex.
Equations
Instances For
@[simp]
theorem
HomologicalComplex₂.XXIsoOfEq_hom_ιTotal
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{x₁ y₁ : I₁}
(h₁ : x₁ = y₁)
{x₂ y₂ : I₂}
(h₂ : x₂ = y₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂)
:
@[simp]
theorem
HomologicalComplex₂.XXIsoOfEq_hom_ιTotal_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{x₁ y₁ : I₁}
(h₁ : x₁ = y₁)
{x₂ y₂ : I₂}
(h₂ : x₂ = y₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂)
{Z : C}
(h✝ : (K.total c₁₂).X i₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (XXIsoOfEq C c₁ c₂ K h₁ h₂).hom
(CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ y₁ y₂ i₁₂ h) h✝) = CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯) h✝
@[simp]
theorem
HomologicalComplex₂.XXIsoOfEq_inv_ιTotal
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{x₁ y₁ : I₁}
(h₁ : x₁ = y₁)
{x₂ y₂ : I₂}
(h₂ : x₂ = y₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂)
:
@[simp]
theorem
HomologicalComplex₂.XXIsoOfEq_inv_ιTotal_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{x₁ y₁ : I₁}
(h₁ : x₁ = y₁)
{x₂ y₂ : I₂}
(h₂ : x₂ = y₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂)
{Z : C}
(h✝ : (K.total c₁₂).X i₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (XXIsoOfEq C c₁ c₂ K h₁ h₂).inv
(CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ x₁ x₂ i₁₂ h) h✝) = CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯) h✝
noncomputable def
HomologicalComplex₂.ιTotalOrZero
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
:
The inclusion of a summand in the total complex, or zero if the degrees do not match.
Equations
Instances For
theorem
HomologicalComplex₂.ιTotalOrZero_eq
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
:
theorem
HomologicalComplex₂.ιTotalOrZero_eq_zero
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) ≠ i₁₂)
:
@[simp]
theorem
HomologicalComplex₂.ι_D₁
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') = K.d₁ c₁₂ i₁ i₂ i₁₂'
@[simp]
theorem
HomologicalComplex₂.ι_D₁_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
{Z : C}
(h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)
(CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂') h✝
@[simp]
theorem
HomologicalComplex₂.ι_D₂
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') = K.d₂ c₁₂ i₁ i₂ i₁₂'
@[simp]
theorem
HomologicalComplex₂.ι_D₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
{Z : C}
(h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)
(CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂') h✝
theorem
HomologicalComplex₂.d₁_eq'
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(i₁₂ : I₁₂)
:
theorem
HomologicalComplex₂.d₁_eq
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(i₁₂ : I₁₂)
(h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂)
:
theorem
HomologicalComplex₂.d₂_eq'
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(i₁₂ : I₁₂)
:
theorem
HomologicalComplex₂.d₂_eq
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(i₁₂ : I₁₂)
(h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂)
:
noncomputable def
HomologicalComplex₂.totalDesc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
{c₁₂ : ComplexShape I₁₂}
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{A : C}
{i₁₂ : I₁₂}
(f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A))
:
Given a bicomplex K, this is a constructor for morphisms from (K.total c₁₂).X i₁₂.
Equations
Instances For
@[simp]
theorem
HomologicalComplex₂.ι_totalDesc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
{c₁₂ : ComplexShape I₁₂}
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{A : C}
{i₁₂ : I₁₂}
(f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
:
@[simp]
theorem
HomologicalComplex₂.ι_totalDesc_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
{c₁₂ : ComplexShape I₁₂}
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{A : C}
{i₁₂ : I₁₂}
(f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
{Z : C}
(h : A ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) (CategoryTheory.CategoryStruct.comp (K.totalDesc f) h) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ hi) h
theorem
HomologicalComplex₂.total.hom_ext
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K : HomologicalComplex₂ C c₁ c₂}
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{A : C}
{i₁₂ : I₁₂}
{f g : (K.total c₁₂).X i₁₂ ⟶ A}
(h :
∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) f = CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) g)
:
theorem
HomologicalComplex₂.total.hom_ext_iff
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K : HomologicalComplex₂ C c₁ c₂}
{c₁₂ : ComplexShape I₁₂}
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
{A : C}
{i₁₂ : I₁₂}
{f g : (K.total c₁₂).X i₁₂ ⟶ A}
:
@[simp]
theorem
HomologicalComplex₂.total.mapAux.d₁_mapMap
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
:
CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂)
(CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₁ c₁₂ i₁ i₂ i₁₂)
@[simp]
theorem
HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
{Z : C}
(h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₁ c₁₂ i₁ i₂ i₁₂) h)
@[simp]
theorem
HomologicalComplex₂.total.mapAux.d₂_mapMap
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
:
CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂)
(CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₂ c₁₂ i₁ i₂ i₁₂)
@[simp]
theorem
HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
{Z : C}
(h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₂ c₁₂ i₁ i₂ i₁₂) h)
theorem
HomologicalComplex₂.total.mapAux.mapMap_D₁
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
(L.D₁ c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂')
(CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
theorem
HomologicalComplex₂.total.mapAux.mapMap_D₁_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
{Z : C}
(h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
(CategoryTheory.CategoryStruct.comp (L.D₁ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂')
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)
theorem
HomologicalComplex₂.total.mapAux.mapMap_D₂
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
(L.D₂ c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂')
(CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
theorem
HomologicalComplex₂.total.mapAux.mapMap_D₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁₂ i₁₂' : I₁₂)
{Z : C}
(h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
(CategoryTheory.CategoryStruct.comp (L.D₂ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂')
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)
noncomputable def
HomologicalComplex₂.total.map
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
:
The morphism K.total c₁₂ ⟶ L.total c₁₂ of homological complexes induced
by a morphism of bicomplexes K ⟶ L.
Equations
Instances For
@[simp]
theorem
HomologicalComplex₂.total.forget_map
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
:
(HomologicalComplex.forget C c₁₂).map (map φ c₁₂) = CategoryTheory.GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂)
@[simp]
theorem
HomologicalComplex₂.total.map_id
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
:
@[simp]
theorem
HomologicalComplex₂.total.map_comp
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L M : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(ψ : L ⟶ M)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
[M.HasTotal c₁₂]
:
map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂ = CategoryTheory.CategoryStruct.comp (map φ c₁₂) (map ψ c₁₂)
theorem
HomologicalComplex₂.total.map_comp_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L M : HomologicalComplex₂ C c₁ c₂}
(φ : K ⟶ L)
(ψ : L ⟶ M)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
[M.HasTotal c₁₂]
{Z : HomologicalComplex C c₁₂}
(h : M.total c₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂) h = CategoryTheory.CategoryStruct.comp (map φ c₁₂) (CategoryTheory.CategoryStruct.comp (map ψ c₁₂) h)
noncomputable def
HomologicalComplex₂.total.mapIso
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(e : K ≅ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
:
The isomorphism K.total c₁₂ ≅ L.total c₁₂ of homological complexes induced
by an isomorphism of bicomplexes K ≅ L.
Equations
Instances For
@[simp]
theorem
HomologicalComplex₂.total.mapIso_inv
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(e : K ≅ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
:
@[simp]
theorem
HomologicalComplex₂.total.mapIso_hom
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K L : HomologicalComplex₂ C c₁ c₂}
(e : K ≅ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
:
@[simp]
theorem
HomologicalComplex₂.ιTotal_map
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K L : HomologicalComplex₂ C c₁ c₂)
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) ((total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotal c₁₂ i₁ i₂ i₁₂ h)
@[simp]
theorem
HomologicalComplex₂.ιTotal_map_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K L : HomologicalComplex₂ C c₁ c₂)
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
(h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂)
{Z : C}
(h✝ : (L.total c₁₂).X i₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)
(CategoryTheory.CategoryStruct.comp ((total.map φ c₁₂).f i₁₂) h✝) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.ιTotal c₁₂ i₁ i₂ i₁₂ h) h✝)
@[simp]
theorem
HomologicalComplex₂.ιTotalOrZero_map
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K L : HomologicalComplex₂ C c₁ c₂)
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
:
CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) ((total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂)
@[simp]
theorem
HomologicalComplex₂.ιTotalOrZero_map_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K L : HomologicalComplex₂ C c₁ c₂)
(φ : K ⟶ L)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[K.HasTotal c₁₂]
[L.HasTotal c₁₂]
(i₁ : I₁)
(i₂ : I₂)
(i₁₂ : I₁₂)
{Z : C}
(h : (L.total c₁₂).X i₁₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂)
(CategoryTheory.CategoryStruct.comp ((total.map φ c₁₂).f i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂)
(CategoryTheory.CategoryStruct.comp (L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) h)
noncomputable def
HomologicalComplex₂.totalFunctor
(C : Type u_1)
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂]
:
CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (HomologicalComplex C c₁₂)
The functor which sends a bicomplex to its total complex.
Equations
Instances For
@[simp]
theorem
HomologicalComplex₂.totalFunctor_obj
(C : Type u_1)
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂]
(K : HomologicalComplex₂ C c₁ c₂)
:
@[simp]
theorem
HomologicalComplex₂.totalFunctor_map
(C : Type u_1)
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{I₁ : Type u_2}
{I₂ : Type u_3}
{I₁₂ : Type u_4}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
(c₁₂ : ComplexShape I₁₂)
[TotalComplexShape c₁ c₂ c₁₂]
[DecidableEq I₁₂]
[∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂]
{X✝ Y✝ : HomologicalComplex₂ C c₁ c₂}
(φ : X✝ ⟶ Y✝)
: