Theorems · Definition · algebraic geometry

AlgebraicGeometry.IsClosedImmersion.lift

{X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [AlgebraicGeometry.IsClosedImmersion f] →
        AlgebraicGeometry.Scheme.Hom.ker f ≤ AlgebraicGeometry.Scheme.Hom.ker g → (Y ⟶ X)

The universal property of closed immersions: For a closed immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose kernel contains the kernel of X in Z, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Cited by

5 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsClosedImmersion