isSeparated_iff_isClosedImmersion_prod_lift

English

For any X, X.IsSeparated is equivalent to IsClosedImmersion(prod.lift(id_X, id_X)).

Русский

Для любой схемы X условие X.IsSeparated эквивалентно IsClosedImmersion(prod.lift(id_X, id_X)).

LaTeX

$$X.IsSeparated \iff IsClosedImmersion\left(\mathrm{prod.lift}(\mathrm{id}_X, \mathrm{id}_X)\right)$$

Lean4

theorem isSeparated_iff_isClosedImmersion_prod_lift {X : Scheme.{u}} :
    X.IsSeparated ↔ IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X)) :=
  by
  rw [isSeparated_iff, AlgebraicGeometry.isSeparated_iff, iff_iff_eq, ←
    MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (prodIsoPullback X X).hom]
  congr
  ext : 1 <;> simp

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