instIsClosedImmersionSndScheme — Mathlib

English

In a pullback diagram with a closed immersion g: Y → Z, the first projection fst: X ×_Z Y → X is a closed immersion.

Русский

В диаграмме вытягивания с замкнутым вложением g: Y → Z первая проекция fst: X ×_Z Y → X — замкнутое вложение.

LaTeX

$$$IsClosedImmersion(g) \\Rightarrow IsClosedImmersion( Limits.pullback.fst f g)$$$

Lean4

instance {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion f] : IsClosedImmersion (Limits.pullback.snd f g) :=
  MorphismProperty.pullback_snd _ _ ‹_›

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