le_isotypicComponent_iff — Mathlib

English

For a simple S and submodule S ≤ M, we have a relation between leq to isotypic component and type isotypic.

Русский

Для простого S и подподмодуля S ≤ M существует связь между отношением включения S и изотипической компонентой и типом изотипическости.

LaTeX

$$$$ S \\le m \\Rightarrow (S \\text{ isotypicComponent}) \\iff \\mathrm{IsIsotypicOfType}(R,S). $$$$

Lean4

theorem le_isotypicComponent_iff [IsSemisimpleModule R M] {m : Submodule R M} :
    m ≤ isotypicComponent R M S ↔ IsIsotypicOfType R m S
    where
  mp h := .of_injective (.isotypicComponent R M S) _ (Submodule.inclusion_injective h)
  mpr
    h :=
    (IsSemisimpleModule.sSup_simples_le m).ge.trans
      (sSup_le_sSup fun S ⟨_, le⟩ ↦ isIsotypicOfType_submodule_iff.mp h S le)

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