instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier

English

If R is Jacobson, then Spec R is a Jacobson space (in the category of rings).

Русский

Если R — кольцо Джейкобсона, то Spec R — пространство Джейкобсона (в контексте категории колец).

LaTeX

$$$\\text{IsJacobsonRing}(R) \\Rightarrow \\text{JacobsonSpace}(\\Spec R)$$$

Lean4

instance {R : CommRingCat} [IsJacobsonRing R] : JacobsonSpace (Spec R) :=
  inferInstanceAs (JacobsonSpace (PrimeSpectrum R))

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