English
IsIsotypicOfType R M S with finite M implies existence of Finite n and S-submodule with M ≅ Fin n → S.
Русский
IsIsotypicOfType R M S при конечном M дает существование n и подподмодуля S, такой что M ≅ Fin n → S.
LaTeX
$$$IsIsotypicOfType(R, M, S) \land Module.Finite R M \Rightarrow \exists n, \exists S \le M, Nonempty (M \cong_{R} Fin n \to S) ∧ IsSimpleModule R S$$$
Lean4
theorem linearEquiv_fun [Module.Finite R M] [Nontrivial M] (h : IsIsotypic R M) :
∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), IsSimpleModule R S ∧ Nonempty (M ≃ₗ[R] Fin n → S) :=
by
have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)
rw [← isSimpleModule_iff_isAtom] at hS
have ⟨n, e⟩ := (h S).linearEquiv_fun
exact ⟨n, neZero_iff.2 <| by rintro rfl; exact not_subsingleton _ (e.some.subsingleton), S, hS, e⟩
