Finite-dimensional modules decompose into indecomposables

The standard existence half of Krull--Schmidt is proved by strong induction on the coefficient-field dimension. This is a bounded adaptation of the module specialization in the Cartan formalization's ClosedRayChain/GenericFiniteness.lean at commit eade4e75.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.summand_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {M : ModuleCat A} (d : FiniteIndecomposableDecomposition M) (hM : Module.Finite k ↑M) (j : Fin d.n) : Module.Finite k ↑(d.summand j)

Every displayed indecomposable summand of a finite-dimensional module is again finite-dimensional.

theorem MagnitudeConjecture.finiteIndecomposableDecomposition_module_exists {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [Module.Finite k A] (M : ModuleCat A) [Module.Finite k ↑M] : Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M)

Every finite-dimensional module over a finite-dimensional algebra is a finite biproduct of indecomposable modules.

theorem MagnitudeConjecture.finiteIndecomposableDecomposition_fgModule_exists {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [Module.Finite k A] [IsNoetherianRing A] (M : FGModuleCat A) [Module.Finite k ↑M] : Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M)

Every finitely generated module that is finite-dimensional over the coefficient field admits a finite indecomposable decomposition inside FGModuleCat.