Finite module control windows up to isomorphism

Local representation-finiteness makes the symmetric Hom neighborhood of an indecomposable finite module finite up to isomorphism. Iterating this construction gives the manuscript's finite three-step control window. The actual set-valued window is the isomorphism closure of a finite family; this distinguishes correctly between finiteness of indecomposable isomorphism classes and literal finiteness of the ambient type of module objects.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.ControlFiniteModule (k : Type v) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (max (max u v) (v + 1))

theorem MagnitudeConjecture.CoveringHom.mem_moduleSupport_iff_of_iso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : ControlFiniteModule k C} (e : M ≅ N) (X : C) : X ∈ moduleSupport k M.obj.obj ↔ X ∈ moduleSupport k N.obj.obj

Isomorphic finite-dimensional modules have the same literal object support.

theorem MagnitudeConjecture.CoveringHom.exists_common_moduleSupport_of_ne_zero {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : ControlFiniteModule k C} (f : M ⟶ N) (hf : f ≠ 0) : ∃ X ∈ moduleSupport k M.obj.obj, X ∈ moduleSupport k N.obj.obj

A nonzero morphism of finite modules has a base object at which both its source and target are nonzero.

structure MagnitudeConjecture.CoveringHom.FiniteIndecomposableHomNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : ControlFiniteModule k C) : Type (max u (v + 1))

A finite list representing every indecomposable module in the symmetric Hom neighborhood of M.

• n : ℕ
• obj : Fin self.n → ControlFiniteModule k C
• indecomposable (i : Fin self.n) : CategoryTheory.Indecomposable (self.obj i)
• covers {Y : ControlFiniteModule k C} : CategoryTheory.Indecomposable Y → CoveringSeparation.homInteraction M Y → ∃ (i : Fin self.n), Nonempty (self.obj i ≅ Y)

def MagnitudeConjecture.CoveringHom.indecomposableHomInteraction {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M Y : ControlFiniteModule k C) : Prop

The interaction relation on the indecomposable vertices of the module category. The indecomposability guard is essential: the manuscript's finite windows are windows in ind(mod C), not literally finite subsets of all module objects.

noncomputable def MagnitudeConjecture.CoveringHom.finiteIndecomposableHomNeighborhood_of_locallyRepresentationFinite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (M : ControlFiniteModule k C) (hM : CategoryTheory.Indecomposable M) : FiniteIndecomposableHomNeighborhood M

Local representation-finiteness supplies a finite symmetric Hom neighborhood for every indecomposable finite module.

theorem MagnitudeConjecture.CoveringHom.finiteIndecomposableHomNeighborhood_obj_commonSupport {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (M : ControlFiniteModule k C) (hM : CategoryTheory.Indecomposable M) (t : Fin (finiteIndecomposableHomNeighborhood_of_locallyRepresentationFinite hlocal M hM).n) : ∃ X ∈ moduleSupport k M.obj.obj, X ∈ moduleSupport k ((finiteIndecomposableHomNeighborhood_of_locallyRepresentationFinite hlocal M hM).obj t).obj.obj

Every representative chosen in a finite Hom neighborhood genuinely shares an object-support point with the center module.

theorem MagnitudeConjecture.CoveringHom.finiteIndecomposableHomNeighborhood_covers_commonSupport {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (M : ControlFiniteModule k C) (hM : CategoryTheory.Indecomposable M) {Y : ControlFiniteModule k C} (hY : CategoryTheory.Indecomposable Y) (hcommon : ∃ X ∈ moduleSupport k M.obj.obj, X ∈ moduleSupport k Y.obj.obj) : ∃ (t : Fin (finiteIndecomposableHomNeighborhood_of_locallyRepresentationFinite hlocal M hM).n), Nonempty ((finiteIndecomposableHomNeighborhood_of_locallyRepresentationFinite hlocal M hM).obj t ≅ Y)

Every indecomposable sharing an object-support point with the center is represented in its finite Hom neighborhood.

structure MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (max u (v + 1))

A finite family of chosen indecomposable module representatives.

• n : ℕ
• obj : Fin self.n → ControlFiniteModule k C
• indecomposable (i : Fin self.n) : CategoryTheory.Indecomposable (self.obj i)

def MagnitudeConjecture.CoveringHom.FiniteIndecomposableFiber.toModuleFamily {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X : C} (H : FiniteIndecomposableFiber X) : FiniteIndecomposableModuleFamily

Forget the coverage property of a pointwise local-representation-finite fiber and retain its finite family of indecomposable representatives.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.subfamily {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (I : Finset (Fin S.n)) : FiniteIndecomposableModuleFamily

Restrict a finite representative family to a finite set of its indices.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.flatten {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (W : ι → FiniteIndecomposableModuleFamily) : FiniteIndecomposableModuleFamily

Flatten a finite family of finite representative families.

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

The set-valued control window represented by a finite family: all module objects isomorphic to one of its chosen representatives.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.obj_mem_subfamily_isoClosure {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (I : Finset (Fin S.n)) {i : Fin S.n} (hi : i ∈ I) : S.obj i ∈ (S.subfamily I).isoClosure

A selected parent representative belongs to the isomorphism closure of the corresponding finite subfamily.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.isoClosure_subset_flatten {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type} [Fintype ι] (W : ι → FiniteIndecomposableModuleFamily) (i : ι) : (W i).isoClosure ⊆ (flatten W).isoClosure

Every member of one constituent family belongs to the isomorphism closure of the flattened finite family.

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

The additive hull generated by the finite indecomposable family: objects isomorphic to finite biproducts of its members, with repetitions allowed. This is the categorical window in which arbitrary relevant factorization cores live.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.range_finite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : (Set.range S.obj).Finite

The literal range of chosen representatives is finite.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.obj_mem_isoClosure {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (i : Fin S.n) : S.obj i ∈ S.isoClosure

Every chosen representative belongs to the isomorphism closure.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.isoClosure_subset_additiveClosure {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : S.isoClosure ⊆ S.additiveClosure

The indecomposable isomorphism closure embeds in the additive hull.

instance MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.additiveClosure_isClosedUnderIsomorphisms {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : (have this := S.additiveClosure; this).IsClosedUnderIsomorphisms

The additive hull is closed under isomorphism.

instance MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.additiveClosure_containsZero {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : (have this := S.additiveClosure; this).ContainsZero

The additive hull contains a zero object, represented by the empty biproduct.

instance MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.additiveClosure_isClosedUnderBinaryProducts {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : (have this := S.additiveClosure; this).IsClosedUnderBinaryProducts

The additive hull is closed under binary biproducts.

instance MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.additiveClosure_isClosedUnderFiniteProducts {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : (have this := S.additiveClosure; this).IsClosedUnderFiniteProducts

Binary biproduct and zero closure give all finite products in the full subcategory on the additive hull.

instance MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.additiveClosure_hasFiniteBiproducts {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : CategoryTheory.Limits.HasFiniteBiproducts (CoveringSeparation.WindowCategory S.additiveClosure)

The full subcategory on the additive hull has finite biproducts.

instance MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.additiveClosure_hasBinaryBiproducts {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : CategoryTheory.Limits.HasBinaryBiproducts (CoveringSeparation.WindowCategory S.additiveClosure)

The finite-biproduct structure on the additive hull supplies binary biproducts explicitly for interfaces which request the two structures separately.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.exists_finiteIndecomposableDecomposition_additiveClosure {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (X : CoveringSeparation.WindowCategory S.additiveClosure) : ∃ (d : CategoryTheory.FiniteIndecomposableDecomposition X), ∀ (i : Fin d.n), CategoryTheory.Indecomposable (d.summand i).obj

Every object of the additive hull has a displayed decomposition whose summands remain indecomposable in the ambient finite-module category.

structure MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.HomNeighborhoodExtension {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) : Type (max u (v + 1))

A finite representative family together with the fact that it covers the indecomposable Hom neighbors of every member of the preceding family.

• family : FiniteIndecomposableModuleFamily
• covers (i : Fin S.n) {Y : ControlFiniteModule k C} : CategoryTheory.Indecomposable Y → CoveringSeparation.homInteraction (S.obj i) Y → ∃ (j : Fin self.family.n), Nonempty (self.family.obj j ≅ Y)

noncomputable def MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.homNeighborhoodExtension {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) : S.HomNeighborhoodExtension

One symmetric Hom-neighborhood enlargement of a finite representative family, retaining its coverage certificate.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.homNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) : FiniteIndecomposableModuleFamily

The finite family underlying one certified Hom-neighborhood extension.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.homNeighborhood_obj_commonSupport {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) (t : Fin (S.homNeighborhood hlocal).n) : ∃ (i : Fin S.n), ∃ X ∈ moduleSupport k (S.obj i).obj.obj, X ∈ moduleSupport k ((S.homNeighborhood hlocal).obj t).obj.obj

Every representative in a family Hom-neighborhood shares a support object with some representative in the preceding family.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.mem_homNeighborhood_isoClosure_of_commonSupport {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) {Y : ControlFiniteModule k C} (hY : CategoryTheory.Indecomposable Y) (hcommon : ∃ (i : Fin S.n), ∃ X ∈ moduleSupport k (S.obj i).obj.obj, X ∈ moduleSupport k Y.obj.obj) : Y ∈ (S.homNeighborhood hlocal).isoClosure

Every indecomposable sharing a support object with a representative of a finite family is represented in the family's Hom-neighborhood.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.interactionNeighborhood_isoClosure_subset_homNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) : CoveringSeparation.interactionNeighborhood indecomposableHomInteraction S.isoClosure ⊆ (S.homNeighborhood hlocal).isoClosure

The isomorphism closure of the enlarged family contains the full set-valued Hom-interaction neighborhood of the previous closure.

def MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.iterateHomNeighborhood {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) : ℕ → FiniteIndecomposableModuleFamily

Iterated finite representative families for successive symmetric Hom neighborhoods.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.interactionNeighborhood_iterateHomNeighborhood_subset {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) (n : ℕ) : CoveringSeparation.interactionNeighborhood indecomposableHomInteraction (S.iterateHomNeighborhood hlocal n).isoClosure ⊆ (S.iterateHomNeighborhood hlocal (n + 1)).isoClosure

Each iterated isomorphism-saturated window contains the full Hom neighborhood of the preceding one.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.mem_iterateHomNeighborhood_succ_of_homInteraction {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) {n : ℕ} {X Y : ControlFiniteModule k C} (hX : X ∈ (S.iterateHomNeighborhood hlocal n).isoClosure) (hY : CategoryTheory.Indecomposable Y) (hXY : CoveringSeparation.homInteraction X Y) : Y ∈ (S.iterateHomNeighborhood hlocal (n + 1)).isoClosure

An indecomposable interacting with a member of the nth certified Hom neighborhood belongs to the next neighborhood.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.mem_iterateHomNeighborhood_succ_of_ne_zero_to {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) {n : ℕ} {X Y : ControlFiniteModule k C} (hX : X ∈ (S.iterateHomNeighborhood hlocal n).isoClosure) (hY : CategoryTheory.Indecomposable Y) (f : X ⟶ Y) (hf : f ≠ 0) : Y ∈ (S.iterateHomNeighborhood hlocal (n + 1)).isoClosure

A nonzero map out of a member of the nth neighborhood puts its indecomposable target in the next neighborhood.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.mem_iterateHomNeighborhood_succ_of_ne_zero_from {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) {n : ℕ} {X Y : ControlFiniteModule k C} (hX : X ∈ (S.iterateHomNeighborhood hlocal n).isoClosure) (hY : CategoryTheory.Indecomposable Y) (f : Y ⟶ X) (hf : f ≠ 0) : Y ∈ (S.iterateHomNeighborhood hlocal (n + 1)).isoClosure

A nonzero map into a member of the nth neighborhood puts its indecomposable source in the next neighborhood.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.bifactor_mem_iterateHomNeighborhood_succ {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) {n : ℕ} {X Y Z : ControlFiniteModule k C} (hX : X ∈ (S.iterateHomNeighborhood hlocal n).isoClosure) (hZ : CategoryTheory.Indecomposable Z) (a : X ⟶ Z) (ha : a ≠ 0) (b : Z ⟶ Y) (hb : b ≠ 0) : Z ∈ (S.iterateHomNeighborhood hlocal (n + 1)).isoClosure ∧ CoveringSeparation.homInteraction X Z ∧ CoveringSeparation.homInteraction Y Z

An indecomposable nonzero factorization witness whose source endpoint is in the nth neighborhood belongs to the next neighborhood and interacts with both endpoints.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.threeStepControlFamily {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) : FiniteIndecomposableModuleFamily

The manuscript's three-step finite control family.

theorem MagnitudeConjecture.CoveringHom.FiniteIndecomposableModuleFamily.bifactor_mem_threeStepControlFamily {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteIndecomposableModuleFamily) (hlocal : IsLocallyRepresentationFinite) {X Y Z : ControlFiniteModule k C} (hX : X ∈ (S.iterateHomNeighborhood hlocal 2).isoClosure) (hZ : CategoryTheory.Indecomposable Z) (a : X ⟶ Z) (ha : a ≠ 0) (b : Z ⟶ Y) (hb : b ≠ 0) : Z ∈ (S.threeStepControlFamily hlocal).isoClosure

The manuscript's U₃ clause: an indecomposable through which a morphism out of a U₂ term factors with both factors nonzero belongs to the three-step control family. In the application the target is a U₂ term as well.

noncomputable def MagnitudeConjecture.CoveringHom.finiteFiberControlSeed {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (X : C) : FiniteIndecomposableModuleFamily

The finite seed family representing the manuscript's set H_x of indecomposables nonzero at the base object x.

theorem MagnitudeConjecture.CoveringHom.finiteFiberControlSeed_obj_nontrivial {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (X : C) (i : Fin (finiteFiberControlSeed hlocal X).n) : Nontrivial ↑(((finiteFiberControlSeed hlocal X).obj i).obj.obj.obj X)

Every representative retained in the fibre seed is genuinely nonzero at the base object. This exactness prevents an overcomplete local-finiteness witness from changing a local-density sum.

theorem MagnitudeConjecture.CoveringHom.mem_finiteFiberControlSeed_isoClosure {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (X : C) {M : ControlFiniteModule k C} (hM : CategoryTheory.Indecomposable M) (hMX : Nontrivial ↑(M.obj.obj.obj X)) : M ∈ (finiteFiberControlSeed hlocal X).isoClosure

Every indecomposable finite module nonzero at x belongs to the isomorphism-saturated seed window represented by finiteFiberControlSeed.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.finiteThreeStepControlFamily {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) (X : C) : FiniteIndecomposableModuleFamily

The manuscript's three successive indecomposable Hom neighborhoods of H_x, represented by one finite family.