Translation invariance of Gabriel push-down

The push-down of a translated module is canonically isomorphic to the push-down of the original module. For a possibly noncommutative additive group, the b-summand of the translated push-down is reindexed as the (b-a)-summand of the original push-down. Shift associativity proves that this right reindexing commutes with the left degree translation used by orbit morphisms.

noncomputable def MagnitudeConjecture.CoveringHom.directSumAddRightEquiv {R : Type uK} [Semiring R] {B : Type w} [AddGroup B] (V : B → Type uM) [(b : B) → AddCommMonoid (V b)] [(b : B) → Module R (V b)] (a : B) : (DirectSum B fun (b : B) => V (b + -a)) ≃ₗ[R] DirectSum B fun (b : B) => V b

Reindex a direct sum by right subtraction in an additive group.

@[simp]

theorem MagnitudeConjecture.CoveringHom.directSumAddRightEquiv_lof {R : Type uK} [Semiring R] {B : Type w} [AddGroup B] (V : B → Type uM) [(b : B) → AddCommMonoid (V b)] [(b : B) → Module R (V b)] [DecidableEq B] (a b : B) (x : V (b + -a)) : (directSumAddRightEquiv V a) ((DirectSum.lof R B (fun (c : B) => V (c + -a)) b) x) = (DirectSum.lof R B (fun (c : B) => V c) (b + -a)) x

theorem MagnitudeConjecture.CoveringHom.shiftMkCoreAdditiveShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] (a : A) : (CategoryTheory.shiftFunctor C a).Additive

A shift constructed from an additive ShiftMkCore has additive shift functors.

theorem MagnitudeConjecture.CoveringHom.shiftMkCoreLinearShift {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (a : A) : CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)

A shift constructed from a linear ShiftMkCore has linear shift functors.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownArrow_shift_reindex {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) {X Y : C} (a c b : A) (f : ShiftHom X Y c) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (-a)).map (orbitPushdownArrow' ⋯ f)) ((CategoryTheory.shiftFunctorAdd' C (c + b) (-a) (c + b + -a) ⋯).inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b (-a) (b + -a) ⋯).inv.app X) (orbitPushdownArrow' ⋯ f)

Shift associativity is exactly the arrow compatibility needed by the right-reindexing of push-down summands.

noncomputable def MagnitudeConjecture.CoveringHom.shiftedOrbitSummandEquiv {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M : LinearModuleCategory k) (a b : A) (X : C) : ↑(((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)).obj ((D.F b).obj X)) ≃ₗ[k] ↑(M.obj.obj ((D.F (b + -a)).obj X))

The value of a shifted module at the b-translated object is the (b-a)-translated value of the original module.

noncomputable def MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownValueEquiv {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M : LinearModuleCategory k) (a : A) (X : C) : orbitPushdownValue ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)) X ≃ₗ[k] orbitPushdownValue M.obj X

Objectwise reindexing isomorphism between the push-down of a shift and the push-down of the original module.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownValueEquiv_lof {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M : LinearModuleCategory k) (a b : A) (X : C) (x : ↑(((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)).obj ((D.F b).obj X))) : (shiftedOrbitPushdownValueEquiv D M a X) ((orbitPushdownLof ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)) X b) x) = (orbitPushdownLof M.obj X (b + -a)) ((shiftedOrbitSummandEquiv D M a b X) x)

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitComponent_reindex {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M : LinearModuleCategory k) {X Y : C} (a c b : A) (f : ShiftHom X Y c) : ↑(shiftedOrbitSummandEquiv D M a (c + b) Y) ∘ₗ orbitPushdownComponent ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)) c b f = orbitPushdownComponent' M.obj ⋯ f ∘ₗ ↑(shiftedOrbitSummandEquiv D M a b X)

The summand reindexing intertwines a homogeneous push-down component.

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownValueEquiv_naturality_homogeneous {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M : LinearModuleCategory k) {X Y : C} (a c : A) (f : ShiftHom X Y c) : ↑(shiftedOrbitPushdownValueEquiv D M a Y) ∘ₗ orbitPushdownHomogeneousMap ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)) c f = orbitPushdownHomogeneousMap M.obj c f ∘ₗ ↑(shiftedOrbitPushdownValueEquiv D M a X)

The value reindexing commutes with each homogeneous morphism in the shift-orbit category.

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownValueEquiv_naturality {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M : LinearModuleCategory k) {X Y : C} (a : A) (f : ShiftOrbitHom A X Y) : ↑(shiftedOrbitPushdownValueEquiv D M a Y) ∘ₗ (orbitPushdownMapLinear ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M))) f = (orbitPushdownMapLinear M.obj) f ∘ₗ ↑(shiftedOrbitPushdownValueEquiv D M a X)

The value reindexing is natural for every finite-support orbit morphism.

noncomputable def MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownIso {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] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] (M : LinearModuleCategory k) (a : A) : orbitPushdown ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)) ≅ orbitPushdown M.obj

Push-down is invariant under translating the upstairs module.