Residual shifts on the strict linear module category

The strict residual shift functors are linear. Their coherent core therefore induces inverse-precomposition shifts on linear modules over the deck-orbit skeleton. Degree a on modules evaluates by the strict orbit translation in degree -a.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCore_linear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] {k : Type uK} [CommRing k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (a : Additive (G ⧸ N)) : CategoryTheory.Functor.Linear k ((D.deckOrbitResidualCore N).F a)

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCoherentDeckShift_core_linear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] {k : Type uK} [CommRing k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (a : Additive (G ⧸ N)) : CategoryTheory.Functor.Linear k ((D.deckOrbitResidualCoherentDeckShift N).core.F a)

The linear structure on the residual core is visible through its packaged coherent deck shift.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualLinearShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] {k : Type uK} [CommRing k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (a : Additive (G ⧸ N)) : CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor (DeckOrbitSkeleton C ↥N) a)

Every strict residual shift functor is linear.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualLinearModuleHasShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] {k : Type uK} [CommRing k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] : CategoryTheory.HasShift (LinearModuleCategory k) (Additive (G ⧸ N))

The residual quotient group acts coherently on linear modules over the strict deck-orbit skeleton by inverse precomposition.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualLinearModuleShiftUnderlyingIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] {k : Type uK} [CommRing k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (M : LinearModuleCategory k) (a : Additive (G ⧸ N)) : (IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M) ≅ ((D.deckOrbitResidualCore N).F (-a)).comp M.obj

Forgetting the linear-module subtype identifies residual degree a with inverse precomposition by strict residual degree -a.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualLinearModuleShiftEvaluationIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] {k : Type uK} [CommRing k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (M : LinearModuleCategory k) (a : Additive (G ⧸ N)) (q : MulAction.orbitRel.Quotient (↥N) C) : ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory a).obj M)).obj q ≅ M.obj.obj ((D.deckOrbitNormalTranslateFunctor N (normalQuotientRepresentative N (Additive.toMul (-a)))).obj q)

Evaluation of the residual module shift is inverse precomposition by the strict deck-orbit translation in degree -a.