Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isPullback_of_isClosedImmersion

∀ {ZX ZY X Y : AlgebraicGeometry.Scheme} (iX : ZX ⟶ X) (iY : ZY ⟶ Y) (Zf : ZX ⟶ ZY) (f : X ⟶ Y)
  [AlgebraicGeometry.IsClosedImmersion iX] [AlgebraicGeometry.IsClosedImmersion iY],
  CategoryTheory.CategoryStruct.comp iX f = CategoryTheory.CategoryStruct.comp Zf iY →
    (AlgebraicGeometry.Scheme.Hom.ker iY).comap f = AlgebraicGeometry.Scheme.Hom.ker iX →
      CategoryTheory.IsPullback iX Zf f iY

To show that the pullback of the closed immersion iX along f is the closed immersion iY, it suffices to check that the preimage of ker iY under f is ker iX.

Defined in

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsClosedImmersionAlgebraicGeometry.IsClosedImmersion