noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFlattenFunctor
{k : Type uK}
[CommRing k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
[CategoryTheory.Linear k C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)]
(N : Subgroup G)
[N.Normal]
:
CategoryTheory.Functor (DeckOrbitSkeleton (DeckOrbitSkeleton C ↥N) (G ⧸ N)) (DeckOrbitSkeleton C G)
Instances For
instance
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFlattenFunctor_additive
{k : Type uK}
[CommRing k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
[CategoryTheory.Linear k C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)]
(N : Subgroup G)
[N.Normal]
:
(D.deckOrbitTowerFlattenFunctor N).Additive
instance
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFlattenFunctor_linear
{k : Type uK}
[CommRing k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
[CategoryTheory.Linear k C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)]
(N : Subgroup G)
[N.Normal]
:
CategoryTheory.Functor.Linear k (D.deckOrbitTowerFlattenFunctor N)
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFlattenFunctor_obj
{k : Type uK}
[CommRing k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
[CategoryTheory.Linear k C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)]
(N : Subgroup G)
[N.Normal]
(q : MulAction.orbitRel.Quotient (G ⧸ N) (MulAction.orbitRel.Quotient (↥N) C))
:
(D.deckOrbitTowerFlattenFunctor N).obj
(have this := q;
this) = have this := (CoveringAction.orbitTowerEquiv N) q;
this