Shifts on object-deletion quotients

If a coherent shift preserves the set of deleted objects, every shift functor preserves the deletion ideal. It therefore descends to the raw Hom-ideal quotient. The induced shift on that quotient preserves the full subcategory of surviving objects and hence restricts to the manuscript's category C/(S).

The construction is stated for an arbitrary additive group of shifts. The covering application takes the shifts indexed by Additive Γ, where the set already deleted at an intermediate stage is a union of Γ-orbits.

def MagnitudeConjecture.ObjectDeletion.ShiftInvariant (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type w) [AddGroup A] [CategoryTheory.HasShift C A] (S : Set C) : Prop

A deleted object set is shift-invariant when membership is unchanged by every shift functor. For a group of shifts, either implication would suffice; the biconditional is the useful interface for both deleted and surviving objects.

@[reducible, inline]

abbrev MagnitudeConjecture.ObjectDeletion.shiftedRawFunctor {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (S : Set C) (a : A) : CategoryTheory.Functor C (RawCategory C S)

Shift first and then apply the raw deletion quotient.

theorem MagnitudeConjecture.ObjectDeletion.shiftedRawFunctor_isKilledBy {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) (a : A) : (ideal C S).IsKilledBy (shiftedRawFunctor S a)

Shift-invariance of the deleted objects makes every shifted raw quotient functor kill the deletion ideal.

noncomputable def MagnitudeConjecture.ObjectDeletion.rawShiftFunctor {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) (a : A) : CategoryTheory.Functor (RawCategory C S) (RawCategory C S)

The shift functor descended to the raw Hom-ideal quotient.

instance MagnitudeConjecture.ObjectDeletion.rawShiftFunctor_additive {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) (a : A) : (rawShiftFunctor S hS a).Additive

instance MagnitudeConjecture.ObjectDeletion.rawShiftFunctor_linear {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) (a : A) : CategoryTheory.Functor.Linear k (rawShiftFunctor S hS a)

noncomputable def MagnitudeConjecture.ObjectDeletion.rawFunctorShiftIso {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) (a : A) : (rawFunctor C S).comp (rawShiftFunctor S hS a) ≅ (CategoryTheory.shiftFunctor C a).comp (rawFunctor C S)

The raw quotient functor intertwines the ambient and descended shifts. This is definitionally the quotient-lift triangle.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.ObjectDeletion.rawHasShift {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) : CategoryTheory.HasShift (RawCategory C S) A

The coherent shift induced on the raw Hom-ideal quotient.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.ObjectDeletion.rawFunctorCommShift {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) : (rawFunctor C S).CommShift A

The raw quotient functor commutes coherently with the induced shifts.

theorem MagnitudeConjecture.ObjectDeletion.isSurvivingRaw_stableUnderShift {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) : (IsSurvivingRaw C S).IsStableUnderShift A

Surviving raw quotient objects are stable under the induced shift.

@[implicit_reducible]

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionHasShift {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) : CategoryTheory.HasShift (DeletionCategory C S) A

The coherent shift on the manuscript's deletion category C/(S).

@[implicit_reducible]

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionInclusionCommShift {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) : (IsSurvivingRaw C S).ι.CommShift A

The inclusion of surviving quotient objects into the raw quotient commutes with the induced shifts.

theorem MagnitudeConjecture.ObjectDeletion.deletionShift_additive {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) (a : A) : (CategoryTheory.shiftFunctor (DeletionCategory C S) a).Additive

Every shift functor on the deletion category remains additive.

theorem MagnitudeConjecture.ObjectDeletion.deletionShift_linear {k : Type z} [Ring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : Set C) (hS : ShiftInvariant C A S) (a : A) : CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor (DeletionCategory C S) a)

Every shift functor on the deletion category remains linear.