Connecting maps of short exact sequences of complexes of modules #
For maps φ : X ⟶ Y and ψ : Y ⟶ Z of complexes of modules with ψ a monomorphism, the short
exact sequence cokernel φ ⟶ cokernel (φ ≫ ψ) ⟶ cokernel ψ
(TauCeti.kernelCokernelCompSequence_snakeInput_L₃_shortExact) has a connecting map on homology.
This file computes it on classes of elements.
Main statements #
TauCeti.exists_δ_kernelCokernelSequence_L₃_eq: the connecting map sends the class of a cyclexofcokernel ψ, lifted to an elementsofZwhose differential is the image of an elementtofY, to the class of the image oftincokernel φ.
theorem
TauCeti.exists_δ_kernelCokernelSequence_L₃_eq
{R : Type u_1}
[Ring R]
{X Y Z : CochainComplex (ModuleCat R) ℤ}
(φ : X ⟶ Y)
(ψ : Y ⟶ Z)
[CategoryTheory.Mono ψ]
(n : ℤ)
(s : ↑(Z.X n))
(t : ↑(Y.X (n + 1)))
(hst : (ModuleCat.Hom.hom (ψ.f (n + 1))) t = (ModuleCat.Hom.hom (Z.d n (n + 1))) s)
(x : ↑((CategoryTheory.Limits.cokernel ψ).X n))
(hx : (ModuleCat.Hom.hom ((CategoryTheory.Limits.cokernel ψ).d n (n + 1))) x = 0)
(hsx : (ModuleCat.Hom.hom ((CategoryTheory.Limits.cokernel.π ψ).f n)) s = x)
:
∃ (hc :
(ModuleCat.Hom.hom ((CategoryTheory.Limits.cokernel φ).d (n + 1) (n + 1 + 1)))
((ModuleCat.Hom.hom ((CategoryTheory.Limits.cokernel.π φ).f (n + 1))) t) = 0),
(ModuleCat.Hom.hom (⋯.δ n (n + 1) ⋯))
((ModuleCat.Hom.hom (HomologicalComplex.homologyπ (CategoryTheory.Limits.cokernel ψ) n))
(HomologicalComplex.moduleCatCyclesMk (CategoryTheory.Limits.cokernel ψ) x (n + 1) ⋯ hx)) = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ (CategoryTheory.Limits.cokernel φ) (n + 1)))
(HomologicalComplex.moduleCatCyclesMk (CategoryTheory.Limits.cokernel φ)
((ModuleCat.Hom.hom ((CategoryTheory.Limits.cokernel.π φ).f (n + 1))) t) (n + 1 + 1) ⋯ hc)
The connecting map of the cokernel sequence of a composite, on classes. Let φ : X ⟶ Y and
ψ : Y ⟶ Z be maps of complexes of modules, ψ a monomorphism, s an element of Z in degree
n and t an element of Y in degree n + 1 with ψ t = d s, such that the image of s in
cokernel ψ is a cycle x. Then the image of t in cokernel φ is a cycle, and it represents
the image of the class of x under the connecting map of
cokernel φ ⟶ cokernel (φ ≫ ψ) ⟶ cokernel ψ.