isIsotypic_iff_isFullyInvariant_imp_bot_or_top

English

For an IsSemisimpleModule M, isotypicComponent(R,M,S) = ⊤ iff IsIsotypicOfType(R,M,S).

Русский

Для полусемисимплексного модуля M, изотипическая компонента равна верхнему подпмодулю тогда и только тогда, когда M изотипичен по типу S.

LaTeX

$$$$ \\mathrm{isotypicComponent}(R,M,S) = \\top \\iff \\mathrm{IsIsotypicOfType}(R,M,S). $$$$

Lean4

theorem isIsotypic_iff_isFullyInvariant_imp_bot_or_top :
    IsIsotypic R M ↔ ∀ N : Submodule R M, N.IsFullyInvariant → N = ⊥ ∨ N = ⊤
    where
  mp h N
    hN :=
    (eq_bot_or_exists_simple_le N).imp_right fun ⟨S, le, _⟩ ↦
      top_unique <|
        (isotypicComponent_eq_top_iff.mpr (h S)).ge.trans
          ((isFullyInvariant_iff_le_imp_isotypicComponent_le.mp hN) _ le)
  mpr h S
    _ :=
    isotypicComponent_eq_top_iff.mp <| (h _ (.isotypicComponent R M S)).resolve_left (bot_lt_isotypicComponent S).ne'

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