Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ShiftOrbitSubgroupFunctor

Functors between subgroup shift-orbit categories #

A coherent deck action of G restricts to every subgroup N. Extending a finitely supported N-graded orbit morphism by zero outside N gives a canonical additive functor from the N shift-orbit category to the G shift-orbit category.

source
noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (N : Subgroup G) (X Y : C) :
ShiftOrbitHom (Additive ↥N) X Y →+ ShiftOrbitHom (Additive G) X Y

Extend a finitely supported N-orbit morphism by zero to a G-orbit morphism.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_of {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 Y : C) (a : Additive ↥N) (f : ShiftHom X Y a) :
    (D.shiftOrbitSubgroupMap N X Y) ((shiftOrbitOf X Y a) f) = (shiftOrbitOf X Y (MagnitudeConjecture.CoveringHom.CoherentDeckShift.subgroupDegree✝ N a)) (MagnitudeConjecture.CoveringHom.CoherentDeckShift.subgroupShiftHom✝ D N X Y a f)
    source
    theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_id {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.shiftOrbitSubgroupMap N X X) (shiftOrbitId X) = shiftOrbitId X
    source
    theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_comp {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 Y Z : C} (f : ShiftOrbitHom (Additive ↥N) X Y) (g : ShiftOrbitHom (Additive ↥N) Y Z) :
    (D.shiftOrbitSubgroupMap N X Z) ((shiftOrbitCompHom f) g) = (shiftOrbitCompHom ((D.shiftOrbitSubgroupMap N X Y) f)) ((D.shiftOrbitSubgroupMap N Y Z) g)
    source
    noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupFunctor {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 (ShiftOrbitCategory C (Additive ↥N)) (ShiftOrbitCategory C (Additive G))

    The canonical inclusion of the subgroup shift-orbit category into the ambient shift-orbit category.

    Instances For
      source
      instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupFunctor_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.shiftOrbitSubgroupFunctor N).Additive