Let $R$ be a ring and let $f:P\rightarrow P'$ be a surjective morphism of smooth $R$-algebras. Let $J$ be the kernel of this map. If $R$ is Noetherian, one can show that $J$ is locally generated by a regular sequence. I am looking for a reference where the non-noetherian case is studied: I don't expect the existence of a regular sequence as they do not necessarily behave well in the non-Noetherian case but I am especially looking for a reference of the following result:


In the situation above with $R$ not necessarily Noetherian, $J$ can locally be generated by a Koszul-regular sequence, in the sense that there exists a sequence $(x\_1,...,x\_r)$ generating $J$ such that the homology of the corresponding Koszul complex is $0$ for $i\geq 1$. Bourbaki also calls these sequences completely secant sequences. I find that I am either not proficient at looking up references on such sequences or the literature is quite scarce. Here is a list of references where Koszul-regular sequences appear and I did not find the result in: Bourbaki (I think 10-Algebra), stacks-project, "Completion, Cech and Local Homology and Cohomology" by P. Schenzel and A. Marie-Simon



Koszul -regular sequences (reference request)
In the stacks project this can be found as [Tag 067U](https://stacks.math.columbia.edu/tag/067U) stated in the language of schemes.


