pullback_snd_of_left — Mathlib

English

Let f: X → Z be an open immersion. Then the second projection from the fiber product X ×_Z Y to Y is an open immersion.

Русский

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

LaTeX

$$$IsOpenImmersion\big( pullback.snd\, f\, g \big)$$$

Lean4

instance pullback_snd_of_left : IsOpenImmersion (pullback.snd f g) :=
  by
  have := PreservesPullback.iso_hom_snd forget f g
  dsimp only [Scheme.forgetToLocallyRingedSpace, inducedFunctor_map] at this
  change LocallyRingedSpace.IsOpenImmersion _
  rw [← this]
  infer_instance

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