Quasi-coherent ideal sheaves

Stream: mathlib4

[Andrew Yang]

Here is a definition of a quasi-coherent ideal sheaves and I was able to show that they are in bijection with closed subschemes and define scheme theoretic images etc. (i.e. an family of ideals of $\Gamma(X, U)$ such that $I(D(f)) = I(U)_f$)

structure IdealSheafData (X : Scheme.{u}) : Type u where
  ideal : ∀ U : X.affineOpens, Ideal Γ(X, U)
  map_ideal_basicOpen : ∀ (U : X.affineOpens) (f : Γ(X, U)),
    (ideal U).map (X.presheaf.map (homOfLE <| X.basicOpen_le f).op).hom =
      ideal (X.affineBasicOpen f)

The question is: do we want this in mathlib? Of course the right thing to do is define quasi-coherent sub-$\mathcal{O}_X$ modules and quotients etc but I think this definition useful to have as an API to construct ideal sheaves (when we eventually have them) anyways so it is fine to add them for now and refactor later.
What do people think?

[Andrew Yang]

cc @Joël Riou @Christian Merten

[Joël Riou]

I am very much ok with this. If this has to be dissolved in a more general API later, we shall refactor it in due time.