isOpenEmbedding_of_pullback — Mathlib

English

If X -> S and Y -> S are open embeddings, then the pullback map limit.π is an open embedding.

Русский

Если X -> S и Y -> S — открытые вложения, то предел limit.π является открытым вложением.

LaTeX

$$$ \text{IsOpenEmbedding}\left( \text{limit.\,π}(\mathrm{cospan}\ f\ g)\ WalkingCospan.one \right) $$$

Lean4

/-- If `X ⟶ S`, `Y ⟶ S` are open embeddings, then so is `X ×ₛ Y ⟶ S`. -/
theorem isOpenEmbedding_of_pullback {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsOpenEmbedding f)
    (H₂ : IsOpenEmbedding g) : IsOpenEmbedding (limit.π (cospan f g) WalkingCospan.one) :=
  by
  convert H₂.comp (snd_isOpenEmbedding_of_left H₁ g)
  rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]
  rfl

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