English
The set of isotypic components of a semisimple module M over R is in order-preserving bijection with the lattice of fully invariant submodules of M. In particular, the lattice of fully invariant submodules forms a complete atomic Boolean algebra.
Русский
Множество изотипических компонент полупрямого модуля M над R образует биективное соответствие сохраняющее порядок между набором полностью инвариантных подмодулов M. Следовательно, множество полностью инвариантных подмодулов образует полную атомарную булеву алгебру.
LaTeX
$$$\\mathrm{setIsotypicComponents} : \\mathrm{Set} \\big( \\mathrm{isotypicComponents} \\; R\\; M \\big) \\simeq_{\\mathrm{ord}} \\mathrm{fullyInvariantSubmodule} \\; R\\; M$ \\\\ \\text{and} \\\\ \\mathrm{fullyInvariantSubmodule} \\; R\\; M \\text{ forms a complete atomic Boolean algebra.}$$
Lean4
/-- Sets of isotypic components in a semisimple module are in order-preserving 1-1
correspondence with fully invariant submodules. Consequently, the fully invariant submodules
form a complete atomic Boolean algebra. -/
@[simps]
def setIsotypicComponents : Set (isotypicComponents R M) ≃o fullyInvariantSubmodule R M
where
toFun s := ⨆ c ∈ s, ⟨c, .of_mem_isotypicComponents c.2⟩
invFun m := {c | c.1 ≤ m}
left_inv := (GaloisCoinsertion.setIsotypicComponents R M).u_l_eq
right_inv
m :=
(iSup₂_le fun _ ↦ by exact id).antisymm <|
(sSup_simples_le m.1).ge.trans <|
sSup_le fun S ⟨simple, le⟩ ↦
S.le_isotypicComponent.trans <|
by
let c : isotypicComponents R M := ⟨_, S, simple, rfl⟩
simp_rw [← show c.1 = isotypicComponent R M S from rfl, CompleteSublattice.coe_iSup]
exact le_biSup _ (isFullyInvariant_iff_le_imp_isotypicComponent_le.mp m.2 _ le)
map_rel_iff' := (GaloisCoinsertion.setIsotypicComponents R M).l_le_l_iff
