Theorems · Definition · algebraic geometry

AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.SheafedSpace C} →
      (f : X ⟶ Y) →
        [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] →
          CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
            (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)

The functor Opens X ⥤ Opens Y associated with an open immersion f : X ⟶ Y.

Defined in

Mathlib.Geometry.RingedSpace.OpenImmersion

Cited by

13 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.SheafedSpace.IsOpenImmersion