linearEquiv_of_ne_zero — Mathlib

English

If f: M → N is a nonzero map, there exists a submodule S ⊆ M such that N is linearly isomorphic to S.

Русский

Если существует ненулевое отображение f: M → N, то существует подмодуль S ⊆ M с $N \cong S$.

LaTeX

$$$[IsSemisimpleModule R M] \\Rightarrow \\exists S:\\ Submodule R M, \\, Nonempty (N \\cong S).$$$

Lean4

theorem linearEquiv_of_ne_zero [IsSemisimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f ≠ 0) :
    ∃ S : Submodule R M, Nonempty (N ≃ₗ[R] S) :=
  have ⟨m, (_ : IsSimpleModule R m), ne⟩ :=
    exists_ne_zero_of_sSup_eq_top h _ (IsSemisimpleModule.sSup_simples_eq_top ..)
  ⟨m, ⟨.symm <| .ofBijective _ ((bijective_or_eq_zero _).resolve_right ne)⟩⟩

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