Coset invariance of normal-orbit translations

For a normal subgroup N ◁ G, ambient elements representing the same coset in G / N induce canonically naturally isomorphic translation functors on the N-shift-orbit category. The same comparison is transported to the chosen strict deck-orbit skeleton. These isomorphisms are the descent datum for the residual quotient-group shift.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateEmbeddingIso {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.shiftOrbitNormalTranslateFunctor N g).comp (D.shiftOrbitSubgroupFunctor N) ≅ D.shiftOrbitSubgroupFunctor N

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateComparisonMap {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₂ : G) (_h : ↑g₁ = ↑g₂) (X : C) : ShiftOrbitHom (Additive ↥N) ((CategoryTheory.shiftFunctor C (Additive.ofMul g₁)).obj X) ((CategoryTheory.shiftFunctor C (Additive.ofMul g₂)).obj X)

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_normalTranslateComparisonMap {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₂ : G) (h : ↑g₁ = ↑g₂) (X : C) : (D.shiftOrbitSubgroupMap N ((CategoryTheory.shiftFunctor C (Additive.ofMul g₁)).obj X) ((CategoryTheory.shiftFunctor C (Additive.ofMul g₂)).obj X)) (D.shiftOrbitNormalTranslateComparisonMap N g₁ g₂ h X) = CategoryTheory.CategoryStruct.comp (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul g₁)).inv (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul g₂)).hom

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateIsoOfQuotientEq {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₂ : G) (h : ↑g₁ = ↑g₂) : D.shiftOrbitNormalTranslateFunctor N g₁ ≅ D.shiftOrbitNormalTranslateFunctor N g₂

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateComparisonIsoApp {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₂ : G) (h : ↑g₁ = ↑g₂) (q : MulAction.orbitRel.Quotient (↥N) C) : (D.deckOrbitNormalTranslateFunctor N g₁).obj (have this := q; this) ≅ (D.deckOrbitNormalTranslateFunctor N g₂).obj (have this := q; this)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateIsoOfQuotientEq {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₂ : G) (h : ↑g₁ = ↑g₂) : D.deckOrbitNormalTranslateFunctor N g₁ ≅ D.deckOrbitNormalTranslateFunctor N g₂