Deck translations on linear module categories

Precomposition reverses the order of coherent endofunctor composition. We therefore first construct a shift by the additive opposite group and then reindex it along negation. The shift of a functor M in degree a is literally D.F (-a) ⋙ M.

For a coherent left deck action, degree g on modules consequently has value M (g • X) at X. This is Gabriel's inverse module translate: if his translated module is written gM(X) = M(g⁻¹X), then Mathlib shift degree g is the module g⁻¹M.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.functorPrecomposition {C : Type u} [CategoryTheory.Category.{v, u} C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] (F : CategoryTheory.Functor C C) : CategoryTheory.Functor (CategoryTheory.Functor C E) (CategoryTheory.Functor C E)

Precomposition by an endofunctor, regarded as an endofunctor of a functor category.

def MagnitudeConjecture.CoveringHom.functorPrecompositionIso {C : Type u} [CategoryTheory.Category.{v, u} C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] {F F' : CategoryTheory.Functor C C} (e : F ≅ F') : functorPrecomposition F ≅ functorPrecomposition F'

Precomposition sends an isomorphism of endofunctors to an isomorphism of endofunctors of the functor category.

def MagnitudeConjecture.CoveringHom.functorCategoryOppositeShiftCore {C : Type u} [CategoryTheory.Category.{v, u} C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) : CategoryTheory.ShiftMkCore (CategoryTheory.Functor C E) Aᵃᵒᵖ

Precomposition converts a coherent additive shift on the source into a shift by the additive opposite group on the functor category.

@[implicit_reducible]

def MagnitudeConjecture.CoveringHom.functorCategoryHasShift {C : Type u} [CategoryTheory.Category.{v, u} C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) : CategoryTheory.HasShift (CategoryTheory.Functor C E) A

A coherent shift on C induces inverse-precomposition shifts on the whole functor category C ⥤ E.

theorem MagnitudeConjecture.CoveringHom.functorCategory_shiftFunctor_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) (a : A) : CategoryTheory.shiftFunctor (CategoryTheory.Functor C E) a = functorPrecomposition (D.F (-a))

The induced degree-a shift is literally precomposition by the degree--a source shift.

theorem MagnitudeConjecture.CoveringHom.functorCategory_shiftFunctorZero_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) (M : CategoryTheory.Functor C E) (X : C) : ((CategoryTheory.shiftFunctorZero (CategoryTheory.Functor C E) A).hom.app M).app X ≍ M.map (D.zero.hom.app X)

The zero-shift comparison on the induced functor-category shift is pointwise application of the source zero comparison.

theorem MagnitudeConjecture.CoveringHom.functorCategory_shiftFunctorZero_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] {A : Type w} [AddGroup A] (D : CategoryTheory.ShiftMkCore C A) (M : CategoryTheory.Functor C E) (X : C) : ((CategoryTheory.shiftFunctorZero (CategoryTheory.Functor C E) A).inv.app M).app X ≍ M.map (D.zero.inv.app X)

The inverse zero-shift comparison on the induced functor-category shift is pointwise application of the inverse source zero comparison.

theorem MagnitudeConjecture.CoveringHom.functorCategory_shiftFunctorZero_inv_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (k : Type uK) [CommRing k] (D : CategoryTheory.ShiftMkCore C A) (M : CategoryTheory.Functor C (ModuleCat k)) (X : C) (x : ↑(M.obj X)) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.shiftFunctorZero (CategoryTheory.Functor C (ModuleCat k)) A).inv.app M).app X)) x ≍ (CategoryTheory.ConcreteCategory.hom (M.map (D.zero.inv.app X))) x

Pointwise form of functorCategory_shiftFunctorZero_inv_app, retaining the dependent equality forced by the proof that negation preserves zero.

theorem MagnitudeConjecture.CoveringHom.functorCategory_shiftFunctorZero_inv_add_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (k : Type uK) [CommRing k] (D : CategoryTheory.ShiftMkCore C A) (M : CategoryTheory.Functor C (ModuleCat k)) (c : A) (X : C) (x : ↑(M.obj ((D.F c).obj X))) : (CategoryTheory.ConcreteCategory.hom (M.map ((D.add c (-0)).inv.app X))) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.shiftFunctorZero (CategoryTheory.Functor C (ModuleCat k)) A).inv.app M).app ((D.F c).obj X))) x) ≍ x

The inverse zero comparison for inverse-precomposition shifts cancels the deck reindexing used by orbit push-down.

theorem MagnitudeConjecture.CoveringHom.functorCategory_shiftFunctorAdd_inv_add_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (k : Type uK) [CommRing k] (D : CategoryTheory.ShiftMkCore C A) (M : CategoryTheory.Functor C (ModuleCat k)) (c a b : A) (X : C) (x : ↑(M.obj ((D.F (-a)).obj ((D.F (-b)).obj ((D.F c).obj X))))) : (CategoryTheory.ConcreteCategory.hom (M.map ((D.add c (-(a + b))).inv.app X))) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.shiftFunctorAdd (CategoryTheory.Functor C (ModuleCat k)) a b).inv.app M).app ((D.F c).obj X))) x) ≍ (CategoryTheory.ConcreteCategory.hom (M.map ((D.add (c + -b) (-a)).inv.app X))) ((CategoryTheory.ConcreteCategory.hom (M.map ((D.F (-a)).map ((D.add c (-b)).inv.app X)))) x)

The inverse additive comparison for inverse-precomposition shifts is compatible with the two successive deck reindexings used by orbit push-down.

def MagnitudeConjecture.CoveringHom.IsLinearModule {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.ObjectProperty (CategoryTheory.Functor C (ModuleCat k))

A module over a linear category is a covariant functor to ModuleCat which preserves addition and scalar multiplication.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.LinearModuleCategory {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (max (max (max u uK) v) (u_1 + 1))

The full category of covariant linear modules over C.

instance MagnitudeConjecture.CoveringHom.instAdditiveModuleCatObjFunctorIsLinearModule {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) : M.obj.Additive

instance MagnitudeConjecture.CoveringHom.instLinearModuleCatObjFunctorIsLinearModule {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) : CategoryTheory.Functor.Linear k M.obj

instance MagnitudeConjecture.CoveringHom.instIsClosedUnderIsomorphismsFunctorModuleCatIsLinearModule {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (IsLinearModule k).IsClosedUnderIsomorphisms

instance MagnitudeConjecture.CoveringHom.isLinearModule_stableUnderShift {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] : (IsLinearModule k).IsStableUnderShift A

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleCategoryHasShift {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CategoryTheory.ShiftMkCore C A) [∀ (a : A), (D.F a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)] : CategoryTheory.HasShift (LinearModuleCategory k) A

Coherent inverse-precomposition translation on linear modules.

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleShiftUnderlyingIso {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (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) : (IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M) ≅ (D.F (-a)).comp M.obj

Forgetting linearity identifies the underlying translated module with inverse precomposition.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleShiftEvaluationIso {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (k : Type uK) [CommRing k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (M : LinearModuleCategory k) (g : G) (X : C) : ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory (Additive.ofMul g)).obj M)).obj X ≅ M.obj.obj (g • X)

Degree g on the module category is Gabriel's inverse module translate: its value at X is the original module's value at g • X.