fst_isEmbedding_of_right — Mathlib

English

If g is an embedding, then the fst projection from the pullback is an embedding.

Русский

Если g — вложение, то fst-проекция из предела является вложением.

LaTeX

$$$ \text{IsEmbedding}\big( \mathrm{pullback.fst} f g \big) $$$

Lean4

theorem fst_isEmbedding_of_right {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : IsEmbedding g) :
    IsEmbedding <| ⇑(pullback.fst f g) :=
  by
  convert
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isEmbedding.comp
      (pullback_map_isEmbedding (i₁ := 𝟙 X) f g f (𝟙 _) (homeoOfIso (Iso.refl _)).isEmbedding H (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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