isPullback_opens_inf — Mathlib

English

For any opens U, V ⊆ X, the natural square built from X.homOfLE inf_le_left and X.homOfLE inf_le_right with U.ι, V.ι is a pullback.

Русский

Для любых открытых U, V ⊆ X, естественный квадрат, построенный из X.homOfLE inf_le_left и X.homOfLE inf_le_right с U.ι и V.ι, является пуллбеком.

LaTeX

$$$IsPullback\big(X.homOfLE inf_le_left, X.homOfLE inf_le_right, U.ι, V.ι\big).$$$

Lean4

theorem isPullback_opens_inf {X : Scheme} (U V : X.Opens) :
    IsPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right) U.ι V.ι :=
  (isPullback_morphismRestrict V.ι U).of_iso (V.ι.isoImage _ ≪≫ X.isoOfEq (V.functor_map_eq_inf U)) (Iso.refl _)
    (Iso.refl _) (Iso.refl _) (by simp [← cancel_mono U.ι]) (by simp [← cancel_mono V.ι]) (by simp) (by simp)

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