Theorems · Definition · algebraic geometry

AlgebraicGeometry.pullbackRestrictIsoRestrict

{X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → (U : Y.Opens) → CategoryTheory.Limits.pullback f U.ι ≅ ↑((TopologicalSpace.Opens.map f.base).obj U)

Given a morphism f : X ⟶ Y and an open set U ⊆ Y, we have X ×[Y] U ≅ X |_{f ⁻¹ U}

Defined in

Mathlib.AlgebraicGeometry.Restrict

Cited by

10 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound