Post #1894435

2026-04-28 14:04 UTC

@iblech I can parse the statement of the conjecture, but it looks quite technical to me. Since you mention it in the context of elimination theory, can it be reformulated in the form »there is a constructive proof that the morphism of locales induced by some morphism of affine/projective schemes has closed/constructible/… image«? (I would propose to call a sublocale of Spec(R) constructible if it lies in the Boolean algebra generated by the complemented sublocales V(f) for f in R.)

Replies (1)

@jdw@mathstodon.xyz 2026-04-28 15:07

@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.

Open ##1894436