submodule_linearEquiv_fun — Mathlib

English

If h : IsIsotypic R m for a submodule m of M, then there exist n, a simple S ≤ m and an isomorphism m ≃ Fin n → S.

Русский

Если m — изотипичный подмодуль, то существует n и простой S ≤ m, а также изоморфизм m ≃ Fin n → S.

LaTeX

$$$h : IsIsotypic(R, m) \Rightarrow \exists n, \exists S \le m, IsSimpleModule(R, S) ∧ Nonempty (m \cong_{R} Fin n \to S)$$$

Lean4

theorem submodule_linearEquiv_fun {m : Submodule R M} [Module.Finite R m] [Nontrivial m] (h : IsIsotypic R m) :
    ∃ (n : ℕ) (_ : NeZero n) (S : Submodule R M), S ≤ m ∧ IsSimpleModule R S ∧ Nonempty (m ≃ₗ[R] Fin n → S) :=
  have ⟨n, hn, S, _, ⟨e⟩⟩ := h.linearEquiv_fun
  let e' := S.equivMapOfInjective _ m.subtype_injective
  ⟨n, hn, _, m.map_subtype_le S, .congr e'.symm, ⟨e.trans <| .piCongrRight fun _ ↦ e'⟩⟩

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