instQuasiSeparatedFstScheme — Mathlib

English

If Y is quasi-separated in the target, then the first projection from the fiber product X ×_S Y to X is quasi-separated after base change along any map f: X → S and g: Y → S.

Русский

Если g: Y → S является квазиразделимым, то проекция fst из базопеременного произведения на X сохраняет квазиразделимость после основания по f: X → S и g: Y → S.

LaTeX

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

Lean4

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

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