Descent of shift-compatible functors through shift-orbit categories

A functor commuting coherently with shifts acts on homogeneous shifted morphisms and hence on their finite-support direct sums. If its target has the trivial shift, summing the target degree components gives a descended functor from the source shift-orbit category. The final section applies this construction to Gabriel orbit push-down.

def MagnitudeConjecture.CoveringHom.shiftOrbitDescendHomogeneousMap {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.CommShift A] {X Y : C} (a : A) (f : ShiftHom X Y a) : ShiftHom (F.obj X) (F.obj Y) a

The image of a homogeneous shifted morphism under a shift-compatible functor.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitDescendHomogeneousMap_id {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.CommShift A] (X : C) : shiftOrbitDescendHomogeneousMap F 0 (shiftHomId X) = shiftHomId (F.obj X)

theorem MagnitudeConjecture.CoveringHom.shiftOrbitDescendHomogeneousMap_comp {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.CommShift A] {X Y Z : C} {a b : A} (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : shiftOrbitDescendHomogeneousMap F (b + a) (shiftHomComp f g) = shiftHomComp (shiftOrbitDescendHomogeneousMap F a f) (shiftOrbitDescendHomogeneousMap F b g)

def MagnitudeConjecture.CoveringHom.shiftOrbitDescendHomogeneousLinearMap {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] {X Y : C} (a : A) : ShiftHom X Y a →ₗ[k] ShiftHom (F.obj X) (F.obj Y) a

The homogeneous action of a shift-compatible linear functor is linear.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitDescendHomogeneousLinearEquiv {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] [F.Full] [F.Faithful] (X Y : C) (a : A) : ShiftHom X Y a ≃ₗ[k] ShiftHom (F.obj X) (F.obj Y) a

A full and faithful shift-compatible linear functor gives a linear equivalence on every homogeneous shifted Hom module.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitMapHomLinearEquiv {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] [F.Full] [F.Faithful] (X Y : C) : ShiftOrbitHom A X Y ≃ₗ[k] ShiftOrbitHom A (F.obj X) (F.obj Y)

The induced map on shift-orbit Hom modules is a linear equivalence when the original functor is full and faithful.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitDescendMapLinear {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] {X Y : C} : ShiftOrbitHom A X Y →ₗ[k] ShiftOrbitHom A (F.obj X) (F.obj Y)

The induced linear map on finite-support shift-orbit morphisms.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitDescendMapLinear_of {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] {X Y : C} (a : A) (f : ShiftHom X Y a) : (shiftOrbitDescendMapLinear F) ((shiftOrbitOf X Y a) f) = (shiftOrbitOf (F.obj X) (F.obj Y) a) (shiftOrbitDescendHomogeneousMap F a f)

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitMapHomLinearEquiv_apply {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] [F.Full] [F.Faithful] {X Y : C} (f : ShiftOrbitHom A X Y) : (shiftOrbitMapHomLinearEquiv F X Y) f = (shiftOrbitDescendMapLinear F) f

theorem MagnitudeConjecture.CoveringHom.shiftOrbitDescendMapLinear_comp {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), (CategoryTheory.shiftFunctor E a).Additive] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] {X Y Z : C} (f : ShiftOrbitHom A X Y) (g : ShiftOrbitHom A Y Z) : (shiftOrbitDescendMapLinear F) ((shiftOrbitCompHom f) g) = (shiftOrbitCompHom ((shiftOrbitDescendMapLinear F) f)) ((shiftOrbitDescendMapLinear F) g)

The induced map respects finite-support convolution.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitMapFunctor {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), (CategoryTheory.shiftFunctor E a).Additive] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] : CategoryTheory.Functor (ShiftOrbitCategory C A) (ShiftOrbitCategory E A)

A shift-compatible linear functor induces a linear functor between its source and target shift-orbit categories.

instance MagnitudeConjecture.CoveringHom.shiftOrbitMapFunctor_additive {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), (CategoryTheory.shiftFunctor E a).Additive] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] : (shiftOrbitMapFunctor F).Additive

instance MagnitudeConjecture.CoveringHom.shiftOrbitMapFunctor_linear {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] [∀ (a : A), (CategoryTheory.shiftFunctor E a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor E a)] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] : CategoryTheory.Functor.Linear k (shiftOrbitMapFunctor F)

instance MagnitudeConjecture.CoveringHom.shiftOrbitMapFunctor_full {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), (CategoryTheory.shiftFunctor E a).Additive] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] [F.Full] [F.Faithful] : (shiftOrbitMapFunctor F).Full

instance MagnitudeConjecture.CoveringHom.shiftOrbitMapFunctor_faithful {k : Type uK} [CommSemiring k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] [CategoryTheory.Preadditive C] {E : Type uD} [CategoryTheory.Category.{vD, uD} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k C] [CategoryTheory.Linear k E] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift E A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), (CategoryTheory.shiftFunctor E a).Additive] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.CommShift A] [F.Full] [F.Faithful] : (shiftOrbitMapFunctor F).Faithful

@[instance_reducible]

def MagnitudeConjecture.CoveringHom.instHasShift_magnitudeConjecture {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] : CategoryTheory.HasShift T A

theorem MagnitudeConjecture.CoveringHom.instAdditiveShiftFunctor_magnitudeConjecture {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] (a : A) : (CategoryTheory.shiftFunctor T a).Additive

theorem MagnitudeConjecture.CoveringHom.instLinearShiftFunctor_magnitudeConjecture {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] (a : A) : CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor T a)

def MagnitudeConjecture.CoveringHom.trivialShiftHomLinearMap {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] (X Y : T) (a : A) : ShiftHom X Y a →ₗ[k] X ⟶ Y

In a trivially shifted category, a degree-indexed shifted morphism is an ordinary morphism.

@[simp]

theorem MagnitudeConjecture.CoveringHom.trivialShiftHomLinearMap_id {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] (X : T) : (trivialShiftHomLinearMap X X 0) (shiftHomId X) = CategoryTheory.CategoryStruct.id X

theorem MagnitudeConjecture.CoveringHom.trivialShiftHomLinearMap_comp {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] {X Y Z : T} {a b : A} (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : (trivialShiftHomLinearMap X Z (b + a)) (shiftHomComp f g) = CategoryTheory.CategoryStruct.comp ((trivialShiftHomLinearMap X Y a) f) ((trivialShiftHomLinearMap Y Z b) g)

noncomputable def MagnitudeConjecture.CoveringHom.trivialShiftOrbitFoldMapLinear {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] (X Y : T) : ShiftOrbitHom A X Y →ₗ[k] X ⟶ Y

Sum all finitely many degree components in a trivially shifted target.

@[simp]

theorem MagnitudeConjecture.CoveringHom.trivialShiftOrbitFoldMapLinear_of {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] {X Y : T} (a : A) (f : ShiftHom X Y a) : (trivialShiftOrbitFoldMapLinear X Y) ((shiftOrbitOf X Y a) f) = (trivialShiftHomLinearMap X Y a) f

theorem MagnitudeConjecture.CoveringHom.trivialShiftOrbitFoldMapLinear_comp {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] {X Y Z : T} (f : ShiftOrbitHom A X Y) (g : ShiftOrbitHom A Y Z) : (trivialShiftOrbitFoldMapLinear X Z) ((shiftOrbitCompHom f) g) = CategoryTheory.CategoryStruct.comp ((trivialShiftOrbitFoldMapLinear X Y) f) ((trivialShiftOrbitFoldMapLinear Y Z) g)

noncomputable def MagnitudeConjecture.CoveringHom.trivialShiftOrbitFoldFunctor {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] : CategoryTheory.Functor (ShiftOrbitCategory T A) T

The augmentation of the shift-orbit category of a trivially shifted linear category, obtained by summing its finite degree support.

instance MagnitudeConjecture.CoveringHom.trivialShiftOrbitFoldFunctor_additive {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] : trivialShiftOrbitFoldFunctor.Additive

instance MagnitudeConjecture.CoveringHom.trivialShiftOrbitFoldFunctor_linear {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] : CategoryTheory.Functor.Linear k trivialShiftOrbitFoldFunctor

@[instance_reducible]

def MagnitudeConjecture.CoveringHom.instHasShift_magnitudeConjecture_1 {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] : CategoryTheory.HasShift T A

theorem MagnitudeConjecture.CoveringHom.instAdditiveShiftFunctor_magnitudeConjecture_1 {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] (a : A) : (CategoryTheory.shiftFunctor T a).Additive

theorem MagnitudeConjecture.CoveringHom.instLinearShiftFunctor_magnitudeConjecture_1 {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] (a : A) : CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor T a)

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitDescendedFunctor {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {S : Type uC} [CategoryTheory.Category.{vC, uC} S] [CategoryTheory.Preadditive S] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k S] [CategoryTheory.Linear k T] [CategoryTheory.HasShift S A] [∀ (a : A), (CategoryTheory.shiftFunctor S a).Additive] (G : CategoryTheory.Functor S T) [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift A] : CategoryTheory.Functor (ShiftOrbitCategory S A) T

A shift-compatible linear functor to a trivially shifted target descends to the source shift-orbit category.

instance MagnitudeConjecture.CoveringHom.shiftOrbitDescendedFunctor_additive {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {S : Type uC} [CategoryTheory.Category.{vC, uC} S] [CategoryTheory.Preadditive S] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k S] [CategoryTheory.Linear k T] [CategoryTheory.HasShift S A] [∀ (a : A), (CategoryTheory.shiftFunctor S a).Additive] (G : CategoryTheory.Functor S T) [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift A] : (shiftOrbitDescendedFunctor G).Additive

instance MagnitudeConjecture.CoveringHom.shiftOrbitDescendedFunctor_linear {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {S : Type uC} [CategoryTheory.Category.{vC, uC} S] [CategoryTheory.Preadditive S] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k S] [CategoryTheory.Linear k T] [CategoryTheory.HasShift S A] [∀ (a : A), (CategoryTheory.shiftFunctor S a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor S a)] (G : CategoryTheory.Functor S T) [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift A] : CategoryTheory.Functor.Linear k (shiftOrbitDescendedFunctor G)

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitDescendedFunctor_map_of {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {S : Type uC} [CategoryTheory.Category.{vC, uC} S] [CategoryTheory.Preadditive S] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k S] [CategoryTheory.Linear k T] [CategoryTheory.HasShift S A] [∀ (a : A), (CategoryTheory.shiftFunctor S a).Additive] (G : CategoryTheory.Functor S T) [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift A] {X Y : S} (a : A) (f : ShiftHom X Y a) : (shiftOrbitDescendedFunctor G).map ((shiftOrbitOf X Y a) f) = shiftOrbitDescendHomogeneousMap G a f

theorem MagnitudeConjecture.CoveringHom.shiftOrbitDescendedFunctor_map_identityComponent {k : Type uK} [CommSemiring k] {A : Type w} [AddMonoid A] {S : Type uC} [CategoryTheory.Category.{vC, uC} S] [CategoryTheory.Preadditive S] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k S] [CategoryTheory.Linear k T] [CategoryTheory.HasShift S A] [∀ (a : A), (CategoryTheory.shiftFunctor S a).Additive] (G : CategoryTheory.Functor S T) [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift A] {X Y : S} (f : X ⟶ Y) : (shiftOrbitDescendedFunctor G).map (ShiftOrbitCategory.identityComponentFunctor.map f) = G.map f

The descended functor restricts along the degree-zero inclusion to the original shift-compatible functor.

@[instance_reducible]

def MagnitudeConjecture.CoveringHom.instHasShift_magnitudeConjecture_2 {T : Type uD} [CategoryTheory.Category.{vD, uD} T] {B : Type w} [AddGroup B] : CategoryTheory.HasShift T B

theorem MagnitudeConjecture.CoveringHom.instAdditiveShiftFunctor_magnitudeConjecture_2 {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] {B : Type w} [AddGroup B] (b : B) : (CategoryTheory.shiftFunctor T b).Additive

theorem MagnitudeConjecture.CoveringHom.instLinearShiftFunctor_magnitudeConjecture_2 {k : Type uK} [CommSemiring k] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k T] {B : Type w} [AddGroup B] (b : B) : CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor T b)

theorem MagnitudeConjecture.CoveringHom.shiftOrbitDescendedFunctor_map_fromShift {k : Type uK} [CommSemiring k] {S : Type uC} [CategoryTheory.Category.{vC, uC} S] [CategoryTheory.Preadditive S] {T : Type uD} [CategoryTheory.Category.{vD, uD} T] [CategoryTheory.Preadditive T] [CategoryTheory.Linear k S] [CategoryTheory.Linear k T] {B : Type w} [AddGroup B] [CategoryTheory.HasShift S B] [∀ (b : B), (CategoryTheory.shiftFunctor S b).Additive] (G : CategoryTheory.Functor S T) [G.Additive] [CategoryTheory.Functor.Linear k G] [G.CommShift B] (X : S) (b : B) : (shiftOrbitDescendedFunctor G).map (shiftOrbitFromShift X b) = (CategoryTheory.Functor.commShiftIso G b).hom.app X

The descended functor sends the canonical path from a shifted object to the corresponding commutation isomorphism.

theorem MagnitudeConjecture.CoveringHom.linearModuleCategoryAdditiveShift {R : Type uK} [CommRing R] {B : Type uC} [CategoryTheory.Category.{vC, uC} B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear R B] {H : Type w} [AddGroup H] (D : CategoryTheory.ShiftMkCore B H) [∀ (a : H), (D.F a).Additive] [∀ (a : H), CategoryTheory.Functor.Linear R (D.F a)] (a : H) : (CategoryTheory.shiftFunctor (LinearModuleCategory R) a).Additive

The induced shifts on linear modules are additive.

theorem MagnitudeConjecture.CoveringHom.linearModuleCategoryLinearShift {R : Type uK} [CommRing R] {B : Type uC} [CategoryTheory.Category.{vC, uC} B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear R B] {H : Type w} [AddGroup H] (D : CategoryTheory.ShiftMkCore B H) [∀ (a : H), (D.F a).Additive] [∀ (a : H), CategoryTheory.Functor.Linear R (D.F a)] (a : H) : CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (LinearModuleCategory R) a)

The induced shifts on linear modules are linear.

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDescended {R : Type uK} [CommRing R] {B : Type uC} [CategoryTheory.Category.{vC, uC} B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear R B] {H : Type w} [AddGroup H] (D : CategoryTheory.ShiftMkCore B H) [∀ (a : H), (D.F a).Additive] [∀ (a : H), CategoryTheory.Functor.Linear R (D.F a)] : CategoryTheory.Functor (ShiftOrbitCategory (LinearModuleCategory R) H) (LinearModuleCategory R)

Gabriel push-down descended from the shift-orbit category of upstairs linear modules to linear modules on the base orbit category.

@[simp]

theorem MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDescended_map_of {R : Type uK} [CommRing R] {B : Type uC} [CategoryTheory.Category.{vC, uC} B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear R B] {H : Type w} [AddGroup H] (D : CategoryTheory.ShiftMkCore B H) [∀ (a : H), (D.F a).Additive] [∀ (a : H), CategoryTheory.Functor.Linear R (D.F a)] (M N : LinearModuleCategory R) (a : H) (f : ShiftHom M N a) : (linearModuleOrbitPushdownDescended D).map ((shiftOrbitOf M N a) f) = CategoryTheory.CategoryStruct.comp (linearModuleOrbitPushdown.map f) ((linearModuleOrbitPushdownCommShiftIso D a).hom.app N)

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDescended_additive {R : Type uK} [CommRing R] {B : Type uC} [CategoryTheory.Category.{vC, uC} B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear R B] {H : Type w} [AddGroup H] (D : CategoryTheory.ShiftMkCore B H) [∀ (a : H), (D.F a).Additive] [∀ (a : H), CategoryTheory.Functor.Linear R (D.F a)] : (linearModuleOrbitPushdownDescended D).Additive

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDescended_linear {R : Type uK} [CommRing R] {B : Type uC} [CategoryTheory.Category.{vC, uC} B] [CategoryTheory.Preadditive B] [CategoryTheory.Linear R B] {H : Type w} [AddGroup H] (D : CategoryTheory.ShiftMkCore B H) [∀ (a : H), (D.F a).Additive] [∀ (a : H), CategoryTheory.Functor.Linear R (D.F a)] : CategoryTheory.Functor.Linear R (linearModuleOrbitPushdownDescended D)