Prove weak Nullstellensatz

[MatthiasHu]

We often use synthetic quasicoherence in the special case where Spec A is empty and we want to conclude that A is trivial. This special case can be formulated without referring to finitely presented algebras (only to polynomial algebras): if a family of polynomials in n variables has no common roots, then 1 is an element of the generated ideal. One can call this "weak Hilbert Nullstellensatz".

I think it would be useful to have this statement explicitly and use it to prove the other things. The case n = 0 (zero polynomial variables) is then almost exactly our generalized field property (except that one has to translate back and forth between k and k[].)