exists_linearEquiv_dfinsupp — Mathlib

English

There exists a linear equivalence between M and a DFinsupp representation built from simple components.

Русский

Существует линейное эквивалентное отображение между M и представлением DFinsupp, составленным из простых компонент.

LaTeX

$$∃ s e, ∀ m : s.Elem, IsSimpleModule R (m.1)$$

Lean4

theorem exists_linearEquiv_dfinsupp [IsSemisimpleModule R M] :
    ∃ (s : Set (Submodule R M)) (_ : M ≃ₗ[R] Π₀ m : s, m.1), sSupIndep s ∧ ∀ m : s, IsSimpleModule R m.1 :=
  by
  have ⟨s, ind, sSup, simple⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
  refine ⟨s, ?_, ind, SetCoe.forall.mpr simple⟩
  rw [sSupIndep_iff] at ind
  classical
    exact
    .symm <|
      .trans (.ofInjective _ ind.dfinsupp_lsum_injective) <|
        .trans (.ofEq _ ⊤ <| by rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']) Submodule.topEquiv

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