Almost-split maps from finite Hom neighborhoods

Finite radical evaluation does not require a globally finite indecomposable skeleton. For a fixed indecomposable source or target it is enough to have finitely many indecomposable representatives covering the other endpoints of its nonzero morphisms. These are the local forms needed for a locally representation-finite covering category.

def MagnitudeConjecture.CategoryTheory.radicalHomSubmodule (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) : Submodule k (X ⟶ Y)

The categorical radical as a linear subspace of a Hom space.

structure MagnitudeConjecture.CategoryTheory.FiniteIndecomposableTargetNeighborhood {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (M : C) : Type u

A finite list of indecomposable targets covering every nonzero morphism from M to an indecomposable object.

• n : ℕ
• obj : Fin self.n → C
• indecomposable (j : Fin self.n) : CategoryTheory.Indecomposable (self.obj j)
• covers {Y : C} : CategoryTheory.Indecomposable Y → ∀ (f : M ⟶ Y), f ≠ 0 → ∃ (j : Fin self.n), Nonempty (self.obj j ≅ Y)

structure MagnitudeConjecture.CategoryTheory.FiniteIndecomposableSourceNeighborhood {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (M : C) : Type u

A finite list of indecomposable sources covering every nonzero morphism from an indecomposable object to M.

• n : ℕ
• obj : Fin self.n → C
• indecomposable (j : Fin self.n) : CategoryTheory.Indecomposable (self.obj j)
• covers {X : C} : CategoryTheory.Indecomposable X → ∀ (f : X ⟶ M), f ≠ 0 → ∃ (j : Fin self.n), Nonempty (self.obj j ≅ X)

theorem MagnitudeConjecture.CategoryTheory.exists_leftAlmostSplit_of_finiteIndecomposableTargetNeighborhood (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (decomposition : ∀ (X : C), Nonempty (FiniteIndecomposableDecomposition X)) {M : C} (hM : CategoryTheory.Indecomposable M) [IsLocalRing (CategoryTheory.End M)] (N : FiniteIndecomposableTargetNeighborhood M) : ∃ (E : C) (f : M ⟶ E), QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f

Finite radical evaluation over a target neighborhood gives a left almost-split map from the chosen indecomposable source.

theorem MagnitudeConjecture.CategoryTheory.exists_rightAlmostSplit_of_finiteIndecomposableSourceNeighborhood (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (decomposition : ∀ (X : C), Nonempty (FiniteIndecomposableDecomposition X)) {M : C} (hM : CategoryTheory.Indecomposable M) [IsLocalRing (CategoryTheory.End M)] (N : FiniteIndecomposableSourceNeighborhood M) : ∃ (E : C) (f : E ⟶ M), QuotientSubmoduleEquidistribution.IsRightAlmostSplit f

Finite radical coevaluation over a source neighborhood gives a right almost-split map to the chosen indecomposable target.