A skeletal base for a coherent deck orbit category

The concrete shift-orbit category retains every upstairs object. This file replaces its object type by the quotient of the strict deck action, chooses one representative of every orbit, and inherits all morphisms from the shift-orbit category between those representatives.

The representative inclusion is fully faithful by construction. For a coherent deck shift it is also essentially surjective, so this induced category is genuinely equivalent to the nonskeletal shift-orbit category. Gabriel push-down and its functorial action on linear modules are then restricted along the representative inclusion.

noncomputable def MagnitudeConjecture.CoveringHom.deckOrbitRepresentative {C : Type u} {G : Type w} [Group G] [MulAction G C] (q : MulAction.orbitRel.Quotient G C) : C

The chosen representative of a strict deck orbit.

@[simp]

theorem MagnitudeConjecture.CoveringHom.deckOrbitRepresentative_mk {C : Type u} {G : Type w} [Group G] [MulAction G C] (q : MulAction.orbitRel.Quotient G C) : Quotient.mk'' (deckOrbitRepresentative q) = q

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.DeckOrbitSkeleton (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (G : Type w) [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] : Type u

One object per strict deck orbit, with morphisms inherited from the shift-orbit category between the chosen representatives.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.deckOrbitRepresentativeFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] : CategoryTheory.Functor (DeckOrbitSkeleton C G) (ShiftOrbitCategory C (Additive G))

Inclusion of the chosen orbit representatives into the nonskeletal shift-orbit category.

instance MagnitudeConjecture.CoveringHom.deckOrbitRepresentativeFunctor_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] : deckOrbitRepresentativeFunctor.Additive

instance MagnitudeConjecture.CoveringHom.deckOrbitRepresentativeFunctor_linear {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : CategoryTheory.Functor.Linear k deckOrbitRepresentativeFunctor

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.orbitSkeletonPushdown {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor (DeckOrbitSkeleton C G) (ModuleCat k)

Gabriel push-down restricted to one chosen representative of each strict deck orbit.

instance MagnitudeConjecture.CoveringHom.orbitSkeletonPushdown_additive {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : (orbitSkeletonPushdown M).Additive

instance MagnitudeConjecture.CoveringHom.orbitSkeletonPushdown_linear {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor.Linear k (orbitSkeletonPushdown M)

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : CategoryTheory.Functor (LinearModuleCategory k) (LinearModuleCategory k)

Skeletal Gabriel push-down as a functor on linear modules.

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_additive {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : linearModuleOrbitSkeletonPushdown.Additive

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_linear {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : CategoryTheory.Functor.Linear k linearModuleOrbitSkeletonPushdown

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.objectIsoDeckOrbitRepresentative {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] (X : C) : (have this := X; this) ≅ have this := deckOrbitRepresentative (Quotient.mk'' X); this

Every upstairs object is isomorphic in the orbit category to the chosen representative of its strict deck orbit.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonMap {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] {X Y : C} (f : X ⟶ Y) : (have this := Quotient.mk'' X; this) ⟶ have this := Quotient.mk'' Y; this

The morphism between chosen orbit representatives induced by an upstairs morphism.

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

The strict-orbit object map and representative-conjugated morphism map form the canonical functor from the upstairs category to the chosen orbit skeleton.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFunctor_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] (X : C) : D.orbitSkeletonFunctor.obj X = Quotient.mk'' X

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFunctor_map {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] {X Y : C} (f : X ⟶ Y) : D.orbitSkeletonFunctor.map f = D.orbitSkeletonMap f

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonMap_add {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] {X Y : C} (f g : X ⟶ Y) : D.orbitSkeletonMap (f + g) = D.orbitSkeletonMap f + D.orbitSkeletonMap g

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFunctor_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] : D.orbitSkeletonFunctor.Additive

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeFunctor_map_orbitSkeletonMap {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] {X Y : C} (f : X ⟶ Y) : deckOrbitRepresentativeFunctor.map (D.orbitSkeletonMap f) = CategoryTheory.CategoryStruct.comp (D.objectIsoDeckOrbitRepresentative X).inv (CategoryTheory.CategoryStruct.comp (ShiftOrbitCategory.identityComponentFunctor.map f) (D.objectIsoDeckOrbitRepresentative Y).hom)

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeFunctor_essSurj {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] : deckOrbitRepresentativeFunctor.EssSurj

The representative inclusion is essentially surjective, hence it really is an orbit skeleton rather than merely a full subcategory.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSkeletonEquivalence {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] : DeckOrbitSkeleton C G ≌ ShiftOrbitCategory C (Additive G)

The one-representative-per-orbit category is equivalent to the full nonskeletal shift-orbit category.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSkeletonEquivalence_functor_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] : D.deckOrbitSkeletonEquivalence.functor.Additive

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitSkeletonEquivalence_functor_linear {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] {k : Type uK} [CommRing k] [CategoryTheory.Linear k C] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] : CategoryTheory.Functor.Linear k D.deckOrbitSkeletonEquivalence.functor