English
If f is surjective, Spec.map f is a closed immersion.
Русский
Если f сюръективно, Spec.map f — закрытое вложение.
LaTeX
$$$\text{surjective}(f) \Rightarrow IsClosedImmersion(\mathrm{Spec.map} f)$$$
Lean4
/-- Given two commutative rings `R S : CommRingCat` and a surjective morphism
`f : R ⟶ S`, the induced scheme morphism `specObj S ⟶ specObj R` is a
closed immersion. -/
theorem spec_of_surjective {R S : CommRingCat} (f : R ⟶ S) (h : Function.Surjective f) : IsClosedImmersion (Spec.map f)
where
base_closed := PrimeSpectrum.isClosedEmbedding_comap_of_surjective _ _ h
surj_on_stalks
x :=
by
haveI : (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso :=
by
rw [← RingHom.toMorphismProperty_respectsIso_iff]
exact RingHom.surjective_respectsIso
apply
(MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f))
(Scheme.arrowStalkMapSpecIso f x)).mpr
exact RingHom.surjective_localRingHom_of_surjective f.hom h x.asIdeal
