Local density under one object deletion

For an indecomposable ambient module, the manuscript extends the local density after deleting an object by zero when the module does not survive. This file makes that convention literal. The minimal-sink comparison proves that the resulting local change vanishes outside the two-step Hom core.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDeletionExtendedLocalDensity {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) : ℤ

The local density after deletion, extended by zero to an ambient indecomposable which does not vanish on the deleted objects.

noncomputable def MagnitudeConjecture.ObjectDeletion.finiteDeletionLocalChangeAt {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) : ℤ

The manuscript's pointwise local-density change across an arbitrary object deletion.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionExtendedLocalDensity_eq_zero_of_not_vanishes {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (hvanish : ¬ModuleVanishesOnDeleted C S M.obj.obj) : finiteDeletionExtendedLocalDensity C hlocal S M hM = 0

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionExtendedLocalDensity_eq_of_iso {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (S : Set C) {M N : CoveringHom.FiniteDimensionalModuleCategory k} (hM : CategoryTheory.Indecomposable M) (hN : CategoryTheory.Indecomposable N) (e : M ≅ N) : finiteDeletionExtendedLocalDensity C hlocal S M hM = finiteDeletionExtendedLocalDensity C hlocal S N hN

The deletion-extended local density depends only on the ambient indecomposable isomorphism class.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionLocalChangeAt_eq_of_iso {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (S : Set C) {M N : CoveringHom.FiniteDimensionalModuleCategory k} (hM : CategoryTheory.Indecomposable M) (hN : CategoryTheory.Indecomposable N) (e : M ≅ N) : finiteDeletionLocalChangeAt C hlocal S M hM = finiteDeletionLocalChangeAt C hlocal S N hN

The pointwise local change depends only on the ambient indecomposable isomorphism class.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletion_restriction_localDensity_eq_of_minimalSink_source_vanishes {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (hvanish : ModuleVanishesOnDeleted C S M.obj.obj) {Y : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ M) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) (dY : CategoryTheory.FiniteIndecomposableDecomposition Y) (hY : ModuleVanishesOnDeleted C S Y.obj.obj) : CoveringHom.finiteModuleLocalDensity ⋯ (finiteDimensionalModuleRestrictionToDeletion C S M hvanish) ⋯ = CoveringHom.finiteModuleLocalDensity hlocal M hM

If a surviving indecomposable has a minimal sink whose source already vanishes on the deleted objects, restriction preserves its intrinsic local density.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionLocalChangeAt_eq_zero_of_minimalSink_source_vanishes {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (S : Set C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (hvanish : ModuleVanishesOnDeleted C S M.obj.obj) {Y : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ M) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) (dY : CategoryTheory.FiniteIndecomposableDecomposition Y) (hY : ModuleVanishesOnDeleted C S Y.obj.obj) : finiteDeletionLocalChangeAt C hlocal S M hM = 0

If both a surviving indecomposable endpoint and the source of one of its minimal right almost-split maps vanish on the deleted objects, its pointwise deletion local change is zero.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletion_localDensity_eq_of_endpoint_not_mem_twoStep {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) (Z : CoveringHom.FiniteDimensionalModuleCategory k) (hZ : CategoryTheory.Indecomposable Z) (houtside : (finiteDimensionalModuleExtensionByZero C {y}).obj Z ∉ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 2).isoClosure) : CoveringHom.finiteModuleLocalDensity ⋯ Z hZ = CoveringHom.finiteModuleLocalDensity hlocal ((finiteDimensionalModuleExtensionByZero C {y}).obj Z) ⋯

Outside the two-step core, a surviving indecomposable has the same intrinsic local density before and after one object deletion.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletion_localDensity_eq_of_not_mem_deletionTwoStepModuleCore {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) (S : Set C) (hy : y ∉ S) (hPstage : ∀ (X : DeletionCategory C S), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) (Z : CoveringHom.FiniteDimensionalModuleCategory k) (hZ : CategoryTheory.Indecomposable Z) (houtside : (finiteDimensionalModuleExtensionByZero (DeletionCategory C S) {survivingObj C S hy}).obj Z ∉ deletionTwoStepModuleCore C hlocal y S) : CoveringHom.finiteModuleLocalDensity ⋯ Z hZ = CoveringHom.finiteModuleLocalDensity ⋯ ((finiteDimensionalModuleExtensionByZero (DeletionCategory C S) {survivingObj C S hy}).obj Z) ⋯

At an intermediate deletion stage, a surviving endpoint outside the fixed ambient two-step core has the same intrinsic density after deleting the chosen surviving object.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionLocalChangeAt_eq_zero_of_not_mem_deletionTwoStepModuleCore {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) (S : Set C) (hy : y ∉ S) (hPstage : ∀ (X : DeletionCategory C S), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (houtside : M ∉ deletionTwoStepModuleCore C hlocal y S) : finiteDeletionLocalChangeAt (DeletionCategory C S) ⋯ {survivingObj C S hy} M hM = 0

At an intermediate stage, the singleton local change at the next surviving object is supported on the fixed ambient two-step core.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletionLocalChangeAt_eq_zero_of_not_mem_twoStep {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) (M : CoveringHom.FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (houtside : M ∉ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 2).isoClosure) : finiteDeletionLocalChangeAt C hlocal {y} M hM = 0

The singleton-deletion local change is supported on the manuscript's two-step Hom neighborhood.