universallyClosed_fst — Mathlib

English

Let f: X → Z and g: Y → Z be morphisms of schemes. If g is universally closed, then the projection from the fiber product X ×_Z Y to X is universally closed.

Русский

Пусть f: X → Z и g: Y → Z — морфизмы расслоения. Если g является универсально замкнутым, тогда проекция fst: X ×_Z Y → X из произведения по основанию Z является универсально замкнутым.

LaTeX

$$$\forall X\,Y\,Z\ (f:X\to Z)\ (g:Y\to Z),\; \operatorname{UniversallyClosed}(g)\Rightarrow \operatorname{UniversallyClosed}(\mathrm{pullback.fst}\; f\; g).$$$

Lean4

instance universallyClosed_fst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : UniversallyClosed g] :
    UniversallyClosed (pullback.fst f g) :=
  MorphismProperty.pullback_fst f g hg

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