sheafedSpace_pullback_snd_of_left

English

If f: X → Z is an open immersion, then the projection pullback.snd f g is also an open immersion.

Русский

Если f: X → Z является открытым вложением, то проекция pullback.snd f g также открытое вложение.

LaTeX

$$$\text{IsOpenImmersion}(\text{pullback.snd}(f,g)).$$$

Lean4

/-- Open immersions are stable under base-change. -/
instance sheafedSpace_pullback_snd_of_left : SheafedSpace.IsOpenImmersion (pullback.snd f g) :=
  by
  delta pullback.snd
  have : _ = limit.π (cospan f g) right := preservesLimitIso_hom_π forget (cospan f g) right
  rw [← this]
  have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan f g ⋙ forget)) right
  erw [Category.comp_id] at this
  rw [← this]
  dsimp
  infer_instance

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