Coherent ambient shifts on a normal-subgroup orbit category

For a normal subgroup N ≤ G, the ambient translations of the N-shift-orbit category form a coherent shift indexed by Additive G. The unit and product constraints are the canonical projected paths constructed in ShiftOrbitNormalTranslateUnitMul.

The coherence proof is checked after applying the faithful inclusion into the full G-orbit category. There it reduces to cancellation of canonical object-shift isomorphisms and the equality transports for the group unit and associativity laws.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateCore {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)

The coherent G-indexed ambient translation core on the N-orbit category. Elements of N are not yet quotiented from the index here.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateHasShift {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)

The G-indexed ambient translation shift on the N-orbit category.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateAdditiveShift {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) : (CategoryTheory.shiftFunctor (ShiftOrbitCategory C (Additive ↥N)) a).Additive

Every ambient translation in the constructed shift is additive.