isFinitelySemisimple_sub_algebraMap_iff

English

For any μ, (f − algebraMap R (End R M) μ) IsFinitelySemisimple ⇔ f.IsFinitelySemisimple.

Русский

Для любого μ, (f − algebraMap R (End R M) μ) IsFinitelySemisimple ⇔ f.IsFinitelySemisimple.

LaTeX

$$$ (f - algebraMap(R, End_R(M))\, \mu).IsFinitelySemisimple \iff f.IsFinitelySemisimple$$$

Lean4

@[simp]
theorem isFinitelySemisimple_sub_algebraMap_iff {μ : R} :
    (f - algebraMap R (End R M) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple :=
  by
  suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, 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)

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