Intrinsic local density in a locally representation-finite module category

The manuscript defines the local density at an indecomposable module from the total number of occurrences in a sink map and from projectivity of the endpoint. Local representation-finiteness supplies a right almost-split map without choosing a global finite skeleton; minimalization and finite Krull--Schmidt decomposition then make this definition literal. Uniqueness of minimal right almost-split maps proves independence from all choices.

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

A minimal right almost-split sink together with a displayed finite indecomposable decomposition of its source.

• source : FiniteDimensionalModuleCategory k
• map : self.source ⟶ M
• rightAlmostSplit : QuotientSubmoduleEquidistribution.IsRightAlmostSplit self.map
• rightMinimal : QuotientSubmoduleEquidistribution.IsRightMinimal self.map
• decomposition : CategoryTheory.FiniteIndecomposableDecomposition self.source

noncomputable def MagnitudeConjecture.CoveringHom.finiteModuleMinimalSinkData {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) : FiniteModuleMinimalSinkData M

Local representation-finiteness chooses a finite minimal sink at every indecomposable finite module.

noncomputable def MagnitudeConjecture.CoveringHom.finiteModuleLocalDensity {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) : ℤ

The manuscript's local density ρ_C(M): twice the nonprojective indicator minus the number of indecomposable occurrences in a minimal sink source.

theorem MagnitudeConjecture.CoveringHom.finiteModuleMinimalSinkData_arity_eq {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} (d : CategoryTheory.FiniteIndecomposableDecomposition E) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) : (finiteModuleMinimalSinkData hlocal M hM).decomposition.n = d.n

The chosen minimal-sink arity agrees with every displayed decomposition of every other minimal right almost-split source at the same endpoint.

theorem MagnitudeConjecture.CoveringHom.finiteModuleLocalDensity_eq_of_minimalRightAlmostSplitDecomposition {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} (d : CategoryTheory.FiniteIndecomposableDecomposition E) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) : finiteModuleLocalDensity hlocal M hM = ARCount.localDensityOfIncomingArity d.n (CategoryTheory.Projective M)

Any displayed finite decomposition of a minimal sink computes the intrinsic local density.

theorem MagnitudeConjecture.CoveringHom.finiteModuleLocalDensity_eq_of_iso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hlocal : IsLocallyRepresentationFinite) {M N : FiniteDimensionalModuleCategory k} (hM : CategoryTheory.Indecomposable M) (hN : CategoryTheory.Indecomposable N) (e : M ≅ N) : finiteModuleLocalDensity hlocal M hM = finiteModuleLocalDensity hlocal N hN

Local density depends only on the isomorphism class of the represented indecomposable module.