Theorems · Definition · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift

{X Y Z : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] →
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆
            Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) →
          (Y ⟶ X)

The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

Defined in

Mathlib.Geometry.RingedSpace.OpenImmersion

Cited by

7 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion