English
For a nonzero submodule m of a semisimple M, m equals the S-isotypic component iff m is IsIsotypicOfType and m is fully invariant.
Русский
Для ненулевого подмодуля m в полусемисимплексном M, равенство m и S-изотипической компоненты эквивалентно тому, что m изотипично относительно S и полностью инвариантен.
LaTeX
$$$$ m \\neq 0 \\implies (m = \\mathrm{isotypicComponent}(R,M,S) \\iff (\\mathrm{IsIsotypicOfType}(R,m,S) \\land m.\\mathrm{IsFullyInvariant})). $$$$
Lean4
theorem eq_isotypicComponent_iff [IsSemisimpleModule R M] {m : Submodule R M} (ne : m ≠ ⊥) :
m = isotypicComponent R M S ↔ IsIsotypicOfType R m S ∧ m.IsFullyInvariant
where
mp := by rintro rfl; exact ⟨.isotypicComponent R M S, .isotypicComponent R M S⟩
mpr := fun ⟨iso, invar⟩ ↦
(le_isotypicComponent_iff.mpr iso).antisymm <|
have ⟨S', le, _⟩ := (IsSemisimpleModule.eq_bot_or_exists_simple_le m).resolve_left ne
(isIsotypicOfType_submodule_iff.mp iso S' le).some.symm.isotypicComponent_eq.trans_le
(isFullyInvariant_iff_le_imp_isotypicComponent_le.mp invar _ le)
