isSemisimple_sub_algebraMap_iff — Mathlib

English

Shifting an endomorphism by a scalar via algebraMap preserves semisimplicity: (f − algebraMap μ)^Semisimple ⇔ f^Semisimple.

Русский

Смещение эндоморфизма на скаляр через отображение алгебра сохраняет семисемпсизм: (f − algebraMap μ)^Semisimple ⇔ f^Semisimple.

LaTeX

$$$ (f - algebraMap(R, End_R(M))\, \mu) \text{ IsSemisimple} \iff f \text{ IsSemisimple}$$$

Lean4

@[simp]
theorem isSemisimple_sub_algebraMap_iff {μ : R} : (f - algebraMap R (End R M) μ).IsSemisimple ↔ f.IsSemisimple :=
  by
  suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp [mem_invtSubmodule, isSemisimple_iff, this]
  refine fun p ↦ ⟨fun h x hx ↦ ?_, fun h x hx ↦ p.sub_mem (h hx) (p.smul_mem μ hx)⟩
  simpa using p.add_mem (h hx) (p.smul_mem μ hx)

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