le_comap_isotypicComponent — Mathlib

English

For a linear map f: M → N and an isotypic component S of M, the component of N pulled back along f contains the image of S.

Русский

Для линейного отображения f: M → N и изотипической компоненты S модуля M соответствующая компонента N сжатой по f содержит образ S.

LaTeX

$$$$ \\mathrm{isotypicComponent}(R,M,S) \\le \\mathrm{comap}_f(\\mathrm{isotypicComponent}(R,N,S)). $$$$

Lean4

theorem le_comap_isotypicComponent (f : M →ₗ[R] N) : isotypicComponent R M S ≤ (isotypicComponent R N S).comap f :=
  sSup_le fun m ⟨e⟩ ↦
    Submodule.map_le_iff_le_comap.mp <|
      have := IsSimpleModule.congr e
      (m.map_le_isotypicComponent f).trans_eq e.isotypicComponent_eq

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