pullbackRestrictIsoRestrict — Mathlib

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]

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