isEmbedding_pullback_to_prod — Mathlib

English

If i1,i2 are embeddings and i3 is mono with compatibility eqs, then the induced pullback.map is an embedding.

Русский

Если i1,i2 — вложения, i3 — моно, и выполнены условия совместимости, то pullback.map является вложением.

LaTeX

$$$ \text{IsEmbedding}\left( \mathrm{pullback.map}(f_1,f_2,g_1,g_2,i_1,i_2,i_3,eq_1,eq_2) \right) $$$

Lean4

theorem isEmbedding_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) :
    IsEmbedding <| ⇑(prod.lift (pullback.fst f g) (pullback.snd f g)) :=
  ⟨isInducing_pullback_to_prod f g, (TopCat.mono_iff_injective _).mp inferInstance⟩

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