English
Let M be a semisimple module over a ring R and m a submodule of M. Then m lies in the collection of isotypic components of M if and only if m is isotypic, m is fully invariant, and m is nonzero.
Русский
Пусть M — полупрямой модуль над кольцом R и m — подмодуль M. Тогда m принадлежит множеству изотипических компонент M тогда и только тогда, когда m является изотипическим подмодулем, полностью инвариантен и отличный от нуля.
LaTeX
$$$m \\in \\mathrm{isotypicComponents}\\; R\\; M \\;\\iff\\; \\mathrm{IsIsotypic}(R,m) \\wedge \\mathrm{IsFullyInvariant}(m) \\wedge m \\neq \\bot$$$
Lean4
theorem mem_isotypicComponents_iff {m : Submodule R M} :
m ∈ isotypicComponents R M ↔ IsIsotypic R m ∧ m.IsFullyInvariant ∧ m ≠ ⊥
where
mp := by rintro ⟨S, _, rfl⟩;
exact ⟨.isotypicComponent R M S, .isotypicComponent R M S, (bot_lt_isotypicComponent S).ne'⟩
mpr := fun ⟨iso, invar, ne⟩ ↦
have ⟨S, le, simple⟩ := (eq_bot_or_exists_simple_le m).resolve_left ne
⟨S, simple, (eq_isotypicComponent_iff ne).mpr ⟨isIsotypic_submodule_iff.mp iso S le, invar⟩⟩
