English
A submodule m of M is fully invariant if and only if m is the supremum of some family of isotypic components of M.
Русский
Подмодуль m подмодуля M полностью инвариантен тогда и только тогда, когда он является супремумом некоторого семейства изотипических компонент M.
LaTeX
$$$m \\text{ IsFullyInvariant} \\;\\iff\\; \\exists s \\subseteq \\mathrm{isotypicComponents} \\; R\\; M,\\; m = \\bigvee s$$$
Lean4
theorem isFullyInvariant_iff_sSup_isotypicComponents {m : Submodule R M} :
m.IsFullyInvariant ↔ ∃ s ⊆ isotypicComponents R M, m = sSup s :=
by
refine ⟨fun h ↦ ⟨OrderIso.setIsotypicComponents.symm ⟨m, h⟩, ⟨?_, ?_⟩⟩, ?_⟩
· rintro _ ⟨c, _, rfl⟩; exact c.2
· convert Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm
simp [sSup_image, OrderIso.setIsotypicComponents, OrderIso.symm]
· rintro ⟨_, hs, rfl⟩
exact (fullyInvariantSubmodule R M).sSupClosed fun _ h ↦ .of_mem_isotypicComponents (hs h)
