Local representation-finiteness for finite functor modules

The manuscript's local representation-finiteness condition is recorded without choosing a global skeleton: at each object of the base category, a finite family represents every indecomposable module nonzero there. Finite support turns these pointwise families into a finite target Hom neighborhood for any fixed module.

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

A finite family representing all indecomposable finite modules nonzero at one base-category object.

• n : ℕ
• obj : Fin self.n → FiniteDimensionalModuleCategory k
• indecomposable (j : Fin self.n) : CategoryTheory.Indecomposable (self.obj j)
• covers {Y : FiniteDimensionalModuleCategory k} : CategoryTheory.Indecomposable Y → Nontrivial ↑(Y.obj.obj.obj X) → ∃ (j : Fin self.n), Nonempty (self.obj j ≅ Y)

def MagnitudeConjecture.CoveringHom.IsLocallyRepresentationFinite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Prop

Only finitely many isomorphism classes of indecomposable finite modules are nonzero at each object of the base category.

noncomputable def MagnitudeConjecture.CoveringHom.finiteIndecomposableTargetNeighborhood_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 : FiniteDimensionalModuleCategory k) : CategoryTheory.FiniteIndecomposableTargetNeighborhood M

A finite-support module has only finitely many indecomposable target neighbors in a locally representation-finite module category.

noncomputable def MagnitudeConjecture.CoveringHom.finiteIndecomposableSourceNeighborhood_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 : FiniteDimensionalModuleCategory k) : CategoryTheory.FiniteIndecomposableSourceNeighborhood M

A finite-support module has only finitely many indecomposable source neighbors in a locally representation-finite module category.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_exists_leftAlmostSplit_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 : FiniteDimensionalModuleCategory k} (hM : CategoryTheory.Indecomposable M) : ∃ (E : FiniteDimensionalModuleCategory k) (f : M ⟶ E), QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f

Finite radical evaluation gives a left almost-split map from every indecomposable finite module under local representation-finiteness.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_exists_rightAlmostSplit_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 : FiniteDimensionalModuleCategory k} (hM : CategoryTheory.Indecomposable M) : ∃ (E : FiniteDimensionalModuleCategory k) (f : E ⟶ M), QuotientSubmoduleEquidistribution.IsRightAlmostSplit f

Finite radical coevaluation gives a right almost-split map to every indecomposable finite module under local representation-finiteness.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_exists_mono_leftAlmostSplit_of_locallyRepresentationFinite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.EnoughInjectives (FiniteDimensionalModuleCategory k)] (hlocal : IsLocallyRepresentationFinite) {M : FiniteDimensionalModuleCategory k} (hM : CategoryTheory.Indecomposable M) (hMnot : ¬CategoryTheory.Injective M) : ∃ (E : FiniteDimensionalModuleCategory k) (f : M ⟶ E), CategoryTheory.Mono f ∧ QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f

At a noninjective indecomposable, the finite radical-evaluation map can be chosen monic whenever the finite module category has enough injectives.