instQuasiSeparatedSndScheme — Mathlib

English

If X ⟶ S and Y ⟶ S with f being a quasi-separated morphism, then the second projection from the fiber product X ×_S Y to Y is quasi-separated.

Русский

Если f:x→S и g:y→S и f квазиразделим, то projection snd из произведения по основанию к Y сохраняет квазиразделимость.

LaTeX

$$$\\forall X,Y,S \\; (f:X\\to S)\\,(g:Y\\to S),\\ [\\mathrm{QuasiSeparated}\\; f] \\Rightarrow \\mathrm{QuasiSeparated}(\\mathrm{pullback.snd}\\,f\\,g).$$$

Lean4

instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiSeparated f] : QuasiSeparated (pullback.snd f g) :=
  MorphismProperty.pullback_snd f g inferInstance

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