A right-module skeleton from a complete finite family in FGModuleCat #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ofFGFamily
{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))
(hcomplete : ∀ (X : FinitelyGeneratedCategory A), CategoryTheory.Indecomposable X → ∃ (i : ι), Nonempty (X ≅ F i))
(hskeletal : ∀ (i j : ι), Nonempty (F i ≅ F j) → i = j)
:
Preserve the exact size of a complete family with no repeated isomorphism classes.