Theorems · Definition · algebraic geometry

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Z) →
        [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
          (g : Y ⟶ Z) →
            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

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.PresheafedSpace.IsOpenImmersion