Theorems · Theorem · algebraic geometry

AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms

∀ {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  [P.IsClosedUnderIsomorphisms],
  AlgebraicGeometry.geometrically P f ↔
    ∀ (K : Type u) [inst : Field K] (y : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Y),
      P (CategoryTheory.Limits.pullback f y)

Defined in

Mathlib.AlgebraicGeometry.Geometrically.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms