English
A fully invariant submodule is the supremum of a subset of isotypic components if and only if it is fully invariant.
Русский
Полностью инвариантный подмодуль является супремумом подмножества изотипических компонент тогда и только тогда, когда он полностью инвариантен.
LaTeX
$$$mIsFullyInvariant \\iff ∃ s ⊆ \\mathrm{isotypicComponents} \\; R\\; M,\\; m = \\bigvee s$$$
Lean4
/-- The **Wedderburn–Artin Theorem**: an Artinian simple ring is isomorphic to a matrix
ring over the opposite of the endomorphism ring of its simple module. -/
theorem exists_ringEquiv_matrix_end_mulOpposite :
∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R I),
Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R I)ᵐᵒᵖ) :=
by
have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R).linearEquiv_fun
refine ⟨n, hn, S, hS, ⟨.trans (.opOp R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
exact .trans (.moduleEndSelf R) <| .trans e.conjRingEquiv (endVecRingEquivMatrixEnd ..)
