Restricting coherent deck shifts to subgroups

A coherent inverse deck-translation action restricts along every subgroup. The restricted ShiftMkCore uses the same ambient shift functors and coherence isomorphisms at the included degrees.

def MagnitudeConjecture.CoveringHom.CoherentDeckShift.restrictCore {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (N : Subgroup G) : CategoryTheory.ShiftMkCore C (Additive ↥N)

Restriction of a coherent shift core along a subgroup inclusion.

def MagnitudeConjecture.CoveringHom.CoherentDeckShift.restrict {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (N : Subgroup G) : CoherentDeckShift C ↥N

Restriction of coherent inverse deck translations to a subgroup.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.restrict_additive {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] (N : Subgroup G) (a : Additive ↥N) : ((D.restrict N).core.F a).Additive

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.restrict_linear {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] {k : Type u_1} [Semiring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) (a : Additive ↥N) : CategoryTheory.Functor.Linear k ((D.restrict N).core.F a)