Gabriel push-down is left adjoint to pull-up

Pull-up is restriction along the degree-zero functor from the covering category to its shift-orbit category. A map from a push-down module is determined by its value on the normalized degree-zero summands. Conversely, a map to pull-up extends over every translated summand by the canonical orbit isomorphism from that translate to the original object.

These constructions are mutually inverse and natural in both module variables. They give the push-down/pull-up adjunction used in Gabriel's proof that push-down preserves Auslander--Reiten sequences.

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPullup {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)] : CategoryTheory.Functor (LinearModuleCategory k) (LinearModuleCategory k)

Pull-up along the degree-zero orbit functor.

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitPullup_additive {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)] : linearModuleOrbitPullup.Additive

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitPullup_linear {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)] : CategoryTheory.Functor.Linear k linearModuleOrbitPullup

theorem MagnitudeConjecture.CoveringHom.shiftFunctorZero_inv_comp_orbitPushdownArrow_zero_of_hasShift {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift 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_of_hasShift {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 : 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))

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownToPullup {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (α : orbitPushdown M ⟶ N) : M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N

Restrict a map out of push-down to the degree-zero input summand.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupToPushdownAppLinear {k : Type uK} [Field k] {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] {M : CategoryTheory.Functor C (ModuleCat k)} {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (β : M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N) (X : C) : orbitPushdownValue M X →ₗ[k] ↑(N.obj X)

Extend a map to pull-up over every translated summand.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPullupToPushdownAppLinear_lof {k : Type uK} [Field k] {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] {M : CategoryTheory.Functor C (ModuleCat k)} {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (β : M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N) (X : C) (b : A) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X))) : (orbitPullupToPushdownAppLinear β X) ((orbitPushdownLof M X b) x) = (CategoryTheory.ConcreteCategory.hom (N.map (shiftOrbitFromShift X b))) ((CategoryTheory.ConcreteCategory.hom (β.app ((CategoryTheory.shiftFunctor C b).obj X))) x)

theorem MagnitudeConjecture.CoveringHom.orbitPullupToPushdownAppLinear_naturality_homogeneous {k : Type uK} [Field k] {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] {M : CategoryTheory.Functor C (ModuleCat k)} {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (β : M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N) {X Y : C} (a : A) (f : ShiftHom X Y a) : orbitPullupToPushdownAppLinear β Y ∘ₗ orbitPushdownHomogeneousMap M a f = ModuleCat.Hom.hom (N.map ((shiftOrbitOf X Y a) f)) ∘ₗ orbitPullupToPushdownAppLinear β X

theorem MagnitudeConjecture.CoveringHom.orbitPullupToPushdownAppLinear_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] [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] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} [N.Additive] (β : M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N) {X Y : C} (f : ShiftOrbitHom A X Y) : orbitPullupToPushdownAppLinear β Y ∘ₗ (orbitPushdownMapLinear M) f = ModuleCat.Hom.hom (N.map f) ∘ₗ orbitPullupToPushdownAppLinear β X

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupToPushdown {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} [N.Additive] (β : M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N) : orbitPushdown M ⟶ N

The extension of a pull-up map is a natural transformation out of push-down.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownFromShift_zero_lof_of_hasShift {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 : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (X : C) (b : A) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X))) : ((orbitPushdownMapLinear M) (shiftOrbitFromShift X b)) ((orbitPushdownLof M ((CategoryTheory.shiftFunctor C b).obj X) 0) ((CategoryTheory.ConcreteCategory.hom (M.map ((CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C b).obj X)))) x)) = (orbitPushdownLof M X b) x

theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTrans_ext_zero_target {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (α β : orbitPushdown M ⟶ N) (hzero : ∀ (X : C) (x : ↑(M.obj X)), (CategoryTheory.ConcreteCategory.hom (α.app X)) ((orbitPushdownLof M X 0) ((CategoryTheory.ConcreteCategory.hom (M.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))) x)) = (CategoryTheory.ConcreteCategory.hom (β.app X)) ((orbitPushdownLof M X 0) ((CategoryTheory.ConcreteCategory.hom (M.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))) x))) : α = β

Maps out of push-down are determined by their restrictions to normalized degree-zero summands.

theorem MagnitudeConjecture.CoveringHom.orbitPullupToPushdown_orbitPushdownToPullup {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} [N.Additive] (α : orbitPushdown M ⟶ N) : orbitPullupToPushdown (orbitPushdownToPullup α) = α

theorem MagnitudeConjecture.CoveringHom.identityZeroInv_comp_shiftOrbitFromShift {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 : C) : (shiftOrbitCompHom (ShiftOrbitCategory.identityComponentFunctor.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))) (shiftOrbitFromShift X 0) = shiftOrbitId X

theorem MagnitudeConjecture.CoveringHom.orbitPushdownToPullup_orbitPullupToPushdown {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} [N.Additive] (β : M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N) : orbitPushdownToPullup (orbitPullupToPushdown β) = β

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownPullupEquiv {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} [N.Additive] : (orbitPushdown M ⟶ N) ≃ (M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N)

The push-down/pull-up Hom correspondence.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownToPullup_comp {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N P : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} [P.Additive] [CategoryTheory.Functor.Linear k P] (α : orbitPushdown M ⟶ N) (g : N ⟶ P) : orbitPushdownToPullup (CategoryTheory.CategoryStruct.comp α g) = CategoryTheory.CategoryStruct.comp (orbitPushdownToPullup α) (ShiftOrbitCategory.identityComponentFunctor.whiskerLeft g)

theorem MagnitudeConjecture.CoveringHom.orbitPushdownToPullup_orbitPushdownNatTrans_comp {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 : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} {L : CategoryTheory.Functor C (ModuleCat k)} [L.Additive] [CategoryTheory.Functor.Linear k L] (f : L ⟶ M) (α : orbitPushdown M ⟶ N) : orbitPushdownToPullup (CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans f) α) = CategoryTheory.CategoryStruct.comp f (orbitPushdownToPullup α)

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownPullupEquiv {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) (N₀ : LinearModuleCategory k) : (linearModuleOrbitPushdown.obj M₀ ⟶ N₀) ≃ (M₀ ⟶ linearModuleOrbitPullup.obj N₀)

The Hom correspondence lifted to the full subcategories of additive linear modules.

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownPullupAdjunction {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)] : linearModuleOrbitPushdown ⊣ linearModuleOrbitPullup

Gabriel push-down is left adjoint to pull-up along the degree-zero orbit functor.