Arrow multiplicities under linear realizations of module categories #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_eq_irreducible_finrank_of_equivalence
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
{C : Type v}
[CategoryTheory.Category.{u, v} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(E : FGModuleCat Aᵐᵒᵖ ≌ C)
[E.functor.Additive]
[CategoryTheory.Functor.Linear k E.functor]
(source target : Fin S.n)
:
FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData source target = Module.finrank k (CategoricalIrreducible.Space k (E.functor.obj (S.fgObj source)) (E.functor.obj (S.fgObj target)))
The official arrow multiplicity is the intrinsic quotient dimension in any linearly equivalent realization of the module category.