instIsClosedImmersionMapDescScheme

English

Pullback map with diagonal is a closed immersion in the separated setting for various schemes.

Русский

Карта pullback с диагональю является замкнутым погружением в обстановке разделённости.

LaTeX

$$$\forall X,Y,S,T\; (f:X\to S) (g:Y\to S) (i:S\to T)[IsSeparated i] : IsClosedImmersion( pullback.mapDesc f g i ).$$$

Lean4

instance {S T : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [IsSeparated i] :
    IsClosedImmersion (pullback.mapDesc f g i) :=
  MorphismProperty.of_isPullback (pullback_map_diagonal_isPullback f g i) inferInstance

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