Linearity of normal deck-orbit translations

Ambient normal translations preserve scalar multiplication on both the nonskeletal shift-orbit category and its chosen strict deck-orbit skeleton. The proof first checks subgroup-degree inclusion on direct-sum generators, then uses its injectivity to descend linearity from ambient conjugation.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_smul {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] {k : Type uK} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) {X Y : C} (r : k) (f : ShiftOrbitHom (Additive ↥N) X Y) : (D.shiftOrbitSubgroupMap N X Y) (r • f) = r • (D.shiftOrbitSubgroupMap N X Y) f

Extending subgroup-graded orbit morphisms by zero preserves scalar multiplication.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMap_smul {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] {k : Type uK} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (g : G) {X Y : C} (r : k) (f : ShiftOrbitHom (Additive ↥N) X Y) : D.shiftOrbitNormalTranslateMap N g (r • f) = r • D.shiftOrbitNormalTranslateMap N g f

Normal translation on the nonskeletal orbit Hom preserves scalar multiplication.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateFunctor_linear {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] {k : Type uK} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (g : G) : CategoryTheory.Functor.Linear k (D.shiftOrbitNormalTranslateFunctor N g)

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateMap_smul {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] {k : Type uK} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (g : G) {q s : MulAction.orbitRel.Quotient (↥N) C} (r : k) (f : (have this := q; this) ⟶ have this := s; this) : D.deckOrbitNormalTranslateMap N g (r • f) = r • D.deckOrbitNormalTranslateMap N g f

Strict normal translation on the deck-orbit skeleton preserves scalar multiplication.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitNormalTranslateFunctor_linear {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] {k : Type uK} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (g : G) : CategoryTheory.Functor.Linear k (D.deckOrbitNormalTranslateFunctor N g)