Finite control of object-deletion source and sink terms

The manuscript places the middle terms created by intrinsic source and sink maps at an object-deletion stage in the second ambient Hom neighborhood. The key point is minimality: every indecomposable summand of a minimal right almost-split source has a nonzero component to the endpoint, and dually every summand of a minimal left almost-split target receives a nonzero component from the endpoint. Extension by zero preserves those nonzero maps.

theorem MagnitudeConjecture.CoveringHom.rightMinimal_middleSummand_mem_nextHomNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (S : FiniteIndecomposableModuleFamily) {n : ℕ} {X Y : ControlFiniteModule k C} (d : CategoryTheory.FiniteIndecomposableDecomposition X) (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightMinimal f) (hY : Y ∈ (S.iterateHomNeighborhood hlocal n).isoClosure) (t : Fin d.n) : d.summand t ∈ (S.iterateHomNeighborhood hlocal (n + 1)).isoClosure

Every displayed middle summand of a right-minimal map ending in the nth Hom neighborhood belongs to the next neighborhood.

theorem MagnitudeConjecture.CoveringHom.leftMinimal_middleSummand_mem_nextHomNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (S : FiniteIndecomposableModuleFamily) {n : ℕ} {X Y : ControlFiniteModule k C} (d : CategoryTheory.FiniteIndecomposableDecomposition Y) (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftMinimal f) (hX : X ∈ (S.iterateHomNeighborhood hlocal n).isoClosure) (t : Fin d.n) : d.summand t ∈ (S.iterateHomNeighborhood hlocal (n + 1)).isoClosure

Every displayed middle summand of a left-minimal map starting in the nth Hom neighborhood belongs to the next neighborhood.

theorem MagnitudeConjecture.CoveringHom.rightMinimal_middleSummand_mem_firstFiberHomNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (y : C) {X Y : ControlFiniteModule k C} (d : CategoryTheory.FiniteIndecomposableDecomposition X) (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightMinimal f) (hY : Y ∈ (finiteFiberControlSeed hlocal y).isoClosure) (t : Fin d.n) : d.summand t ∈ ((finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 1).isoClosure

The manuscript's U₁ sink clause: middle summands of a right-minimal sink map ending at a seed module lie in the first Hom neighborhood.

theorem MagnitudeConjecture.CoveringHom.leftMinimal_middleSummand_mem_firstFiberHomNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (y : C) {X Y : ControlFiniteModule k C} (d : CategoryTheory.FiniteIndecomposableDecomposition Y) (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftMinimal f) (hX : X ∈ (finiteFiberControlSeed hlocal y).isoClosure) (t : Fin d.n) : d.summand t ∈ ((finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 1).isoClosure

The manuscript's U₁ source clause: middle summands of a left-minimal source map starting at a seed module lie in the first Hom neighborhood.

theorem MagnitudeConjecture.ObjectDeletion.rightMinimal_source_vanishesAt_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] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) {Y Z : CoveringHom.FiniteDimensionalModuleCategory k} (dY : CategoryTheory.FiniteIndecomposableDecomposition Y) (g : Y ⟶ Z) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) (hZ : CategoryTheory.Indecomposable Z) (houtside : Z ∉ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 2).isoClosure) : ModuleVanishesOnDeleted C {y} Y.obj.obj

If an indecomposable endpoint lies outside the two-step Hom neighborhood of y, the source of any right-minimal map to that endpoint vanishes at y.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletion_sink_localData_unchanged_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) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C {y}).obj Z) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) (hZ : CategoryTheory.Indecomposable ((finiteDimensionalModuleExtensionByZero C {y}).obj Z)) (houtside : (finiteDimensionalModuleExtensionByZero C {y}).obj Z ∉ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 2).isoClosure) (dY : CategoryTheory.FiniteIndecomposableDecomposition Y) (dR : CategoryTheory.FiniteIndecomposableDecomposition (finiteVanishingModuleRestriction C {y} ((finiteMaximalVanishingSubmoduleFunctor C {y}).obj Y))) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (finiteDeletionRightAdjointSinkCandidate C {y} g) ∧ QuotientSubmoduleEquidistribution.IsRightMinimal (finiteDeletionRightAdjointSinkCandidate C {y} g) ∧ dR.n = dY.n ∧ (CategoryTheory.Projective Z ↔ CategoryTheory.Projective ((finiteDimensionalModuleExtensionByZero C {y}).obj Z))

Outside the two-step control neighborhood of a deleted object, the intrinsic deletion sink retains right almost-splitness, right minimality, source arity, and the projectivity flag of its ambient endpoint.

theorem MagnitudeConjecture.ObjectDeletion.exists_finiteDeletion_rightMinimal_sink_controlled {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) {Y : CoveringHom.FiniteDimensionalModuleCategory k} {Z : CoveringHom.FiniteDimensionalModuleCategory k} (g : Y ⟶ (finiteDimensionalModuleExtensionByZero C S).obj Z) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hY : Y ∈ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 1).isoClosure) : ∃ (Y' : CoveringHom.FiniteDimensionalModuleCategory k) (g' : Y' ⟶ Z) (i : Y' ⟶ finiteVanishingModuleRestriction C S ((finiteMaximalVanishingSubmoduleFunctor C S).obj Y)) (d : CategoryTheory.FiniteIndecomposableDecomposition Y'), QuotientSubmoduleEquidistribution.IsRightAlmostSplit g' ∧ QuotientSubmoduleEquidistribution.IsRightMinimal g' ∧ CategoryTheory.IsSplitMono i ∧ CategoryTheory.CategoryStruct.comp i (finiteDeletionRightAdjointSinkCandidate C S g) = g' ∧ ∀ (t : Fin d.n), (finiteDimensionalModuleExtensionByZero C S).obj (d.summand t) ∈ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 2).isoClosure

If the ambient middle term to which the right adjoint is applied lies in the first Hom neighborhood, then every indecomposable middle summand of the resulting right-minimal deletion-stage sink lies in the second ambient Hom neighborhood.

theorem MagnitudeConjecture.ObjectDeletion.exists_finiteDeletion_leftMinimal_source_controlled {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) {Z : CoveringHom.FiniteDimensionalModuleCategory k} {Y : CoveringHom.FiniteDimensionalModuleCategory k} (f : (finiteDimensionalModuleExtensionByZero C S).obj Z ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (hY : Y ∈ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 1).isoClosure) : ∃ (Y' : CoveringHom.FiniteDimensionalModuleCategory k) (f' : Z ⟶ Y') (i : Y' ⟶ finiteVanishingModuleRestriction C S ((finiteMaximalVanishingQuotientFunctor C S).obj Y)) (d : CategoryTheory.FiniteIndecomposableDecomposition Y'), QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f' ∧ QuotientSubmoduleEquidistribution.IsLeftMinimal f' ∧ CategoryTheory.IsSplitMono i ∧ CategoryTheory.CategoryStruct.comp f' i = finiteDeletionLeftAdjointSourceCandidate C S f ∧ ∀ (t : Fin d.n), (finiteDimensionalModuleExtensionByZero C S).obj (d.summand t) ∈ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 2).isoClosure

Dually, if the ambient middle term to which the left adjoint is applied lies in the first Hom neighborhood, every indecomposable middle summand of the resulting left-minimal deletion-stage source lies in the second ambient Hom neighborhood.

theorem MagnitudeConjecture.ObjectDeletion.finiteDeletion_bifactor_extension_mem_threeStepControlFamily {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) {X Y Z : CoveringHom.FiniteDimensionalModuleCategory k} (hX : (finiteDimensionalModuleExtensionByZero C S).obj X ∈ ((CoveringHom.finiteFiberControlSeed hlocal y).iterateHomNeighborhood hlocal 2).isoClosure) (hZ : CategoryTheory.Indecomposable Z) (a : X ⟶ Z) (ha : a ≠ 0) (b : Z ⟶ Y) (hb : b ≠ 0) : (finiteDimensionalModuleExtensionByZero C S).obj Z ∈ (CoveringHom.finiteThreeStepControlFamily hlocal y).isoClosure

A nonzero factorization through an indecomposable deletion-stage module is still a nonzero factorization after extension by zero. If its source term lies in the ambient U₂ window, the witness therefore lies in the ambient U₃ window, independently of which earlier objects were deleted.