Incoming arrow sums for a numbered family under an equivalence

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ofFGFamily_inverse_incoming_sum_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type} [Fintype ι] {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] (H : ι → C) (hi : ∀ (i : ι), CategoryTheory.Indecomposable (E.inverse.obj (H i))) (hc : ∀ (X : FinitelyGeneratedCategory A), CategoryTheory.Indecomposable X → ∃ (i : ι), Nonempty (X ≅ E.inverse.obj (H i))) (hs : ∀ (i j : ι), Nonempty (E.inverse.obj (H i) ≅ E.inverse.obj (H j)) → i = j) (j : Fin (Fintype.card ι)) : ∑ i : Fin (Fintype.card ι), FiniteTauMatrix.arrowMultiplicity (ofFGFamily (fun (a : ι) => E.inverse.obj (H a)) hi hc hs).finiteTauCategoryData.toFiniteRightTauCategoryData i j = ∑ a : ι, Module.finrank k (CategoricalIrreducible.Space k (H a) (H ((Fintype.equivFin ι).symm j)))

Summing the numbered arrows of an inverse-image family gives the incoming irreducible dimension sum in the original category.