Unit and multiplication for normal-orbit translations

Ambient normal-orbit translation by the identity is naturally isomorphic to the identity functor, and translation by a product is naturally isomorphic to the composite translations. The components are projected canonical paths in the full orbit category. Their degrees multiply to the identity, so they lie in every normal subgroup orbit category.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateUnitHom {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] (X : C) : ShiftOrbitHom (Additive ↥N) ((CategoryTheory.shiftFunctor C (Additive.ofMul 1)).obj X) X

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateUnitInv {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] (X : C) : ShiftOrbitHom (Additive ↥N) X ((CategoryTheory.shiftFunctor C (Additive.ofMul 1)).obj X)

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_normalTranslateUnitHom {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] (X : C) : (D.shiftOrbitSubgroupMap N ((CategoryTheory.shiftFunctor C (Additive.ofMul 1)).obj X) X) (D.shiftOrbitNormalTranslateUnitHom N X) = (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul 1)).inv

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_normalTranslateUnitInv {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] (X : C) : (D.shiftOrbitSubgroupMap N X ((CategoryTheory.shiftFunctor C (Additive.ofMul 1)).obj X)) (D.shiftOrbitNormalTranslateUnitInv N X) = (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul 1)).hom

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateUnitIso {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] : D.shiftOrbitNormalTranslateFunctor N 1 ≅ CategoryTheory.Functor.id (ShiftOrbitCategory C (Additive ↥N))

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateUnitIso_hom_app {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] (X : C) : (D.shiftOrbitNormalTranslateUnitIso N).hom.app X = D.shiftOrbitNormalTranslateUnitHom N X

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateUnitIso_inv_app {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] (X : C) : (D.shiftOrbitNormalTranslateUnitIso N).inv.app X = D.shiftOrbitNormalTranslateUnitInv N X

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMulHom {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 h : G) (X : C) : ShiftOrbitHom (Additive ↥N) ((CategoryTheory.shiftFunctor C (Additive.ofMul (g * h))).obj X) ((CategoryTheory.shiftFunctor C (Additive.ofMul h)).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X))

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

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMulInv {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 h : G) (X : C) : ShiftOrbitHom (Additive ↥N) ((CategoryTheory.shiftFunctor C (Additive.ofMul h)).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)) ((CategoryTheory.shiftFunctor C (Additive.ofMul (g * h))).obj X)

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

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMulIso {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 h : G) : D.shiftOrbitNormalTranslateFunctor N (g * h) ≅ (D.shiftOrbitNormalTranslateFunctor N g).comp (D.shiftOrbitNormalTranslateFunctor N h)

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMulIso_hom_app {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 h : G) (X : C) : (D.shiftOrbitNormalTranslateMulIso N g h).hom.app X = D.shiftOrbitNormalTranslateMulHom N g h X

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMulIso_inv_app {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 h : G) (X : C) : (D.shiftOrbitNormalTranslateMulIso N g h).inv.app X = D.shiftOrbitNormalTranslateMulInv N g h X