isSemisimpleRing_of_surjective — Mathlib

English

If f: R → S is a surjective ring homomorphism and R is semisimple, then S is semisimple.

Русский

Если кольцевое отображение f: R → S сюръективно и R полносемпло, то S полносемпло.

LaTeX

$$$\\text{IsSemisimpleRing}(R) \\land (f: R \\to \\! S) \\text{ surjective} \\Rightarrow \\text{IsSemisimpleRing}(S).$$$

Lean4

theorem isSemisimpleRing_of_surjective (f : R →+* S) (hf : Function.Surjective f) [IsSemisimpleRing R] :
    IsSemisimpleRing S := by
  letI : Module R S := Module.compHom _ f
  haveI : RingHomSurjective f := ⟨hf⟩
  let e : S →ₛₗ[f] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
  rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]
  infer_instance

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