English
If f is an embedding, then for any g the pullback.snd f g is an embedding.
Русский
Если f — вложение, то для любого g предел pullback.snd f g является вложением.
LaTeX
$$$ \text{IsEmbedding}\big( \mathrm{pullback.snd} f g \big) $$$
Lean4
/-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are open embeddings, and `S ⟶ T`
is mono, then the induced morphism `W ×ₛ X ⟶ Y ×ₜ Z` is also an open embedding.
```
W ⟶ Y
↘ ↘
S ⟶ T
↗ ↗
X ⟶ Z
```
-/
theorem pullback_map_isOpenEmbedding {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₁ : IsOpenEmbedding i₁) (H₂ : IsOpenEmbedding i₂) (i₃ : S ⟶ T) [H₃ : Mono i₃]
(eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) : IsOpenEmbedding (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) :=
by
constructor
· apply pullback_map_isEmbedding f₁ f₂ g₁ g₂ H₁.isEmbedding H₂.isEmbedding i₃ eq₁ eq₂
· rw [range_pullback_map]
apply IsOpen.inter <;> apply Continuous.isOpen_preimage
· apply ContinuousMap.continuous_toFun
· exact H₁.isOpen_range
· apply ContinuousMap.continuous_toFun
· exact H₂.isOpen_range
