isEmbedding_of_pullback — Mathlib

English

If f and g are embeddings, then the projection π to the pullback is an embedding.

Русский

Если f и g — вложения, то предельная проекция π предела является вложением.

LaTeX

$$$ \text{IsEmbedding}\big( \mathrm{limit.\,π}(\mathrm{cospan}\ f\ g)\ WalkingCospan.one \big) $$$

Lean4

theorem isEmbedding_of_pullback {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsEmbedding f) (H₂ : IsEmbedding g) :
    IsEmbedding (limit.π (cospan f g) WalkingCospan.one) :=
  by
  convert H₂.comp (snd_isEmbedding_of_left H₁ g)
  rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]
  rfl

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