The residual quotient-group shift

For N ◁ G, the chosen G / N-representative translations of the N-shift-orbit category satisfy the two unit laws and associativity. They therefore define a coherent shift indexed by Additive (G / N).

The proofs use the canonical-path formulas from ShiftOrbitResidualTranslate. Faithful inclusion into the full G-orbit category reduces every coherence equation to cancellation of object-shift isomorphisms and dependent congruence along a quotient-group law.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualCore {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 (ShiftOrbitCategory C (Additive ↥N)) (Additive (G ⧸ N))

The coherent residual G / N-indexed translation core on the N-shift-orbit category.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualHasShift {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 (ShiftOrbitCategory C (Additive ↥N)) (Additive (G ⧸ N))

The residual G / N shift on the N-shift-orbit category.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualAdditiveShift {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).Additive

Every functor in the residual quotient shift is additive.