The local splitting statement, up to unit nonvanishing

The assembly of the local splitting statement: the splitting algebra of the dualised unit-form point, with its class and the restriction identity, feeds the reduction. What remains at each consumer is the nonvanishing of the algebra's unit, which over an ind-category follows from the stage units through the filtered criterion.

noncomputable def RS.rappel210Algebra {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] : D

The splitting algebra of a short exact sequence: the local splitting chain of the dualised unit-form point.

Equations

• RS.rappel210Algebra S = RS.splitAlgebra (RS.unitFormMid S)ᘁ (RS.unitFormPoint S)

theorem RS.rappel210_of_unit_nonzero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight Z)] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (hS : S.ShortExact) (hnz : splitAlgebraUnit (unitFormMid S)ᘁ (unitFormPoint S) ≠ 0) : Rappel210Statement S hS

The local splitting statement holds once the unit of the splitting algebra survives: the class of the dual middle object restricts on the point to the unit, so the reduction applies.