isSemisimple_iff — Mathlib

English

Let f: End_R(M) and g: End_R(M') be endomorphisms and e: M ≃_R M' a linear isomorphism such that e ∘ f = g ∘ e. Then f is semisimple if and only if g is semisimple.

Русский

Пусть f: End_R(M) и g: End_R(M') — эндоморфизмы, а e: M ≃_R M' — линейное изоморфизм, удовлетворяющее e ∘ f = g ∘ e. Тогда f семисемпслим тогда и только тогда, когда g семисемпслим.

LaTeX

$$$\forall R, M, M', f \in \mathrm{End}_R(M),\ g \in \mathrm{End}_R(M'), e: M \simeq_R M',\ e \circ f = g \circ e \Rightarrow IsSemisimple(f) \iff IsSemisimple(g))$$$

Lean4

protected theorem _root_.LinearEquiv.isSemisimple_iff {M₂ : Type*} [AddCommGroup M₂] [Module R M₂] (g : End R M₂)
    (e : M ≃ₗ[R] M₂) (he : e ∘ₗ f = g ∘ₗ e) : f.IsSemisimple ↔ g.IsSemisimple :=
  by
  let e : AEval' f ≃ₗ[R[X]] AEval' g :=
    LinearEquiv.ofAEval _ (e.trans (AEval'.of g)) fun x ↦ by simpa [AEval'.X_smul_of] using LinearMap.congr_fun he x
  simp_rw [IsSemisimple, isSemisimpleModule_iff, (Submodule.orderIsoMapComap e).complementedLattice_iff]

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