sheafedSpace_pullback_fst_of_right

English

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

Русский

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

LaTeX

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

Lean4

instance sheafedSpace_pullback_fst_of_right : SheafedSpace.IsOpenImmersion (pullback.fst g f) :=
  by
  delta pullback.fst
  have : _ = limit.π (cospan g f) left := preservesLimitIso_hom_π forget (cospan g f) left
  rw [← this]
  have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan g f ⋙ forget)) left
  erw [Category.comp_id] at this
  rw [← this]
  dsimp
  infer_instance

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