instOfIsIsoScheme — Mathlib

English

For a surjective ring morphism, the induced Spec map is a closed immersion with surjective stalk maps.

Русский

Для сюръективного кольцевого морфизма индуцированное отображение Spec — закрытое вложение с сюръективными морфизмами стойков.

LaTeX

$$$\text{surjective}(f) \Rightarrow IsClosedImmersion(\mathrm{Spec.map} f)$$$

Lean4

/-- Isomorphisms are closed immersions. -/
instance {X Y : Scheme} (f : X ⟶ Y) [IsIso f] : IsClosedImmersion f
    where
  base_closed := Homeomorph.isClosedEmbedding <| TopCat.homeoOfIso (asIso f.base)
  surj_on_stalks := fun _ ↦ (ConcreteCategory.bijective_of_isIso _).2

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