The residual shift on the strict deck-orbit skeleton

For N ◁ G, the residual G / N-shift on the nonskeletal N-shift-orbit category transports to the chosen deck-orbit skeleton. Its degree-q functor is literally the fixed strict translation by the chosen representative Quotient.out q; the coherence is transported through the fully faithful representative functor.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateRepresentativeNatIso {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] (g : G) : (D.deckOrbitNormalTranslateFunctor N g).comp deckOrbitRepresentativeFunctor ≅ deckOrbitRepresentativeFunctor.comp (D.shiftOrbitNormalTranslateFunctor N g)

Strict normal translation intertwines the representative inclusion with normal translation on the nonskeletal orbit category.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualIntertwiningIso {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)) : (D.deckOrbitNormalTranslateFunctor N (normalQuotientRepresentative N (Additive.toMul a))).comp deckOrbitRepresentativeFunctor ≅ deckOrbitRepresentativeFunctor.comp (CategoryTheory.shiftFunctor (ShiftOrbitCategory C (Additive ↥N)) a)

The strict normal translation by the chosen representative of a quotient degree intertwines the representative inclusion with the residual shift.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCore {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] : CategoryTheory.ShiftMkCore (DeckOrbitSkeleton C ↥N) (Additive (G ⧸ N))

The coherent residual G / N-translation core on the strict deck-orbit skeleton.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualHasShift {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] : CategoryTheory.HasShift (DeckOrbitSkeleton C ↥N) (Additive (G ⧸ N))

The residual G / N-shift on the strict deck-orbit skeleton.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.hasShiftMk_deckOrbitResidualCore_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) [N.Normal] : CategoryTheory.hasShiftMk (DeckOrbitSkeleton C ↥N) (Additive (G ⧸ N)) (D.deckOrbitResidualCore N) = D.deckOrbitResidualHasShift N

Rebuilding the transported residual shift from its exported coherent core does not change the HasShift instance. This is the controlled comparison used when a construction needs both the transport and coherent-deck APIs.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeResidualCommShift {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] : deckOrbitRepresentativeFunctor.CommShift (Additive (G ⧸ N))

The representative inclusion intertwines the strict residual shift with the nonskeletal residual shift, including zero and addition coherence.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCore_additive {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)) : ((D.deckOrbitResidualCore N).F a).Additive

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualAdditiveShift {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 (DeckOrbitSkeleton C ↥N) a).Additive

Every strict residual shift functor is additive.