English
The isotypic component of a fully invariant submodule is itself fully invariant.
Русский
Изотипическая компонента полностью инвариантного подподмодуля сам является полностью инвариантной.
LaTeX
$$$$ (\\mathrm{isotypicComponent}(R,M,S)).IsFullyInvariant. $$$$
Lean4
/-- The Galois coinsertion from sets of isotypic components to fully invariant submodules. -/
def setIsotypicComponents :
GaloisCoinsertion (α := Set (isotypicComponents R M)) (β := fullyInvariantSubmodule R M)
(fun s ↦ ⨆ c ∈ s, ⟨c, .of_mem_isotypicComponents c.2⟩) fun m ↦ {c | c.1 ≤ m} :=
GaloisConnection.toGaloisCoinsertion (fun _ _ ↦ iSup₂_le_iff) fun s c hc ↦
of_not_not fun hcs ↦
(bot_lt_isotypicComponents c.2).ne' <|
(sSupIndep_isotypicComponents R M c.2).eq_bot_of_le <|
hc.trans <| by
simp_rw [CompleteSublattice.coe_iSup, iSup₂_le_iff]
exact fun c hc ↦ le_sSup ⟨c.2, Subtype.coe_ne_coe.mpr (ne_of_mem_of_not_mem hc hcs)⟩
