The coherent residual deck shift

For a normal subgroup N ◁ G, the strict residual shift on the chosen N-orbit skeleton is compatible with the canonical G / N action on N-orbits. This packages that shift core and object identification as a CoherentDeckShift for the quotient group.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCore_obj_eq_inv_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] (N : Subgroup G) [N.Normal] (q : G ⧸ N) (X : DeckOrbitSkeleton C ↥N) : ((D.deckOrbitResidualCore N).F (Additive.ofMul q)).obj X = q⁻¹ • X

On objects, strict residual degree q is inverse translation by the quotient action.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCoherentDeckShift {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] : CoherentDeckShift (DeckOrbitSkeleton C ↥N) (G ⧸ N)

The strict residual core, together with the quotient action on orbit objects, is a coherent deck shift by G / N.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCoherentDeckShift_hasShift_eq {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.deckOrbitResidualCoherentDeckShift N).hasShift = D.deckOrbitResidualHasShift N

The shift exported by the coherent residual deck package is the already constructed transported residual shift.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualIsCancelSMul {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] [IsCancelSMul G C] (N : Subgroup G) [N.Normal] : IsCancelSMul (G ⧸ N) (DeckOrbitSkeleton C ↥N)

Freeness of the ambient action descends to the canonical residual action on the strict subgroup-orbit skeleton.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualCoherentDeckShift_core_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] (a : Additive (G ⧸ N)) : ((D.deckOrbitResidualCoherentDeckShift N).core.F a).Additive

The additive structure on the residual core is visible through its packaged coherent deck shift.