exists_isClosedImmersion_forall_factors_iff_of_idealCut.lean

theorem ideal_eq_of_forall_map_eq_bot_iff {B : Type u} [CommRing B] (J₁ J₂ : Ideal B)
    (h : ∀ (A : Type u) [CommRing A] (φ : B →+* A), Ideal.map φ J₁ = ⊥ ↔ Ideal.map φ J₂ = ⊥) : J₁ =
      J₂

theorem specMap_ofHom_comp {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] (φ : A →+* B) (χ
  : B →+* C) :
    Spec.map (CommRingCat.ofHom (χ.comp φ)) = Spec.map (CommRingCat.ofHom χ) ≫ Spec.map
      (CommRingCat.ofHom φ)

theorem _root_.AlgebraicGeometry.exists_isClosedImmersion_forall_factors_iff_of_idealCut
    (H : Scheme.{u})
    (Q : ∀ (A : Type u) [CommRing A], (Spec (CommRingCat.of A) ⟶ H) → Prop)
    (hQmap : ∀ (A A' : Type u) [CommRing A] [CommRing A'] (φ : A →+* A') (u : Spec (CommRingCat.of
      A) ⟶ H),
      Q A u → Q A' (Spec.map (CommRingCat.ofHom φ) ≫ u))
    (hQloc : ∀ (A : Type u) [CommRing A] (u : Spec (CommRingCat.of A) ⟶ H) (ι : Type u) (r : ι → A),
      Ideal.span (Set.range r) = ⊤ →
      (∀ i, Q (Localization.Away (r i))
        (Spec.map (CommRingCat.ofHom (algebraMap A (Localization.Away (r i)))) ≫ u)) → Q A u)
    (hQcut : ∀ (U : H.Opens) (_hU : IsAffineOpen U) (B : Type u) [CommRing B]
      (e : Spec (CommRingCat.of B) ≅ (U : Scheme.{u})),
      ∃ J : Ideal B, ∀ (A : Type u) [CommRing A] (φ : B →+* A),
        Q A (Spec.map (CommRingCat.ofHom φ) ≫ e.hom ≫ U.ι) ↔ Ideal.map φ J = ⊥) :
    ∃ (C : Scheme.{u}) (ι : C ⟶ H), IsClosedImmersion ι ∧
      ∀ (A : Type u) [CommRing A] (u : Spec (CommRingCat.of A) ⟶ H),
        (∃ v : Spec (CommRingCat.of A) ⟶ C, v ≫ ι = u) ↔ Q A u