Residual descent of the subgroup orbit functor

For a normal subgroup N ◁ G, extension by zero from the N-shift-orbit category to the G-shift-orbit category commutes coherently with the residual G / N shift when the target is trivially shifted. It therefore descends through the residual shift-orbit category.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupFunctor_map_eq {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] (N : Subgroup G) {X Y : ShiftOrbitCategory C (Additive ↥N)} (f : X ⟶ Y) : (D.shiftOrbitSubgroupFunctor N).map f = (D.shiftOrbitSubgroupMap N (have this := X; this) (have this := Y; this)) f

The map of the subgroup orbit functor is literally extension by zero in deck degree.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupFunctor_linear {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G 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)] (N : Subgroup G) : CategoryTheory.Functor.Linear k (D.shiftOrbitSubgroupFunctor N)

Extension by zero is a linear functor between the subgroup and ambient shift-orbit categories.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupResidualCommShiftIso {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] (N : Subgroup G) [N.Normal] (a : Additive (G ⧸ N)) : (CategoryTheory.shiftFunctor (ShiftOrbitCategory C (Additive ↥N)) a).comp (D.shiftOrbitSubgroupFunctor N) ≅ (D.shiftOrbitSubgroupFunctor N).comp (CategoryTheory.shiftFunctor (ShiftOrbitCategory C (Additive G)) a)

The subgroup inclusion commutes with a fixed residual quotient shift when the ambient orbit category is given the trivial quotient shift.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupResidualCommShift {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] (N : Subgroup G) [N.Normal] : (D.shiftOrbitSubgroupFunctor N).CommShift (Additive (G ⧸ N))

The residual commutation isomorphisms satisfy the zero and addition coherence laws.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualLinearShift {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G 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)] (N : Subgroup G) [N.Normal] (a : Additive (G ⧸ N)) : CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor (ShiftOrbitCategory C (Additive ↥N)) a)

Every nonskeletal residual shift functor is linear.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenFunctor {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G 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)] (N : Subgroup G) [N.Normal] : CategoryTheory.Functor (ShiftOrbitCategory (ShiftOrbitCategory C (Additive ↥N)) (Additive (G ⧸ N))) (ShiftOrbitCategory C (Additive G))

Extension by zero descends through the residual quotient shift-orbit category to the ambient G-shift-orbit category.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenFunctor_additive {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G 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)] (N : Subgroup G) [N.Normal] : (D.shiftOrbitResidualFlattenFunctor N).Additive

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenFunctor_linear {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G 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)] (N : Subgroup G) [N.Normal] : CategoryTheory.Functor.Linear k (D.shiftOrbitResidualFlattenFunctor N)