Deck shifts on invariant object-deletion quotients

An intermediate covering stage deletes a union of orbits for the subgroup Γ. This file supplies exactly the symmetry retained by such a stage. An action-invariant, isomorphism-closed deleted set is invariant under the coherent deck shifts, so the shifts descend through C/(S). The literal deck action on surviving objects and the descended shifts again form a CoherentDeckShift.

def MagnitudeConjecture.ObjectDeletion.ActionInvariant {C : Type u} {G : Type w} [Group G] [MulAction G C] (S : Set C) : Prop

Membership in a set of objects is unchanged by the literal left group action.

theorem MagnitudeConjecture.ObjectDeletion.isClosedUnderIsomorphisms_of_skeletal {C : Type u} [CategoryTheory.Category.{v, u} C] (hC : CategoryTheory.Skeletal C) (S : Set C) : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S

In a skeletal category every object property is closed under isomorphisms.

theorem MagnitudeConjecture.ObjectDeletion.CoherentDeckShift.shiftInvariant_of_actionInvariant {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoveringHom.CoherentDeckShift C G) (S : Set C) [CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S] (hS : ActionInvariant S) : ShiftInvariant C (Additive G) S

Literal deck invariance, together with closure under isomorphism, implies invariance under the chosen coherent deck functors.

@[implicit_reducible]

def MagnitudeConjecture.ObjectDeletion.deletionMulAction {k : Type z} [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] (S : Set C) (hS : ActionInvariant S) : MulAction G (DeletionCategory C S)

The literal deck action on the surviving objects of C/(S).

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.deletion_smul_obj_as {k : Type z} [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] (S : Set C) (hS : ActionInvariant S) (g : G) (X : DeletionCategory C S) : (g • X).obj.as = g • X.obj.as

theorem MagnitudeConjecture.ObjectDeletion.deletionIsCancelSMul {k : Type z} [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] [IsCancelSMul G C] (S : Set C) (hS : ActionInvariant S) : IsCancelSMul G (DeletionCategory C S)

Freeness of the literal object action survives deletion.

noncomputable def MagnitudeConjecture.ObjectDeletion.CoherentDeckShift.deletionCoherentDeckShift {k : Type z} [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] (D : CoveringHom.CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : Set C) [CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S] (hS : ActionInvariant S) : have hShift := ⋯; CoveringHom.CoherentDeckShift (DeletionCategory C S) G

A coherent deck shift descends to an invariant object-deletion quotient. The resulting object comparison is the composite of the full-subcategory shift comparison with the quotient of the original deck comparison.

theorem MagnitudeConjecture.ObjectDeletion.CoherentDeckShift.deletionCoherentDeckShift_hasShift_eq {k : Type z} [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] (D : CoveringHom.CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : Set C) [CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S] (hS : ActionInvariant S) : have hShift := ⋯; CoveringHom.CoherentDeckShift.hasShift (deletionCoherentDeckShift D S hS) = deletionHasShift S hShift

The shift instance exported by the coherent deletion package is the inherited deletion shift from which its core was built.

theorem MagnitudeConjecture.ObjectDeletion.CoherentDeckShift.deletionCoherentDeckShift_core_F_eq_shiftFunctor {k : Type z} [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] (D : CoveringHom.CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : Set C) [CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S] (hS : ActionInvariant S) (a : Additive G) : have hShift := ⋯; (deletionCoherentDeckShift D S hS).core.F a = CategoryTheory.shiftFunctor (DeletionCategory C S) a

The functor field of the coherent deletion shift is the inherited deletion shift functor. This equation exposes the otherwise private constructor used by deletionCoherentDeckShift.

theorem MagnitudeConjecture.ObjectDeletion.CoherentDeckShift.deletionCoherentDeckShift_restrict_core_eq {k : Type z} [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] (D : CoveringHom.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) (S : Set C) [CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S] (hSG : ActionInvariant S) (hSN : ActionInvariant S) : have DG := deletionCoherentDeckShift D S hSG; have DN := deletionCoherentDeckShift (D.restrict N) S hSN; (DG.restrict N).core = DN.core

Descending an invariant deck shift through object deletion commutes with restriction to a subgroup at the level of the complete coherent shift core.

instance MagnitudeConjecture.ObjectDeletion.CoherentDeckShift.deletionCoherentDeckShift_core_additive {k : Type z} [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] (D : CoveringHom.CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : Set C) [CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S] (hS : ActionInvariant S) (a : Additive G) : have hShift := ⋯; ((deletionCoherentDeckShift D S hS).core.F a).Additive

instance MagnitudeConjecture.ObjectDeletion.CoherentDeckShift.deletionCoherentDeckShift_core_linear {k : Type z} [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] (D : CoveringHom.CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : Set C) [CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms S] (hS : ActionInvariant S) (a : Additive G) : have hShift := ⋯; CategoryTheory.Functor.Linear k ((deletionCoherentDeckShift D S hS).core.F a)