Split-component lifting between tau-sequences

This file begins the categorical chain-map lifting used in Iyama, Tau-categories I, 3.5.2. For two right tau-sequences, a split-epimorphic right-endpoint component forces both earlier components to be split epic. The mixed left-mesh-to-right-mesh specialization is built on this lemma.

theorem QuotientSubmoduleEquidistribution.Iyama.RightTauSequence.splitEpi_components_of_splitEpi_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S T : CategoryTheory.ShortComplex C} (hS : RightTauSequence S) (hT : RightTauSequence T) (φ : S ⟶ T) [CategoryTheory.IsSplitEpi φ.τ₃] : CategoryTheory.IsSplitEpi φ.τ₁ ∧ CategoryTheory.IsSplitEpi φ.τ₂

A chain map between right tau-sequences which is split epic at the right endpoint is split epic in the other two degrees as well.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence.splitMono_components_of_splitMono_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S T : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) (hT : LeftTauSequence T) (phi : S ⟶ T) [CategoryTheory.IsSplitMono phi.τ₁] : CategoryTheory.IsSplitMono phi.τ₂ ∧ CategoryTheory.IsSplitMono phi.τ₃

A chain map between left tau-sequences which is split monic at the left endpoint is split monic in the other two degrees as well.