∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {R : Type u}
  [inst : CommRing R] {f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)},
  AlgebraicGeometry.geometrically P f ↔
    ∀ ⦃K : Type u⦄ [inst_1 : Field K] [inst_2 : Algebra R K] ⦃Y : AlgebraicGeometry.Scheme⦄ (fst : Y ⟶ X)
      (snd : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)),
      CategoryTheory.IsPullback fst snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) → P Y