isStableUnderBaseChange — Mathlib

English

Given f: X→Y and g: Y→Z with g separated, the induced lift map X→X×[Z]Y is a closed immersion.

Русский

Дано f: X→Y и g: Y→Z с разделённостью g, индуцированная карта подъёма X→X×[Z]Y является замкнутым погружением.

LaTeX

$$$[IsSeparated g] \Rightarrow IsClosedImmersion( pullback.mapDesc f (\mathbf{1}) g ).$$$

Lean4

instance isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsSeparated :=
  by
  rw [isSeparated_eq_diagonal_isClosedImmersion]
  infer_instance

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