Post #1894436

@iblech The Stacks Project's proof of Chevalley's theorem https://stacks.math.columbia.edu/tag/00FE looks very constructive, with the nontrivial input coming from https://stacks.math.columbia.edu/tag/00FB and https://stacks.math.columbia.edu/tag/00FD (I think here the determinants of classical invariant theory are entering), so this looks like a good starting point for a constructive and abstract/general elimination theory. (I just need to review the theory of sublocales and images of locale morphisms to check that my proposed definition makes sense.) The main theorem of elimination theory (X × P^n -> X maps closed sublocales (cut out by finitely many homogeneous equations) to closed sublocales) would be the other theorem I'd like to understand constructively.