Ambient translations on a normal deck-orbit skeleton

For a normal subgroup N ◁ G, every ambient element g : G inverse-translates the strict N-orbit of an object. This file upgrades that object operation to an additive endofunctor of the chosen deck-orbit skeleton. On morphisms it uses the normal translation of the nonskeletal N-shift-orbit category, conjugated by the canonical isomorphisms to the chosen orbit representatives.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateRepresentativeIso {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) (q : MulAction.orbitRel.Quotient (↥N) C) : (D.shiftOrbitNormalTranslateFunctor N g).obj (deckOrbitRepresentative q) ≅ deckOrbitRepresentative (MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalTranslateOrbitObject✝ N g q)

The fixed ambient shift of a chosen N-orbit representative is isomorphic in the N-orbit category to the representative of the inverse translated strict orbit.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateMap {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) {q r : MulAction.orbitRel.Quotient (↥N) C} (f : (have this := q; this) ⟶ have this := r; this) : (have this := MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalTranslateOrbitObject✝ N g q; this) ⟶ have this := MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalTranslateOrbitObject✝ N g r; this

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateFunctor {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) : CategoryTheory.Functor (DeckOrbitSkeleton C ↥N) (DeckOrbitSkeleton C ↥N)

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateMap_add {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) {q r : MulAction.orbitRel.Quotient (↥N) C} (f h : (have this := q; this) ⟶ have this := r; this) : D.deckOrbitNormalTranslateMap N g (f + h) = D.deckOrbitNormalTranslateMap N g f + D.deckOrbitNormalTranslateMap N g h

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateFunctor_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] (g : G) : (D.deckOrbitNormalTranslateFunctor N g).Additive