English
If M is semisimple and finite, there exists a finite index n and a linear equivalence to a finite DFinsupp representation with simple components.
Русский
Если M полупрямой и конечно-генерируемый, существует конечный индекс n и линейное эквивалентное отображение к DFinsupp-представлению с простыми компонентами.
LaTeX
$$∃ n, ∃ S : Fin n → Submodule R M, (M ≃ₗ[R] Π₀ i : Fin n, S i) ∧ ∀ i, IsSimpleModule R (S i)$$
Lean4
theorem exists_linearEquiv_fin_dfinsupp [IsSemisimpleModule R M] [Module.Finite R M] :
∃ (n : ℕ) (S : Fin n → Submodule R M) (_ : M ≃ₗ[R] Π₀ i : Fin n, S i), ∀ i, IsSimpleModule R (S i) :=
have ⟨s, e, h, simple⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
have :=
WellFoundedGT.finite_of_iSupIndep ((sSupIndep_iff _).mp h) fun S ↦
(S.1.nontrivial_iff_ne_bot).mp <| IsSimpleModule.nontrivial R S
⟨_, _, e.trans <| DirectSum.lequivCongrLeft R (Finite.equivFin s), fun _ ↦ simple _⟩
