Magnitude conjecture

MagnitudeConjecture.CategoryTheory.DeckOrbitTowerEquivalence

Equivalence for strict orbit towers #

For a normal subgroup N ◁ G, flattening the residual strict orbit skeleton followed by the N-orbit skeleton gives the direct strict G-orbit skeleton. The flattening functor is full, faithful, and essentially surjective, hence an equivalence.

source
noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualFlattenRepresentativeNatIso {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.deckOrbitResidualFlattenFunctor N).comp deckOrbitRepresentativeFunctor ≅ (shiftOrbitMapFunctor deckOrbitRepresentativeFunctor).comp (D.shiftOrbitResidualFlattenFunctor N)

Residual strict flattening followed by the ambient representative inclusion agrees naturally with nonskeletal residual flattening after mapping the subgroup representative inclusion through the residual orbit category.

Instances For
    source
    instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualFlattenFunctor_full {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.deckOrbitResidualFlattenFunctor N).Full

    Strict residual flattening is full.

    source
    instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitResidualFlattenFunctor_faithful {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.deckOrbitResidualFlattenFunctor N).Faithful

    Strict residual flattening is faithful.

    source
    instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFlattenFunctor_full {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).Full

    The strict orbit-tower flattening functor is full.

    source
    instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFlattenFunctor_faithful {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).Faithful

    The strict orbit-tower flattening functor is faithful.

    source
    instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFlattenFunctor_essSurj {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).EssSurj

    The strict orbit-tower flattening functor is essentially surjective.

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

    The two-stage strict orbit skeleton for N and G / N is equivalent to the direct strict G-orbit skeleton.

    Instances For