= Coherent theory of local rings
Use the signature of unital <commutative rings>, its equational axioms, and the <coherent sequents> $0=1\vdash\bot$ and $\top\vdash_x\operatorname{Inv}(x)\vee\operatorname{Inv}(1-x)$, where $\operatorname{Inv}(x)$ abbreviates $\exists y\,(xy=1)$. In a set-based model the nonunits form its unique <maximal ideal>; this is the usual nonzero <local ring>. In a <topos> the disjunction expresses local existence of a unit witness. Its <classifying topos> is defined by the <Zariski coverage on finitely presented rings>.
Back to article page
