pullback_map_isOpenImmersion — Mathlib

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

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