isPullback_morphismRestrict — Mathlib

English

The restriction morphism f|_U forms a pullback square with the corresponding inverse image restriction.

Русский

Ограничение морфизма f|_U образует квадрат-подтягивание вместе с соответствующим ограничением обратного образа.

LaTeX

$$$\text{IsPullback }(f|_U, f^{-1}U).\iota, U.\iota, f$$$

Lean4

theorem isPullback_morphismRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f := by
  delta morphismRestrict
  rw [← Category.id_comp f]
  refine
    (IsPullback.of_horiz_isIso ⟨?_⟩).paste_horiz (IsPullback.of_hasPullback f (Y.ofRestrict U.isOpenEmbedding)).flip
  erw [pullbackRestrictIsoRestrict_inv_fst]
  rw [Category.comp_id]

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