linearEquiv_finsupp — Mathlib

English

If M is isotypic to S, there exists an index set ι such that M ≅ ι →₀ S (DFinsupp) as linear modules.

Русский

Если M изотипичен к S, существует множество индексов ι, такое что M ≅ ι →₀ S как линейные модули.

LaTeX

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

Lean4

theorem linearEquiv_finsupp (h : IsIsotypicOfType R M S) : ∃ ι : Type u, Nonempty (M ≃ₗ[R] ι →₀ S) :=
  by
  have ⟨s, e, _, hs⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
  classical
    exact
    ⟨s, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun m : s ↦ (h m.1).some) |>.trans (finsuppLequivDFinsupp R).symm⟩⟩

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