eq_isotypicComponent_of_le — Mathlib

English

If c ∈ isotypicComponents and S ≤ c with S simple, then c equals the isotypicComponent determined by S.

Русский

Если c принадлежит isotypicComponents и S ≤ c с S простым, то c равно изотипической компоненте, определяемой S.

LaTeX

$$$$ c \\in \\mathrm{isotypicComponents}(R,M) \\; \\wedge \\; S \\le c \\; (S \\text{ прост}) \\Rightarrow c = \\mathrm{isotypicComponent}(R,M,S). $$$$

Lean4

theorem eq_isotypicComponent_of_le {S c : Submodule R M} (hc : c ∈ isotypicComponents R M) [IsSimpleModule R S]
    (le : S ≤ c) : c = isotypicComponent R M S :=
  by
  obtain ⟨S', _, rfl⟩ := hc
  have ⟨e⟩ := isIsotypicOfType_submodule_iff.mp (.isotypicComponent R M S') _ le
  exact e.symm.isotypicComponent_eq

Похожие утверждения