Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  [P.RespectsRight AlgebraicGeometry.IsOpenImmersion],
  P f ↔
    ∀ (x : ↥X),
      ∃ U V,
        ∃ (_ : x ∈ V.carrier) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          P (AlgebraicGeometry.Scheme.Hom.resLE f U V e)

If P is local at the source, local at the target and is stable under post-composition with open immersions, then P can be checked locally around points.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsZariskiLocalAtSourceAlgebraicGeometry.IsZariskiLocalAtTargetCategoryTheory.MorphismProperty.RespectsRight