iff_isPreimmersion — Mathlib

English

If a ring morphism f: R → S is surjective, then the induced Spec map Spec(S) → Spec(R) is a closed immersion.

Русский

Если отображение колец f: R → S сюръективно, то индуцированное отображение спектра Spec(S) → Spec(R) является закрытым вложением.

LaTeX

$$$\text{If } f:R\to S \text{ is surjective, then } \mathrm{Spec}(S)\to \mathrm{Spec}(R) \text{ is a closed immersion}$$$

Lean4

theorem iff_isPreimmersion {X Y : Scheme} {f : X ⟶ Y} :
    IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range f.base) := by
  rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]

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