linearEquiv_finsupp — Mathlib

English

Same as above under nontriviality of M; there exists ι and a linear isomorphism M ≃ ι →₀ S with S simple.

Русский

То же самое при не тривиальности M: существует ι и линейное изоморфизм M ≃ ι →₀ S с S простым.

LaTeX

$$$IsIsotypicOfType(R, M, S) \land [Nontrivial M] \Rightarrow \exists \iota, Nonempty (M \cong_{R} \iota \to_{0} S)$$$

Lean4

theorem linearEquiv_finsupp [Nontrivial M] (h : IsIsotypic R M) :
    ∃ (ι : Type u) (_ : Nonempty ι) (S : Submodule R M), IsSimpleModule R S ∧ Nonempty (M ≃ₗ[R] ι →₀ S) :=
  by
  have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)
  rw [← isSimpleModule_iff_isAtom] at hS
  have ⟨ι, e⟩ := (h S).linearEquiv_finsupp
  exact ⟨ι, (isEmpty_or_nonempty ι).resolve_left fun _ ↦ not_subsingleton _ (e.some.subsingleton), S, hS, e⟩

Похожие утверждения