Gabriel's pull-up/push-down decomposition

This file identifies the explicit coproduct model for pull-up of push-down with the bundled pull-up functor and with the formal module shifts attached to a chosen shift core.

noncomputable def MagnitudeConjecture.CoveringHom.linearOrbitPullupPushdownIso {k : Type uK} [Field 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 : LinearModuleCategory k) : (linearOrbitPullupPushdownTranslateCofan M).pt ≅ linearModuleOrbitPullup.obj (linearModuleOrbitPushdown.obj M)

The explicit coproduct object is the bundled pull-up of the bundled push-down.