Linear maps out of a degreewise split short complex of cochain complexes of modules

Let S be a short complex of cochain complexes of A-modules, with chosen splittings of the degreewise short complexes S.X₁ n ⟶ S.X₂ n ⟶ S.X₃ n. The splittings need not commute with the differentials. This file records how an A-linear map from a term of the middle complex to an A-module M which kills the image of the differential restricts along the inclusion S.f, is corrected by a primitive composed with the retraction, and descends along the section to the third complex. These are the elementary steps in the proof that the dual of the middle complex is exact when the duals of the outer complexes are.

Main results

• CategoryTheory.ShortComplex.comp_f_comp_d_eq_zero: restriction to the first complex preserves killing the image of the differential.
• CategoryTheory.ShortComplex.residual_comp_f_eq_zero: the residual functional φ - ψ₁ ∘ r ∘ d vanishes on the first complex.
• CategoryTheory.ShortComplex.residual_comp_d_eq_zero: subtracting a functional of the form ψ₀ ∘ d preserves killing the image of the differential.
• CategoryTheory.ShortComplex.comp_s_comp_d_eq_zero: a functional vanishing on the first complex and on the image of the differential descends along the section to the third complex.

theorem CategoryTheory.ShortComplex.comp_f_comp_d_eq_zero {A : Type u} [Ring A] {S : ShortComplex (CochainComplex (ModuleCat A) ℤ)} {M : Type w} [AddCommGroup M] [Module A M] {i j : ℤ} {φ : ↑(S.X₂.X j) →ₗ[A] M} (hφ : φ ∘ₗ ModuleCat.Hom.hom (S.X₂.d i j) = 0) : (φ ∘ₗ ModuleCat.Hom.hom (S.f.f j)) ∘ₗ ModuleCat.Hom.hom (S.X₁.d i j) = 0

Restricting a functional that kills the image of the middle differential to the first complex along the inclusion gives a functional that kills the image of the first differential.

theorem CategoryTheory.ShortComplex.residual_comp_f_eq_zero {A : Type u} [Ring A] {S : ShortComplex (CochainComplex (ModuleCat A) ℤ)} {M : Type w} [AddCommGroup M] [Module A M] {k : ℤ} (s : { X₁ := S.X₁.X k, X₂ := S.X₂.X k, X₃ := S.X₃.X k, f := S.f.f k, g := S.g.f k, zero := ⋯ }.Splitting) {j : ℤ} {φ : ↑(S.X₂.X j) →ₗ[A] M} {ψ₁ : ↑(S.X₁.X k) →ₗ[A] M} (hψ₁ : ψ₁ ∘ₗ ModuleCat.Hom.hom (S.X₁.d j k) = φ ∘ₗ ModuleCat.Hom.hom (S.f.f j)) : (φ - (ψ₁ ∘ₗ ModuleCat.Hom.hom s.r) ∘ₗ ModuleCat.Hom.hom (S.X₂.d j k)) ∘ₗ ModuleCat.Hom.hom (S.f.f j) = 0

The residual functional φ - ψ₁ ∘ r ∘ d vanishes on the first complex, where ψ₁ is a primitive of the restriction of φ to the first complex.

theorem CategoryTheory.ShortComplex.residual_comp_d_eq_zero {A : Type u} [Ring A] {S : ShortComplex (CochainComplex (ModuleCat A) ℤ)} {M : Type w} [AddCommGroup M] [Module A M] {i j k : ℤ} {φ : ↑(S.X₂.X j) →ₗ[A] M} (hφ : φ ∘ₗ ModuleCat.Hom.hom (S.X₂.d i j) = 0) (ψ₀ : ↑(S.X₂.X k) →ₗ[A] M) : (φ - ψ₀ ∘ₗ ModuleCat.Hom.hom (S.X₂.d j k)) ∘ₗ ModuleCat.Hom.hom (S.X₂.d i j) = 0

Subtracting a functional of the form ψ₀ ∘ d from one killing the image of the middle differential into degree j keeps it killing that image, as d ∘ d = 0.

theorem CategoryTheory.ShortComplex.comp_s_comp_d_eq_zero {A : Type u} [Ring A] {S : ShortComplex (CochainComplex (ModuleCat A) ℤ)} {M : Type w} [AddCommGroup M] [Module A M] {i j : ℤ} (si : { X₁ := S.X₁.X i, X₂ := S.X₂.X i, X₃ := S.X₃.X i, f := S.f.f i, g := S.g.f i, zero := ⋯ }.Splitting) (sj : { X₁ := S.X₁.X j, X₂ := S.X₂.X j, X₃ := S.X₃.X j, f := S.f.f j, g := S.g.f j, zero := ⋯ }.Splitting) {ρ : ↑(S.X₂.X j) →ₗ[A] M} (hρf : ρ ∘ₗ ModuleCat.Hom.hom (S.f.f j) = 0) (hρ : ρ ∘ₗ ModuleCat.Hom.hom (S.X₂.d i j) = 0) : (ρ ∘ₗ ModuleCat.Hom.hom sj.s) ∘ₗ ModuleCat.Hom.hom (S.X₃.d i j) = 0

A functional on the middle complex that vanishes on the first complex and on the image of the differential into degree j descends along the section to a functional on the third complex that vanishes on the image of its differential.