English
A binary product of semisimple rings is semisimple: if R and S are semisimple rings, then R × S is semisimple.
Русский
Двоичное произведение полносемповых колец полносемплово.
LaTeX
$$$\\text{IsSemisimpleRing}(R) \\land \\text{IsSemisimpleRing}(S) \\Rightarrow \\text{IsSemisimpleRing}(R \\times S).$$$
Lean4
/-- A binary product of semisimple rings is semisimple. -/
instance [hR : IsSemisimpleRing R] [hS : IsSemisimpleRing S] : IsSemisimpleRing (R × S) :=
by
letI : Module (R × S) R := Module.compHom _ (.fst R S)
letI : Module (R × S) S :=
Module.compHom _
(.snd R S)
-- e₁, e₂ got falsely flagged by the unused argument linter
let _e₁ : R →ₛₗ[.fst R S] R := { AddMonoidHom.id R with map_smul' := fun _ _ ↦ rfl }
let _e₂ : S →ₛₗ[.snd R S] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR
rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS
rw [IsSemisimpleRing, ← Submodule.topEquiv.isSemisimpleModule_iff_of_bijective (LinearEquiv.bijective _), ←
LinearMap.sup_range_inl_inr]
exact .sup (.range _) (.range _)
