Functors between strict deck-orbit skeletons

For a subgroup N ≤ G, the inclusion of shift-orbit morphisms descends to the strict orbit skeletons. On objects the resulting functor is the literal map from an N-orbit to the G-orbit containing it.

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

The morphism on strict orbit skeletons induced by extension from the subgroup shift-orbit category.

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

Passing from the strict N-orbit skeleton to the strict G-orbit skeleton. Its object map sends an N-orbit to the G-orbit containing it.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSubgroupFunctor_obj_mk {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) (X : C) : (D.deckOrbitSubgroupFunctor N).obj (have this := Quotient.mk'' X; this) = have this := Quotient.mk'' X; this

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitTowerEquiv_mk_eq_deckOrbitSubgroupFunctor_obj {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 : MulAction.orbitRel.Quotient (↥N) C) : (CoveringAction.orbitTowerEquiv N) (Quotient.mk'' q) = (D.deckOrbitSubgroupFunctor N).obj (have this := q; this)

The strict-orbit object functor is the flattening map in the orbit-tower equivalence.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSubgroupFunctor_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) : (D.deckOrbitSubgroupFunctor N).Additive