English
Let {M_i} be a family of modules over a ring R. Then the Jacobson radical of the direct product ∏_i M_i is contained in the coordinatewise Jacobson radical, i.e. Jac_R(∏_i M_i) ⊆ Submodule.pi Set.univ (Jac_R(M_i)).
Русский
Пусть {M_i} — семья модулей над кольцом R. Тогда Якобсонов радикал прямого произведения ∏_i M_i содержится в поперечном радикале по координатам, то есть Jac_R(∏_i M_i) ⊆ Submodule.pi(Set.univ, Jac_R(M_i)).
LaTeX
$$$\\operatorname{jacobson}_R\\Big(\\prod_{i} M_i\\Big) \\le \\operatorname{Submodule.pi} (\\mathrm{Set.univ})\\Big(\\operatorname{jacobson}_R\\big(M_i\\big)\\Big).$$$
Lean4
theorem jacobson_pi_le : jacobson R (Π i, M i) ≤ Submodule.pi Set.univ (jacobson R <| M ·) :=
by
simp_rw [← iInf_comap_proj, jacobson, sInf_eq_iInf', comap_iInf, le_iInf_iff]
intro i m
exact iInf_le_of_le ⟨_, (isCoatom_comap_iff <| LinearMap.proj_surjective i).mpr m.2⟩ le_rfl
