Generalized spaces for constructive algebra
arXiv:2012.13850
Abstract
The purpose of this contribution is to give a coherent account of a particular narrative which links locales, geometric theories, sheaf semantics and constructive commutative algebra. We are hoping to convey a firm grasp of three ideas: (1) Locales are a kind of space in which opens instead of points are fundamental. (2) Sheaf semantics allows us to explore mathematical objects from custom-tailored mathematical universes. (3) Without loss of generality, any reduced ring is a field.
Chapter for an upcoming collection "Proof and Computation" (proceedings of the Herrsching 2020 workshop)