spec_of_quotient_mk — Mathlib

English

For any commutative ring R and any ideal I ⊆ R, the natural morphism Spec(R/I) → Spec(R) is a closed immersion.

Русский

Для любого коммутативного кольца R и любого идеала I ⊆ R соответствующий морфизм Spec(R/I) → Spec(R) является замкнутым вложением.

LaTeX

$$$\\\\forall R \\,\\\\forall I \\, (I \\triangleleft R),\\\\\\ IsClosedImmersion(\\\\mathrm{Spec.map}(\\\\mathrm{CommRingCat.ofHom}(\\\\mathrm{Ideal.Quotient.mk} I)))$$$

Lean4

/-- For any ideal `I` in a commutative ring `R`, the quotient map `specObj R ⟶ specObj (R ⧸ I)`
is a closed immersion. -/
instance spec_of_quotient_mk {R : CommRingCat.{u}} (I : Ideal R) :
    IsClosedImmersion (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) :=
  spec_of_surjective _ Ideal.Quotient.mk_surjective

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