Residual separation of a finite module family

A nonzero shifted map between finite-support modules forces the source support to meet a translate of the target support. Only finitely many deck degrees can do this for a finite family. Residual finiteness therefore supplies a finite-index normal subgroup on which every nonidentity shifted Hom between the chosen modules vanishes.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.exists_support_overlap_of_shiftHom_ne_zero {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive 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)] (M N : FiniteDimensionalModuleCategory k) (g : G) (t : ShiftHom M.obj N.obj (Additive.ofMul g)) (ht : t ≠ 0) : ∃ X ∈ moduleSupport k M.obj.obj, g • X ∈ moduleSupport k N.obj.obj

A nonzero shifted map between finite modules is detected at an object in the source support whose translate belongs to the target support.

def MagnitudeConjecture.CoveringHom.moduleSupportTransportDegrees {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (N : FiniteDimensionalModuleCategory k) : Set G

Deck degrees carrying some object of the source support into the target support.

theorem MagnitudeConjecture.CoveringHom.moduleSupportTransportDegrees_finite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [IsCancelSMul G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (N : FiniteDimensionalModuleCategory k) : (moduleSupportTransportDegrees M N).Finite

Only finitely many deck degrees can carry one finite module support into another when the action on objects is free.

def MagnitudeConjecture.CoveringHom.finiteModuleFamilySupportBadDegrees {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : Set G

The nonidentity ambient degrees that can overlap the supports of two chosen modules.

theorem MagnitudeConjecture.CoveringHom.finiteModuleFamilySupportBadDegrees_finite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [IsCancelSMul G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : (finiteModuleFamilySupportBadDegrees S).Finite

theorem MagnitudeConjecture.CoveringHom.exists_finiteIndexNormalSubgroup_avoiding_supportBadDegrees {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [IsCancelSMul G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Group.ResiduallyFinite G] (S : FiniteIndecomposableModuleFamily) : ∃ (N : FiniteIndexNormalSubgroup G), ∀ g ∈ finiteModuleFamilySupportBadDegrees S, g ∉ N

Residual finiteness supplies one finite-index normal subgroup avoiding every nonidentity support-overlap degree of the finite module family.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.restrict_finiteModuleWindowShiftHomOrthogonal_of_avoids {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive 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)] (S : FiniteIndecomposableModuleFamily) (N : Subgroup G) (havoid : ∀ g ∈ finiteModuleFamilySupportBadDegrees S, g ∉ N) : (D.restrict N).FiniteModuleWindowShiftHomOrthogonal (Set.range S.obj)

Avoiding every nonidentity support-overlap degree makes the restricted deck shift orthogonal on the literal chosen family.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.exists_finiteIndexNormalSubgroup_restrict_shiftHomOrthogonal {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [IsCancelSMul G C] [CategoryTheory.Preadditive 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)] [Group.ResiduallyFinite G] (S : FiniteIndecomposableModuleFamily) : ∃ (N : FiniteIndexNormalSubgroup G), (D.restrict N.toSubgroup).FiniteModuleWindowShiftHomOrthogonal (Set.range S.obj)

Residual finiteness produces a finite-index normal subgroup whose restricted coherent deck shift is shift-Hom orthogonal on the chosen finite module family.