Degree extraction from Gabriel push-down transformations

A natural transformation between two orbit push-down modules has a component in every deck degree. This file extracts the degree-a component by inserting the source module in degree zero, applying the transformation, and projecting to degree -a. Naturality for zero-degree orbit arrows turns the extracted component into an upstairs module map, and the inverse-precomposition translation isomorphism turns it into a genuine shifted morphism.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownNatTransDegreeAppLinear {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (a : A) (X : C) : (orbitPushdown M ⟶ orbitPushdown N) → ↑(M.obj X) →ₗ[k] ↑(N.obj ((D.F (-a)).obj X))

The (-a) output component of a push-down transformation, evaluated on the zero input component.

theorem MagnitudeConjecture.CoveringHom.shiftFunctorZero_inv_comp_orbitPushdownArrow_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) {X Y : C} (h : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).inv.app X) (orbitPushdownArrow' ⋯ (shiftHomZero h)) = CategoryTheory.CategoryStruct.comp h ((CategoryTheory.shiftFunctorZero C A).inv.app Y)

theorem MagnitudeConjecture.CoveringHom.orbitPushdownZeroMap_inclusion {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] {M : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {X Y : C} (h : X ⟶ Y) (x : ↑(M.obj X)) : ((orbitPushdownMapLinear M) ((shiftOrbitOf X Y 0) (shiftHomZero h))) ((orbitPushdownLof M X 0) ((CategoryTheory.ConcreteCategory.hom (M.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))) x)) = (orbitPushdownLof M Y 0) ((CategoryTheory.ConcreteCategory.hom (M.map ((CategoryTheory.shiftFunctorZero C A).inv.app Y))) ((CategoryTheory.ConcreteCategory.hom (M.map h)) x))

theorem MagnitudeConjecture.CoveringHom.orbitPushdownArrow_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) {X Y : C} (h : X ⟶ Y) (b : A) : orbitPushdownArrow' ⋯ (shiftHomZero h) = (CategoryTheory.shiftFunctor C b).map h

theorem MagnitudeConjecture.CoveringHom.orbitPushdownHomogeneousMap_zero_lof {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) {N : CategoryTheory.Functor C (ModuleCat k)} {X Y : C} (h : X ⟶ Y) (b : A) (x : ↑(N.obj ((D.F b).obj X))) : (orbitPushdownHomogeneousMap N 0 (shiftHomZero h)) ((orbitPushdownLof N X b) x) = (orbitPushdownLof N Y b) ((CategoryTheory.ConcreteCategory.hom (N.map ((CategoryTheory.shiftFunctor C b).map h))) x)

theorem MagnitudeConjecture.CoveringHom.orbitPushdownZeroMap_component {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] {N : CategoryTheory.Functor C (ModuleCat k)} [N.Additive] [CategoryTheory.Functor.Linear k N] {X Y : C} (h : X ⟶ Y) (b : A) : DirectSum.component k A (fun (c : A) => ↑(N.obj ((CategoryTheory.shiftFunctor C c).obj Y))) b ∘ₗ (orbitPushdownMapLinear N) ((shiftOrbitOf X Y 0) (shiftHomZero h)) = ModuleCat.Hom.hom (N.map ((CategoryTheory.shiftFunctor C b).map h)) ∘ₗ DirectSum.component k A (fun (c : A) => ↑(N.obj ((CategoryTheory.shiftFunctor C c).obj X))) b

theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTransDegreeAppLinear_naturality {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (a : A) (α : orbitPushdown M ⟶ orbitPushdown N) {X Y : C} (h : X ⟶ Y) : orbitPushdownNatTransDegreeAppLinear D a Y α ∘ₗ ModuleCat.Hom.hom (M.map h) = ModuleCat.Hom.hom (N.map ((D.F (-a)).map h)) ∘ₗ orbitPushdownNatTransDegreeAppLinear D a X α

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownNatTransDegreeRaw {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (a : A) : (orbitPushdown M ⟶ orbitPushdown N) → (M ⟶ (D.F (-a)).comp N)

The degree-a part recovered from a transformation between two Gabriel push-down modules, before identifying inverse precomposition with module translation.

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegree {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M₀ N₀ : LinearModuleCategory k) (a : A) : (linearModuleOrbitPushdown.obj M₀ ⟶ linearModuleOrbitPushdown.obj N₀) → ShiftHom M₀ N₀ a

The degree-a upstairs module map recovered from a transformation between Gabriel push-downs.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownNatTransDegreeAppLinearMap {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (a : A) (X : C) : (orbitPushdown M ⟶ orbitPushdown N) →ₗ[k] ↑(M.obj X) →ₗ[k] ↑(N.obj ((D.F (-a)).obj X))

Degree extraction at one object is linear in the push-down transformation.

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegreeLinear {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M₀ N₀ : LinearModuleCategory k) (a : A) : (linearModuleOrbitPushdown.obj M₀ ⟶ linearModuleOrbitPushdown.obj N₀) →ₗ[k] ShiftHom M₀ N₀ a

Extraction of one shifted module map is linear.