Finitely many surviving object-deletion windows

The manuscript fixes the finite ambient family U₃(x) and observes that an intermediate deletion stage can only discard some of those representatives. Hence only finitely many surviving full subcategories occur. This file formalizes that finite signature and the ensuing choice-and-union argument for upward-closed finite control data.

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionSurvivingIndices {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (D : Set C) : Finset (Fin W.n)

The indices of a finite ambient family whose representatives survive a given deletion, equivalently whose modules vanish on every deleted object.

@[simp]

theorem MagnitudeConjecture.ObjectDeletion.mem_deletionSurvivingIndices_iff {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (D : Set C) (i : Fin W.n) : i ∈ deletionSurvivingIndices C W D ↔ ModuleVanishesOnDeleted C D (W.obj i).obj.obj

noncomputable def MagnitudeConjecture.ObjectDeletion.deletionSurvivingSubfamily {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (D : Set C) : CoveringHom.FiniteIndecomposableModuleFamily

The finite subfamily of ambient representatives surviving a deletion.

theorem MagnitudeConjecture.ObjectDeletion.deletionSurvivingSubfamily_obj_vanishes {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (D : Set C) (t : Fin (deletionSurvivingSubfamily C W D).n) : ModuleVanishesOnDeleted C D ((deletionSurvivingSubfamily C W D).obj t).obj.obj

Every object of the surviving subfamily really vanishes on the deleted set.

theorem MagnitudeConjecture.ObjectDeletion.mem_deletionSurvivingSubfamily_isoClosure {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (D : Set C) {M : CoveringHom.FiniteDimensionalModuleCategory k} (hM : M ∈ W.isoClosure) (hvanish : ModuleVanishesOnDeleted C D M.obj.obj) : M ∈ (deletionSurvivingSubfamily C W D).isoClosure

Any module represented by the ambient family and surviving the deletion is represented by the corresponding finite surviving subfamily.

theorem MagnitudeConjecture.ObjectDeletion.mem_deletionSurvivingSubfamily_isoClosure_iff {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (D : Set C) {M : CoveringHom.FiniteDimensionalModuleCategory k} : M ∈ (deletionSurvivingSubfamily C W D).isoClosure ↔ M ∈ W.isoClosure ∧ ModuleVanishesOnDeleted C D M.obj.obj

The surviving finite subfamily represents exactly the members of the ambient family that vanish on the deleted objects. Thus its isomorphism closure is the manuscript's full surviving subcategory inside the fixed finite window.

def MagnitudeConjecture.ObjectDeletion.RealizedSurvivorSignature {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (Allowed : Set C → Prop) : Type

A realized survivor signature is one of the finite subsets of the fixed ambient family actually produced by an allowed deleted set.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.ObjectDeletion.realizedSurvivorSignatureFintype {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (Allowed : Set C → Prop) : Fintype (RealizedSurvivorSignature C W Allowed)

noncomputable def MagnitudeConjecture.ObjectDeletion.realizedSurvivorSignatureOf {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (Allowed : Set C → Prop) (D : Set C) (hD : Allowed D) : RealizedSurvivorSignature C W Allowed

The signature associated to one allowed deletion stage.

def MagnitudeConjecture.ObjectDeletion.RealizedSurvivorSignature.representativeDeletedSet {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {W : CoveringHom.FiniteIndecomposableModuleFamily} {Allowed : Set C → Prop} (q : RealizedSurvivorSignature C W Allowed) : Set C

Choose one deleted set realizing a given survivor signature.

theorem MagnitudeConjecture.ObjectDeletion.RealizedSurvivorSignature.representative_allowed {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {W : CoveringHom.FiniteIndecomposableModuleFamily} {Allowed : Set C → Prop} (q : RealizedSurvivorSignature C W Allowed) : Allowed (representativeDeletedSet C q)

theorem MagnitudeConjecture.ObjectDeletion.RealizedSurvivorSignature.representative_indices {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {W : CoveringHom.FiniteIndecomposableModuleFamily} {Allowed : Set C → Prop} (q : RealizedSurvivorSignature C W Allowed) : deletionSurvivingIndices C W (representativeDeletedSet C q) = ↑q

theorem MagnitudeConjecture.ObjectDeletion.exists_uniformControlFamily_of_survivorSignatures {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (W : CoveringHom.FiniteIndecomposableModuleFamily) (Allowed : Set C → Prop) (Control : Set C → CoveringHom.FiniteIndecomposableModuleFamily → Prop) (exists_control : ∀ (D : Set C), Allowed D → ∃ (V : CoveringHom.FiniteIndecomposableModuleFamily), Control D V) (control_invariant : ∀ {D E : Set C}, Allowed D → Allowed E → deletionSurvivingIndices C W D = deletionSurvivingIndices C W E → ∀ {V : CoveringHom.FiniteIndecomposableModuleFamily}, Control D V ↔ Control E V) (control_upward : ∀ (D : Set C), Allowed D → ∀ {V U : CoveringHom.FiniteIndecomposableModuleFamily}, Control D V → V.isoClosure ⊆ U.isoClosure → Control D U) : ∃ (U : CoveringHom.FiniteIndecomposableModuleFamily), ∀ (D : Set C), Allowed D → Control D U

Finite survivor signatures and upward closure turn stagewise existence of finite control families into one finite family controlling every allowed deletion stage. The invariance premise is the exact statement that control depends only on the surviving full subcategory of the fixed ambient family.

theorem MagnitudeConjecture.ObjectDeletion.exists_uniformControlFamily_for_threeStepDeletionStages {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) (Allowed : Set C → Prop) (Control : Set C → CoveringHom.FiniteIndecomposableModuleFamily → Prop) (exists_control : ∀ (D : Set C), Allowed D → ∃ (V : CoveringHom.FiniteIndecomposableModuleFamily), Control D V) (control_invariant : ∀ {D E : Set C}, Allowed D → Allowed E → deletionSurvivingIndices C (CoveringHom.finiteThreeStepControlFamily hlocal y) D = deletionSurvivingIndices C (CoveringHom.finiteThreeStepControlFamily hlocal y) E → ∀ {V : CoveringHom.FiniteIndecomposableModuleFamily}, Control D V ↔ Control E V) (control_upward : ∀ (D : Set C), Allowed D → ∀ {V U : CoveringHom.FiniteIndecomposableModuleFamily}, Control D V → V.isoClosure ⊆ U.isoClosure → Control D U) : ∃ (U : CoveringHom.FiniteIndecomposableModuleFamily), ∀ (D : Set C), Allowed D → Control D U

The uniform-choice argument specialized to the manuscript's fixed three-step Hom window U₃(y).