English
For semisimple M, IsIsotypic R M is equivalent to: every fully invariant submodule is either 0 or M.
Русский
Для полусемисимплексного модуля M условие IsIsotypic эквивалентно: любой полностью инвариантный подпомодуль равен 0 или M.
LaTeX
$$$$ \\mathrm{IsIsotypic}(R,M) \\iff \\forall N \\subseteq M, N \\text{IsFullyInvariant } \\Rightarrow N = 0 \\text{ or } N = M. $$$$
Lean4
theorem isFullyInvariant_iff_le_imp_isotypicComponent_le [IsSemisimpleModule R M] {m : Submodule R M} :
m.IsFullyInvariant ↔ ∀ S ≤ m, [IsSimpleModule R S] → isotypicComponent R M S ≤ m
where
mp h S le
_ :=
sSup_le fun S' ⟨e⟩ ↦
by
have ⟨p, eq⟩ := extension_property _ S.subtype_injective (S'.subtype ∘ₗ e.symm)
refine le_trans ?_ (Submodule.map_le_iff_le_comap.mpr (le.trans (h p)))
rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]
mpr h
f :=
(sSup_simples_le m).ge.trans <|
sSup_le fun S ⟨_, le⟩ ↦ Submodule.map_le_iff_le_comap.mp ((S.map_le_isotypicComponent f).trans (h S le))
