English
If the maps i1, i2 are open immersions and i3 is mono, then the pullback.map is an open immersion.
Русский
Если i1, i2 — открытые вложения, а i3 — моно, то отображение пулбэка является открытым вложением.
LaTeX
$$$$ \text{IsOpenImmersion}(\text{pullback.map } f g f' g' i1 i2 i3 e1 e2) $$$$
Lean4
instance pullback_map_isOpenImmersion {X Y S X' Y' S' : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S')
(i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [IsOpenImmersion i₁]
[IsOpenImmersion i₂] [Mono i₃] : IsOpenImmersion (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) :=
by
rw [pullback_map_eq_pullbackFstFstIso_inv]
infer_instance