isPullback_opens_inf_le — Mathlib

English

Given two Opens U, V ⊆ X with U ≤ W and V ≤ W for some W, the induced square from the maps X.homOfLE inf_le_left, X.homOfLE inf_le_right, X.homOfLE hU, X.homOfLE hV is a pullback.

Русский

Если имеем две открытости U, V ⊆ X, с U ≤ W, V ≤ W для некоторого W, то соответствующий квадрат диаграмм является пуллбеком.

LaTeX

$$$IsPullback\big(X.homOfLE inf_le_left, X.homOfLE inf_le_right, X.homOfLE hU, X.homOfLE hV\big).$$$

Lean4

theorem isPullback_opens_inf_le {X : Scheme} {U V W : X.Opens} (hU : U ≤ W) (hV : V ≤ W) :
    IsPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right) (X.homOfLE hU) (X.homOfLE hV) :=
  by
  refine
    (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫ X.isoOfEq ?_)
      (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
  · rw [← TopologicalSpace.Opens.map_comp_obj, ← Scheme.comp_base, Scheme.homOfLE_ι]
    exact V.functor_map_eq_inf U
  · exact (W.functor_map_eq_inf U).trans (by simpa)
  all_goals { simp [← cancel_mono (Scheme.Opens.ι _)]
  }

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