Orbit push-down commutes with deck translations

The target module category is equipped with the trivial shift. Reindexing direct-sum components then identifies the push-down of a translated module with the original push-down. This file proves naturality and the zero and addition coherence laws, and packages them as a Functor.CommShift structure.

def MagnitudeConjecture.CoveringHom.trivialShiftMkCore (E : Type u) [CategoryTheory.Category.{v, u} E] (A : Type w) [AddMonoid A] : CategoryTheory.ShiftMkCore E A

The coherent trivial shift on a category.

@[implicit_reducible]

def MagnitudeConjecture.CoveringHom.trivialHasShift (E : Type u) [CategoryTheory.Category.{v, u} E] (A : Type w) [AddMonoid A] : CategoryTheory.HasShift E A

A category equipped with the coherent trivial shift.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.trivialFunctorCommShift {B : Type u} [CategoryTheory.Category.{v, u} B] {E : Type uM} [CategoryTheory.Category.{uK, uM} E] {A : Type w} [AddMonoid A] (F : CategoryTheory.Functor B E) : F.CommShift A

Any functor between categories carrying the trivial shift commutes with that shift.

theorem MagnitudeConjecture.CoveringHom.trivialFunctorCommShift_hom_app {B : Type u} [CategoryTheory.Category.{v, u} B] {E : Type uM} [CategoryTheory.Category.{uK, uM} E] {A : Type w} [AddMonoid A] (F : CategoryTheory.Functor B E) (a : A) (X : B) : (CategoryTheory.Functor.commShiftIso F a).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

The commutation map for a functor between trivially shifted categories is the identity on every object.

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitSummandEquiv_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 N : LinearModuleCategory k} (f : M ⟶ N) (a b : A) (X : C) (x : ↑(((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)).obj ((D.F b).obj X))) : (shiftedOrbitSummandEquiv D N a b X) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.shiftFunctor (LinearModuleCategory k) a).map f).hom.app ((D.F b).obj X))) x) = (CategoryTheory.ConcreteCategory.hom (f.hom.app ((D.F (b + -a)).obj X))) ((shiftedOrbitSummandEquiv D M a b X) x)

Reindexing a shifted summand is natural in the linear module.

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownValueEquiv_module_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 N : LinearModuleCategory k} (f : M ⟶ N) (a : A) (X : C) : ↑(shiftedOrbitPushdownValueEquiv D N a X) ∘ₗ orbitPushdownNatTransAppLinear ((CategoryTheory.shiftFunctor (LinearModuleCategory k) a).map f).hom X = orbitPushdownNatTransAppLinear f.hom X ∘ₗ ↑(shiftedOrbitPushdownValueEquiv D M a X)

The direct-sum reindexing is natural in the linear module.

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownCommShiftIso {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)] (a : A) : (CategoryTheory.shiftFunctor (LinearModuleCategory k) a).comp linearModuleOrbitPushdown ≅ linearModuleOrbitPushdown.comp (CategoryTheory.shiftFunctor (LinearModuleCategory k) a)

Push-down commutes with a fixed deck translation, before imposing the zero and addition coherence laws.

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownValueEquiv_zero {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 : C) : ↑(shiftedOrbitPushdownValueEquiv D M 0 X) = orbitPushdownNatTransAppLinear ((CategoryTheory.shiftFunctorZero (LinearModuleCategory k) A).hom.app M).hom X

The push-down translation isomorphism preserves the zero shift.

theorem MagnitudeConjecture.CoveringHom.shiftedOrbitPushdownValueEquiv_add {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) : ↑(shiftedOrbitPushdownValueEquiv D M (a + b) X) = ↑(shiftedOrbitPushdownValueEquiv D M a X) ∘ₗ ↑(shiftedOrbitPushdownValueEquiv D ((CategoryTheory.shiftFunctor (LinearModuleCategory k) a).obj M) b X) ∘ₗ orbitPushdownNatTransAppLinear ((CategoryTheory.shiftFunctorAdd (LinearModuleCategory k) a b).hom.app M).hom X

The push-down translation isomorphisms preserve addition of shifts.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownCommShift {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)] : linearModuleOrbitPushdown.CommShift A

Gabriel orbit push-down commutes coherently with deck translations when the target is equipped with the trivial shift.