The homology sequence #
If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is a short exact sequence in a category of complexes
HomologicalComplex C c in an abelian category (i.e. S is a short complex in
that category and satisfies hS : S.ShortExact), then whenever i and j are degrees
such that hij : c.Rel i j, then there is a long exact sequence :
... ⟶ S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j ⟶ ....
The connecting homomorphism S.X₃.homology i ⟶ S.X₁.homology j is hS.δ i j hij, and
the exactness is asserted as lemmas hS.homology_exact₁, hS.homology_exact₂ and
hS.homology_exact₃.
The proof is based on the snake lemma, similarly as it was originally done in the Liquid Tensor Experiment.
References #
noncomputable def
HomologicalComplex.opcyclesToCycles
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
K.opcycles i ⟶ K.cycles j
The morphism K.opcycles i ⟶ K.cycles j that is induced by K.d i j.
Equations
- K.opcyclesToCycles i j = K.liftCycles (K.fromOpcycles i j) (c.next j) ⋯ ⋯
Instances For
@[simp]
theorem
HomologicalComplex.opcyclesToCycles_iCycles_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
{Z : C}
(h : K.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) = CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h
@[simp]
theorem
HomologicalComplex.opcyclesToCycles_iCycles
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j) = K.fromOpcycles i j
theorem
HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
{Z : C}
(h : K.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles i)
(CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h)) = CategoryTheory.CategoryStruct.comp (K.d i j) h
theorem
HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles i)
(CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j)) = K.d i j
@[simp]
theorem
HomologicalComplex.pOpcycles_opcyclesToCycles_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
{Z : C}
(h : K.cycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) h) = CategoryTheory.CategoryStruct.comp (K.toCycles i j) h
@[simp]
theorem
HomologicalComplex.pOpcycles_opcyclesToCycles
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.opcyclesToCycles i j) = K.toCycles i j
@[simp]
theorem
HomologicalComplex.homologyι_opcyclesToCycles_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
{Z : C}
(h : K.cycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
HomologicalComplex.homologyι_opcyclesToCycles
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.opcyclesToCycles i j) = 0
@[simp]
theorem
HomologicalComplex.opcyclesToCycles_homologyπ_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
{Z : C}
(h : K.homology j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
HomologicalComplex.opcyclesToCycles_homologyπ
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.homologyπ j) = 0
@[simp]
theorem
HomologicalComplex.opcyclesToCycles_naturality_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(φ : K ⟶ L)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
[L.HasHomology i]
[L.HasHomology j]
{Z : C}
(h : L.cycles j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i)
(CategoryTheory.CategoryStruct.comp (L.opcyclesToCycles i j) h) = CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ j) h)
@[simp]
theorem
HomologicalComplex.opcyclesToCycles_naturality
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(φ : K ⟶ L)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
[L.HasHomology i]
[L.HasHomology j]
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (L.opcyclesToCycles i j) = CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (HomologicalComplex.cyclesMap φ j)
@[simp]
theorem
HomologicalComplex.natTransOpCyclesToCycles_app
(C : Type u_1)
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(c : ComplexShape ι)
(i : ι)
(j : ι)
[CategoryTheory.CategoryWithHomology C]
(K : HomologicalComplex C c)
:
(HomologicalComplex.natTransOpCyclesToCycles C c i j).app K = K.opcyclesToCycles i j
noncomputable def
HomologicalComplex.natTransOpCyclesToCycles
(C : Type u_1)
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(c : ComplexShape ι)
(i : ι)
(j : ι)
[CategoryTheory.CategoryWithHomology C]
:
The natural transformation K.opcyclesToCycles i j : K.opcycles i ⟶ K.cycles j for all
K : HomologicalComplex C c.
Equations
- HomologicalComplex.natTransOpCyclesToCycles C c i j = { app := fun (K : HomologicalComplex C c) => K.opcyclesToCycles i j, naturality := ⋯ }
Instances For
noncomputable def
HomologicalComplex.HomologySequence.composableArrows₃
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.
Equations
- HomologicalComplex.HomologySequence.composableArrows₃ K i j = CategoryTheory.ComposableArrows.mk₃ (K.homologyι i) (K.opcyclesToCycles i j) (K.homologyπ j)
Instances For
instance
HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.Mono ((HomologicalComplex.HomologySequence.composableArrows₃ K i j).map' 0 1 ⋯ ⋯)
Equations
- ⋯ = ⋯
instance
HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
[K.HasHomology i]
[K.HasHomology j]
:
CategoryTheory.Epi ((HomologicalComplex.HomologySequence.composableArrows₃ K i j).map' 2 3 ⋯ ⋯)
Equations
- ⋯ = ⋯
theorem
HomologicalComplex.HomologySequence.composableArrows₃_exact
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
(j : ι)
(hij : c.Rel i j)
[CategoryTheory.CategoryWithHomology C]
:
(HomologicalComplex.HomologySequence.composableArrows₃ K i j).Exact
The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j is exact
when c.Rel i j.
@[simp]
theorem
HomologicalComplex.HomologySequence.composableArrows₃Functor_map
(C : Type u_1)
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(i : ι)
(j : ι)
[CategoryTheory.CategoryWithHomology C]
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(φ : K ⟶ L)
:
@[simp]
theorem
HomologicalComplex.HomologySequence.composableArrows₃Functor_obj
(C : Type u_1)
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(i : ι)
(j : ι)
[CategoryTheory.CategoryWithHomology C]
(K : HomologicalComplex C c)
:
noncomputable def
HomologicalComplex.HomologySequence.composableArrows₃Functor
(C : Type u_1)
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
(i : ι)
(j : ι)
[CategoryTheory.CategoryWithHomology C]
:
The functor HomologicalComplex C c ⥤ ComposableArrows C 3 that maps K to the
diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HomologicalComplex.opcycles_right_exact
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
(S : CategoryTheory.ShortComplex (HomologicalComplex C c))
(hS : S.Exact)
[CategoryTheory.Epi S.g]
(i : ι)
[S.X₁.HasHomology i]
[S.X₂.HasHomology i]
[S.X₃.HasHomology i]
:
(CategoryTheory.ShortComplex.mk (HomologicalComplex.opcyclesMap S.f i) (HomologicalComplex.opcyclesMap S.g i) ⋯).Exact
If X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is an exact sequence of homological complexes, then
X₁.opcycles i ⟶ X₂.opcycles i ⟶ X₃.opcycles i ⟶ 0 is exact. This lemma states
the exactness at X₂.opcycles i, while the fact that X₂.opcycles i ⟶ X₃.opcycles i
is an epi is an instance.
theorem
HomologicalComplex.cycles_left_exact
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
(S : CategoryTheory.ShortComplex (HomologicalComplex C c))
(hS : S.Exact)
[CategoryTheory.Mono S.f]
(i : ι)
[S.X₁.HasHomology i]
[S.X₂.HasHomology i]
[S.X₃.HasHomology i]
:
(CategoryTheory.ShortComplex.mk (HomologicalComplex.cyclesMap S.f i) (HomologicalComplex.cyclesMap S.g i) ⋯).Exact
If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ is an exact sequence of homological complex, then
0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i is exact. This lemma states
the exactness at X₂.cycles i, while the fact that X₁.cycles i ⟶ X₂.cycles i
is a mono is an instance.
@[simp]
theorem
HomologicalComplex.HomologySequence.snakeInput_v₀₁
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₀₁ = S.mapNatTrans (HomologicalComplex.natTransHomologyι C c i)
@[simp]
theorem
HomologicalComplex.HomologySequence.snakeInput_L₂
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₂ = (HomologicalComplex.cyclesFunctor C c j).mapShortComplex.obj S
@[simp]
theorem
HomologicalComplex.HomologySequence.snakeInput_L₁
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₁ = (HomologicalComplex.opcyclesFunctor C c i).mapShortComplex.obj S
@[simp]
theorem
HomologicalComplex.HomologySequence.snakeInput_L₀
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₀ = (HomologicalComplex.homologyFunctor C c i).mapShortComplex.obj S
@[simp]
theorem
HomologicalComplex.HomologySequence.snakeInput_L₃
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₃ = (HomologicalComplex.homologyFunctor C c j).mapShortComplex.obj S
@[simp]
theorem
HomologicalComplex.HomologySequence.snakeInput_v₂₃
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₂₃ = S.mapNatTrans (HomologicalComplex.natTransHomologyπ C c j)
@[simp]
theorem
HomologicalComplex.HomologySequence.snakeInput_v₁₂
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₁₂ = S.mapNatTrans (HomologicalComplex.natTransOpCyclesToCycles C c i j)
noncomputable def
HomologicalComplex.HomologySequence.snakeInput
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
Given a short exact short complex S : HomologicalComplex C c, and degrees i and j
such that c.Rel i j, this is the snake diagram whose four lines are respectively
obtained by applying the functors homologyFunctor C c i, opcyclesFunctor C c i,
cyclesFunctor C c j, homologyFunctor C c j to S. Applying the snake lemma to this
gives the homology sequence of S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.ShortComplex.ShortExact.δ
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
S.X₃.homology i ⟶ S.X₁.homology j
The connecting homoomorphism S.X₃.homology i ⟶ S.X₁.homology j for a short exact
short complex S.
Equations
- hS.δ i j hij = (HomologicalComplex.HomologySequence.snakeInput hS i j hij).δ
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
{Z : C}
(h : S.X₂.homology j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (hS.δ i j hij)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.f j) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.δ_comp
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
CategoryTheory.CategoryStruct.comp (hS.δ i j hij) (HomologicalComplex.homologyMap S.f j) = 0
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
{Z : C}
(h : S.X₁.homology j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.g i)
(CategoryTheory.CategoryStruct.comp (hS.δ i j hij) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.comp_δ
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.g i) (hS.δ i j hij) = 0
theorem
CategoryTheory.ShortComplex.ShortExact.homology_exact₁
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(CategoryTheory.ShortComplex.mk (hS.δ i j hij) (HomologicalComplex.homologyMap S.f j) ⋯).Exact
Exactness of S.X₃.homology i ⟶ S.X₁.homology j ⟶ S.X₂.homology j.
theorem
CategoryTheory.ShortComplex.ShortExact.homology_exact₂
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
:
(CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact
Exactness of S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i.
theorem
CategoryTheory.ShortComplex.ShortExact.homology_exact₃
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
(CategoryTheory.ShortComplex.mk (HomologicalComplex.homologyMap S.g i) (hS.δ i j hij) ⋯).Exact
Exactness of S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j.
theorem
CategoryTheory.ShortComplex.ShortExact.δ_eq'
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
{A : C}
(x₃ : A ⟶ S.X₃.homology i)
(x₂ : A ⟶ S.X₂.opcycles i)
(x₁ : A ⟶ S.X₁.cycles j)
(h₂ : CategoryTheory.CategoryStruct.comp x₂ (HomologicalComplex.opcyclesMap S.g i) = CategoryTheory.CategoryStruct.comp x₃ (S.X₃.homologyι i))
(h₁ : CategoryTheory.CategoryStruct.comp x₁ (HomologicalComplex.cyclesMap S.f j) = CategoryTheory.CategoryStruct.comp x₂ (S.X₂.opcyclesToCycles i j))
:
CategoryTheory.CategoryStruct.comp x₃ (hS.δ i j hij) = CategoryTheory.CategoryStruct.comp x₁ (S.X₁.homologyπ j)
theorem
CategoryTheory.ShortComplex.ShortExact.δ_eq
{C : Type u_1}
{ι : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
(j : ι)
(hij : c.Rel i j)
{A : C}
(x₃ : A ⟶ S.X₃.X i)
(hx₃ : CategoryTheory.CategoryStruct.comp x₃ (S.X₃.d i j) = 0)
(x₂ : A ⟶ S.X₂.X i)
(hx₂ : CategoryTheory.CategoryStruct.comp x₂ (S.g.f i) = x₃)
(x₁ : A ⟶ S.X₁.X j)
(hx₁ : CategoryTheory.CategoryStruct.comp x₁ (S.f.f j) = CategoryTheory.CategoryStruct.comp x₂ (S.X₂.d i j))
(k : ι)
(hk : c.next j = k)
:
CategoryTheory.CategoryStruct.comp (S.X₃.liftCycles x₃ j ⋯ hx₃)
(CategoryTheory.CategoryStruct.comp (S.X₃.homologyπ i) (hS.δ i j hij)) = CategoryTheory.CategoryStruct.comp (S.X₁.liftCycles x₁ k hk ⋯) (S.X₁.homologyπ j)