English
If M is isotypic to S (with finite generation), there exists n and a simple S-submodule with M ≅ Fin n → S.
Русский
Если M изотипичен к S и модуль конечной размерности, то существует n и простый подпереход S such that M ≅ Fin n → S.
LaTeX
$$$IsIsotypicOfType(R, M, S) \land Module.Finite R M \Rightarrow \exists n, \exists S \le M, IsSimpleModule R S ∧ Nonempty (M \cong_{R} Fin\,n \to S)$$$
Lean4
theorem linearEquiv_fun [Module.Finite R M] (h : IsIsotypicOfType R M S) : ∃ n : ℕ, Nonempty (M ≃ₗ[R] Fin n → S) :=
by
have ⟨n, S, e, hs⟩ := IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp R M
classical
exact
⟨n,
⟨e.trans (DFinsupp.mapRange.linearEquiv fun i ↦ (h (S i)).some) |>.trans (finsuppLequivDFinsupp R).symm |>.trans
(Finsupp.linearEquivFunOnFinite ..)⟩⟩
