Residual quotient translations of a normal-subgroup orbit category

Let N ◁ G. A chosen representative of each coset in G / N determines an ambient translation functor of the N-shift-orbit category. This file constructs the residual unit and product isomorphisms. They combine the canonical coset-comparison isomorphisms with the coherent unit and product isomorphisms for fixed ambient translations.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalQuotientRepresentative {G : Type w} [Group G] (N : Subgroup G) (q : G ⧸ N) : G

The representative of a quotient-group element used by the residual translation construction.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalQuotientRepresentative_mk {G : Type w} [Group G] (N : Subgroup G) (q : G ⧸ N) : ↑(normalQuotientRepresentative N q) = q

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalQuotientRepresentative_one_eq {G : Type w} [Group G] (N : Subgroup G) [N.Normal] : ↑(normalQuotientRepresentative N 1) = ↑1

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalQuotientRepresentative_mul_eq {G : Type w} [Group G] (N : Subgroup G) [N.Normal] (q r : G ⧸ N) : ↑(normalQuotientRepresentative N (q * r)) = ↑(normalQuotientRepresentative N q * normalQuotientRepresentative N r)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualUnitIso {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 (normalQuotientRepresentative N 1) ≅ CategoryTheory.Functor.id (ShiftOrbitCategory C (Additive ↥N))

The residual translation at the identity coset is isomorphic to the identity functor.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualAddIso {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] (q r : G ⧸ N) : D.shiftOrbitNormalTranslateFunctor N (normalQuotientRepresentative N (q * r)) ≅ (D.shiftOrbitNormalTranslateFunctor N (normalQuotientRepresentative N q)).comp (D.shiftOrbitNormalTranslateFunctor N (normalQuotientRepresentative N r))

The residual translation at a product coset is isomorphic to the composite residual translations at its two factors.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_residualUnitHom {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 (normalQuotientRepresentative N 1))).obj X) X) ((D.shiftOrbitResidualUnitIso N).hom.app (have this := X; this)) = (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul (normalQuotientRepresentative N 1))).inv

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_residualUnitInv {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 (normalQuotientRepresentative N 1))).obj X)) ((D.shiftOrbitResidualUnitIso N).inv.app (have this := X; this)) = (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul (normalQuotientRepresentative N 1))).hom

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_residualAddHom {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] (q r : G ⧸ N) (X : C) : (D.shiftOrbitSubgroupMap N ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (q * r)))).obj X) ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N r))).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N q))).obj X))) ((D.shiftOrbitResidualAddIso N q r).hom.app (have this := X; this)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul (normalQuotientRepresentative N (q * r)))).inv (ShiftOrbitCategory.objectShiftIso X (Additive.ofMul (normalQuotientRepresentative N q))).hom) (ShiftOrbitCategory.objectShiftIso ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N q))).obj X) (Additive.ofMul (normalQuotientRepresentative N r))).hom