Theorems · Definition · algebraic geometry

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom

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

If X ⟶ Y is an open immersion of PresheafedSpaces, and Y is a SheafedSpace, we can upgrade it into a morphism of SheafedSpaces.

Defined in: Mathlib.Geometry.RingedSpace.OpenImmersion
Cited by: 2 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category AlgebraicGeometry.PresheafedSpace.IsOpenImmersion

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement and proof · cited by 1,988
AlgebraicGeometry.PresheafedSpacestatement and proof · cited by 260
AlgebraicGeometry.SheafedSpacestatement and proof · cited by 142
AlgebraicGeometry.PresheafedSpace.IsOpenImmersionstatement and proof · cited by 44
CategoryTheory.InducedCategory.homMkproof · cited by 33
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpacestatement · cited by 5

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_basestatement · cited by 0
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_cstatement · cited by 0