{X : AlgebraicGeometry.Scheme} →
  {A : CommRingCat} →
    (f : X.Hom (AlgebraicGeometry.Spec A)) →
      (I : Ideal ↑A) →
        I ≤
            RingHom.ker
              (CommRingCat.Hom.hom
                (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop)) →
          (X ⟶ AlgebraicGeometry.Spec { carrier := ↑A ⧸ I, commRing := Ideal.Quotient.commRing I })