map_le_isotypicComponent — Mathlib

English

For a submodule S ≤ M and a linear map f: M → N, the image S.map f is contained in the isotypic component of N corresponding to S.

Русский

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

LaTeX

$$$$ S.map f \\le \\mathrm{isotypicComponent}(R,N,S). $$$$

Lean4

theorem map_le_isotypicComponent (S : Submodule R M) [IsSimpleModule R S] (f : M →ₗ[R] N) :
    S.map f ≤ isotypicComponent R N S :=
  by
  conv_lhs => rw [← S.range_subtype, ← LinearMap.range_comp]
  obtain inj | eq := (f ∘ₗ S.subtype).injective_or_eq_zero
  · exact le_sSup ⟨.symm <| .ofInjective _ inj⟩
  · simp_rw [eq, LinearMap.range_zero, bot_le]

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