Direct-sum push-down to a shift-orbit category

For a linear module M : C ⥤ ModuleCat k, its push-down to the shift-orbit category has value ⨁ b, M(X⟦b⟧) at X. A homogeneous map of degree a sends the b-summand to the (a + b)-summand.

This file constructs that action, verifies its unit and composition laws from Mathlib's shift coherence, and packages it as an additive linear module over the orbit category. The construction is generic; covering-specific finite-support hypotheses enter only when restricting its values to finite-dimensional modules.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.orbitPushdownValue {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) (X : C) : Type (max uM w)

The value of the push-down module at an object of the orbit category.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownLof {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) (X : C) (b : A) : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X)) →ₗ[k] orbitPushdownValue M X

Inclusion of one translated value into the push-down direct sum.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownLof_eq_directSumOf {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) [DecidableEq A] (X : C) (b : A) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X))) : (orbitPushdownLof M X b) x = (DirectSum.of (fun (c : A) => ↑(M.obj ((CategoryTheory.shiftFunctor C c).obj X))) b) x

The push-down summand inclusion is the standard direct-sum generator.

def MagnitudeConjecture.CoveringHom.orbitPushdownArrow' {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {X Y : C} {a b c : A} (h : a + b = c) (f : ShiftHom X Y a) : (CategoryTheory.shiftFunctor C b).obj X ⟶ (CategoryTheory.shiftFunctor C c).obj Y

The map from the b-summand induced by a homogeneous orbit morphism of degree a, with an explicitly chosen output degree.

def MagnitudeConjecture.CoveringHom.orbitPushdownComponent' {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) {X Y : C} {a b c : A} (h : a + b = c) (f : ShiftHom X Y a) : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X)) →ₗ[k] ↑(M.obj ((CategoryTheory.shiftFunctor C c).obj Y))

Applying the upstairs module to the component arrow.

def MagnitudeConjecture.CoveringHom.orbitPushdownComponent {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) {X Y : C} (a b : A) (f : ShiftHom X Y a) : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X)) →ₗ[k] ↑(M.obj ((CategoryTheory.shiftFunctor C (a + b)).obj Y))

The component map with its canonical output degree.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownComponent_apply_heq_component'_apply {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) {X Y : C} {a b c : A} (h : a + b = c) (f : ShiftHom X Y a) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X))) : (orbitPushdownComponent M a b f) x ≍ (orbitPushdownComponent' M h f) x

The canonical component map agrees heterogeneously with the component map at any propositionally equal output degree.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPushdownComponent'_id {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) (X : C) (b : A) : orbitPushdownComponent' M ⋯ (shiftHomId X) = LinearMap.id

theorem MagnitudeConjecture.CoveringHom.orbitPushdownArrow'_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {X Y Z : C} {a c b ab ca d : A} (hab : a + b = ab) (hca : c + a = ca) (hleft : ca + b = d) (hright : c + ab = d) (f : ShiftHom X Y a) (g : ShiftHom Y Z c) : orbitPushdownArrow' hleft (shiftHomComp' hca f g) = CategoryTheory.CategoryStruct.comp (orbitPushdownArrow' hab f) (orbitPushdownArrow' hright g)

Component arrows respect homogeneous composition, including all degree reassociations.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownArrow_comp_fromShift {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 : C} (a b : A) (f : ShiftHom X Y a) : (shiftOrbitCompHom ((shiftOrbitOf ((CategoryTheory.shiftFunctor C b).obj X) ((CategoryTheory.shiftFunctor C (a + b)).obj Y) 0) (shiftHomZero (orbitPushdownArrow' ⋯ f)))) (shiftOrbitFromShift Y (a + b)) = (shiftOrbitCompHom (shiftOrbitFromShift X b)) ((shiftOrbitOf X Y a) f)

A homogeneous component arrow followed by the canonical path from its target translate equals the canonical path from the source translate followed by the original orbit morphism.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownComponent'_comp {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) {X Y Z : C} {a c b ab ca d : A} (hab : a + b = ab) (hca : c + a = ca) (hleft : ca + b = d) (hright : c + ab = d) (f : ShiftHom X Y a) (g : ShiftHom Y Z c) : orbitPushdownComponent' M hleft (shiftHomComp' hca f g) = orbitPushdownComponent' M hright g ∘ₗ orbitPushdownComponent' M hab f

Applying the module turns composition of component arrows into composition of component linear maps.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownHomogeneousMap {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) {X Y : C} (a : A) (f : ShiftHom X Y a) : orbitPushdownValue M X →ₗ[k] orbitPushdownValue M Y

A homogeneous orbit morphism acts on the direct sum by translating the summand index on the left by its degree.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPushdownHomogeneousMap_lof {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) {X Y : C} (a b : A) (f : ShiftHom X Y a) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X))) : (orbitPushdownHomogeneousMap M a f) ((orbitPushdownLof M X b) x) = (orbitPushdownLof M Y (a + b)) ((orbitPushdownComponent M a b f) x)

theorem MagnitudeConjecture.CoveringHom.orbitPushdownHomogeneousMap_comp {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) {X Y Z : C} {a c : A} (f : ShiftHom X Y a) (g : ShiftHom Y Z c) : orbitPushdownHomogeneousMap M (c + a) (shiftHomComp f g) = orbitPushdownHomogeneousMap M c g ∘ₗ orbitPushdownHomogeneousMap M a f

Homogeneous push-down maps respect homogeneous composition.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownHomogeneousLinearMap {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] {X Y : C} (a : A) : ShiftHom X Y a →ₗ[k] orbitPushdownValue M X →ₗ[k] orbitPushdownValue M Y

The action of degree-a homogeneous morphisms is linear in the morphism.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownMapLinear {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] {X Y : C} : ShiftOrbitHom A X Y →ₗ[k] orbitPushdownValue M X →ₗ[k] orbitPushdownValue M Y

The linear action of all finite-support orbit morphisms.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPushdownMapLinear_of {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] {X Y : C} (a : A) (f : ShiftHom X Y a) : (orbitPushdownMapLinear M) ((shiftOrbitOf X Y a) f) = orbitPushdownHomogeneousMap M a f

theorem MagnitudeConjecture.CoveringHom.orbitPushdownMapLinear_comp {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] {X Y Z : C} (f : ShiftOrbitHom A X Y) (g : ShiftOrbitHom A Y Z) : (orbitPushdownMapLinear M) ((shiftOrbitCompHom f) g) = (orbitPushdownMapLinear M) g ∘ₗ (orbitPushdownMapLinear M) f

The action of arbitrary finite-support orbit morphisms respects orbit composition.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPushdownHomogeneousMap_id {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) (X : C) : orbitPushdownHomogeneousMap M 0 (shiftHomId X) = LinearMap.id

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdown {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)

Gabriel's direct-sum push-down of a linear module along the canonical projection to the shift-orbit category.

instance MagnitudeConjecture.CoveringHom.orbitPushdown_additive {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : (orbitPushdown M).Additive

instance MagnitudeConjecture.CoveringHom.orbitPushdown_linear {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor.Linear k (orbitPushdown M)