English
If W ⟶ Y and X ⟶ Z are embeddings in a pullback diagram, then the induced map W ×_S X ⟶ Y ×_T Z is an embedding.
Русский
Если в диаграмме Пуллбэков стрелы W ⟶ Y и X ⟶ Z являются вложениями, то индуцированное отображение W ×_S X ⟶ Y ×_T Z также является вложением.
LaTeX
$$$\\text{IsEmbedding}(\\text{pullback.map} \\; f_1 \\; f_2 \\; g_1 \\; g_2 \\; i_1 \\; i_2 \\; e)$$$
Lean4
/-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are embeddings,
then the induced morphism `W ×ₛ X ⟶ Y ×ₜ Z` is also an embedding.
```
W ⟶ Y
↘ ↘
S ⟶ T
↗ ↗
X ⟶ Z
```
-/
theorem pullback_map_isEmbedding {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T)
{i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : IsEmbedding i₁) (H₂ : IsEmbedding i₂) (i₃ : S ⟶ T) (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁)
(eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) : IsEmbedding (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :=
by
refine
.of_comp (ContinuousMap.continuous_toFun _)
(show Continuous (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) from ContinuousMap.continuous_toFun _) ?_
suffices IsEmbedding (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ Limits.prod.map i₁ i₂) by
simpa [← coe_comp] using this
rw [coe_comp]
exact (isEmbedding_prodMap H₁ H₂).comp (isEmbedding_pullback_to_prod _ _)
