English
For morphisms f: X → Y and an open U ⊆ Y, the pullback of f along U is isomorphic to the restricted X along f^{-1}(U).
Русский
Для отображения f: X → Y и открытого U ⊆ Y, произведение вытягивания по f вдоль U изоморфно ограничению X по f^{-1}(U).
LaTeX
$$pullback f U.ι ≅ f ⁻¹ᵁ U$$
Lean4
/-- Given a morphism `f : X ⟶ Y` and an open set `U ⊆ Y`, we have `X ×[Y] U ≅ X |_{f ⁻¹ U}` -/
def pullbackRestrictIsoRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) : pullback f (U.ι) ≅ f ⁻¹ᵁ U :=
by
refine IsOpenImmersion.isoOfRangeEq (pullback.fst f _) (Scheme.Opens.ι _) ?_
simp [IsOpenImmersion.range_pullback_fst_of_right]