English
A submodule N ⊂ M is fully invariant if N is mapped into itself by every R-linear endomorphism of M; equivalently, N is stable under all endomorphisms of M.
Русский
Подмодуль N ⊂ M полностью инвариантен, если он инвариантен относительно каждого R-линейного эндоморфизма M; т.е. N стабилен под всеми эндоморфизмами M.
LaTeX
$$$$ \\text{IsFullyInvariant}(N) \\iff \\forall f ∈ \\mathrm{End}_R(M),\\; N \\le N^{\,f}. $$$$
Lean4
/-- A submodule `N` an `R`-module `M` is fully invariant if `N` is mapped into itself by all
`R`-linear endomorphisms of `M`.
If `M` is semisimple, this is equivalent to `N` being a sum of isotypic components of `M`:
see `isFullyInvariant_iff_sSup_isotypicComponents`. -/
def IsFullyInvariant (N : Submodule R M) : Prop :=
∀ f : Module.End R M, N ≤ N.comap f
