Residual descent on strict deck-orbit skeletons

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

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSubgroupRepresentativeNatIso {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) : deckOrbitRepresentativeFunctor.comp (D.shiftOrbitSubgroupFunctor N) ≅ (D.deckOrbitSubgroupFunctor N).comp deckOrbitRepresentativeFunctor

The strict and nonskeletal subgroup functors commute with their representative inclusions.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSubgroupFunctor_linear {k : Type uK} [CommRing 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.deckOrbitSubgroupFunctor N)

Passing from the strict subgroup orbit skeleton to the strict ambient orbit skeleton is linear.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSubgroupResidualCommShift {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.deckOrbitSubgroupFunctor N).CommShift (Additive (G ⧸ N))

The strict subgroup orbit functor commutes coherently with residual quotient shifts when the strict ambient orbit skeleton is trivially shifted.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualFlattenFunctor {k : Type uK} [CommRing 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 (DeckOrbitSkeleton C ↥N) (Additive (G ⧸ N))) (DeckOrbitSkeleton C G)

Residual descent of the strict subgroup orbit functor.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualFlattenFunctor_additive {k : Type uK} [CommRing 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.deckOrbitResidualFlattenFunctor N).Additive

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualFlattenFunctor_linear {k : Type uK} [CommRing 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.deckOrbitResidualFlattenFunctor N)