Arrow multiplicities for a numbered finite module family

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ofFGFamily_fgObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type} [Fintype ι] (F : ι → FinitelyGeneratedCategory A) (hF : ∀ (i : ι), CategoryTheory.Indecomposable (F i)) (hc : ∀ (X : FinitelyGeneratedCategory A), CategoryTheory.Indecomposable X → ∃ (i : ι), Nonempty (X ≅ F i)) (hs : ∀ (i j : ι), Nonempty (F i ≅ F j) → i = j) (i : Fin (ofFGFamily F hF hc hs).n) : (ofFGFamily F hF hc hs).fgObj i ≅ F ((Fintype.equivFin ι).symm i)

Rebundling a family as a numbered skeleton preserves each representative.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ofFGFamily_arrowMultiplicity_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type} [Fintype ι] (F : ι → FinitelyGeneratedCategory A) (hF : ∀ (i : ι), CategoryTheory.Indecomposable (F i)) (hc : ∀ (X : FinitelyGeneratedCategory A), CategoryTheory.Indecomposable X → ∃ (i : ι), Nonempty (X ≅ F i)) (hs : ∀ (i j : ι), Nonempty (F i ≅ F j) → i = j) [IsAlgClosed k] (i j : Fin (ofFGFamily F hF hc hs).n) : FiniteTauMatrix.arrowMultiplicity (ofFGFamily F hF hc hs).finiteTauCategoryData.toFiniteRightTauCategoryData i j = Module.finrank k (CategoricalIrreducible.Space k (F ((Fintype.equivFin ι).symm i)) (F ((Fintype.equivFin ι).symm j)))

Numbering a finite family computes arrows by its original quotient spaces.

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

For a family realized by inverse images, numbering computes arrows on the original objects of the equivalent category.