Componentwise factorization in shift-orbit categories

This file gives the finite-support assembly used in Gabriel's almost-split push-down argument. If every homogeneous component of a shift-orbit morphism factors through an ordinary map, then the whole orbit morphism factors through its degree-zero inclusion.

theorem MagnitudeConjecture.CoveringHom.shiftHomComp'_zero_left {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {X Y Z : C} {a : A} (f : X ⟶ Y) (g : ShiftHom Y Z a) : shiftHomComp' ⋯ (shiftHomZero f) g = CategoryTheory.CategoryStruct.comp f g

Composition of an ordinary map in degree zero with a homogeneous map is ordinary categorical composition.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_zero_left_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y Z : C} {a : A} (f : X ⟶ Y) (g : ShiftHom Y Z a) : (shiftOrbitCompHom ((shiftOrbitOf X Y 0) (shiftHomZero f))) ((shiftOrbitOf Y Z a) g) = (shiftOrbitOf X Z a) (CategoryTheory.CategoryStruct.comp f g)

In the shift-orbit category, composing an ordinary degree-zero map with a homogeneous morphism is ordinary categorical composition.

theorem MagnitudeConjecture.CoveringHom.exists_shiftOrbit_factor_of_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y Z : C} (f : X ⟶ Y) (q : ShiftOrbitHom A X Z) (hfac : ∀ (a : A), ∃ (c : ShiftHom Y Z a), (shiftOrbitCompHom ((shiftOrbitOf X Y 0) (shiftHomZero f))) ((shiftOrbitOf Y Z a) c) = (shiftOrbitOf X Z a) (q a)) : ∃ (c : ShiftOrbitHom A Y Z), (shiftOrbitCompHom ((shiftOrbitOf X Y 0) (shiftHomZero f))) c = q

Componentwise factorizations through an ordinary morphism assemble into a factorization of a finite-support shift-orbit morphism.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_zero_left_component_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [Field k] [CategoryTheory.Linear k C] {X Y Z : C} (f : X ⟶ Y) (r : ShiftOrbitHom A Y Z) : ((shiftOrbitCompHom ((shiftOrbitOf X Y 0) (shiftHomZero f))) r) 0 = shiftHomZero (CategoryTheory.CategoryStruct.comp f ((shiftHomZeroLinearEquiv Y Z).symm (r 0)))

The identity-degree component after precomposition by an ordinary map is ordinary composition.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_zero_right_component_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [Field k] [CategoryTheory.Linear k C] {X Y Z : C} (r : ShiftOrbitHom A X Y) (f : Y ⟶ Z) : ((shiftOrbitCompHom r) ((shiftOrbitOf Y Z 0) (shiftHomZero f))) 0 = shiftHomZero (CategoryTheory.CategoryStruct.comp ((shiftHomZeroLinearEquiv X Y).symm (r 0)) f)

The identity-degree component after postcomposition by an ordinary map is ordinary categorical composition.

theorem MagnitudeConjecture.CoveringHom.isSplitMono_of_shiftOrbit_zero_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (k : Type u_2) [Field k] [CategoryTheory.Linear k C] {X Y : C} (f : X ⟶ Y) (hsplit : CategoryTheory.IsSplitMono (have this := (shiftOrbitOf X Y 0) (shiftHomZero f); this)) : CategoryTheory.IsSplitMono f

The degree-zero orbit inclusion reflects split monomorphisms.