isJacobsonRing_of_isIntegral' — Mathlib

English

If there exists a ring homomorphism f: R → S which is integral and R is Jacobson, then S is Jacobson.

Русский

Если существует кольцевой гомоморфизм f: R → S, который интегрален, и R — кольцо Якобсона, то S также является кольцом Якобсона.

LaTeX

$$$IsJacobsonRing(R) \\rightarrow (\\exists f: R \\to R[S]?; \\text{IsIntegral}(f)) \\rightarrow IsJacobsonRing(S)$$$

Lean4

/-- A variant of `isJacobsonRing_of_isIntegral` that takes `RingHom.IsIntegral` instead. -/
theorem isJacobsonRing_of_isIntegral' (f : R →+* S) (hf : f.IsIntegral) [IsJacobsonRing R] : IsJacobsonRing S :=
  let _ : Algebra R S := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  isJacobsonRing_of_isIntegral (R := R)

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