Theorems · Definition · algebraic geometry

AlgebraicGeometry.morphismRestrictOpensRange

{X Y U : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (g : U ⟶ Y) →
      [inst : AlgebraicGeometry.IsOpenImmersion g] →
        CategoryTheory.Arrow.mk (f ∣_ AlgebraicGeometry.Scheme.Hom.opensRange g) ≅
          CategoryTheory.Arrow.mk (CategoryTheory.Limits.pullback.snd f g)

Restricting a morphism onto the image of an open immersion is isomorphic to the base change along the immersion.

Defined in

Mathlib.AlgebraicGeometry.Restrict

Cited by

7 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersion