universallyClosed_snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance universallyClosed_snd {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf : UniversallyClosed f] :
    UniversallyClosed (pullback.snd f g) :=
  MorphismProperty.pullback_snd f g hf

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