exists_isClosedImmersion_locallyOfFinitePresentation_forall_factors_iff_of_fg_idealCut.lean

theorem finitePresentation_app_of_fg_cut {C H : Scheme.{u}} (ι : C ⟶ H) [IsClosedImmersion ι]
    (U : H.Opens) (hU : IsAffineOpen U) (J : Ideal Γ(H, U)) (hJ : J.FG)
    (hcut : ∀ (A : Type u) [CommRing A] (φ : Γ(H, U) →+* A),
      (∃ v : Spec (CommRingCat.of A) ⟶ C, v ≫ ι = Spec.map (CommRingCat.ofHom φ) ≫ hU.fromSpec) ↔
        Ideal.map φ J = ⊥) :
    (ι.app U).hom.FinitePresentation

theorem finitePresentation_map_of_isAffineOpen {C : Scheme.{u}} (V W : C.Opens)
    (hV : IsAffineOpen V) (hW : IsAffineOpen W) (e : V ≤ W) :
    (C.presheaf.map (homOfLE e).op).hom.FinitePresentation

theorem exists_isClosedImmersion_locallyOfFinitePresentation_forall_factors_iff_of_fg_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, J.FG ∧ ∀ (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 ι ∧ LocallyOfFinitePresentation ι ∧
      ∀ (A : Type u) [CommRing A] (u : Spec (CommRingCat.of A) ⟶ H),
        (∃ v : Spec (CommRingCat.of A) ⟶ C, v ≫ ι = u) ↔ Q A u