[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## Mathematical structures Move on from ideals, we should study anti-ideals. Move on from set rings, we should study apartness rings. Most relevant rings have apartness structure on them, such as the integers, the rational numbers, and the real numbers. Instead of saying anti-ideal, we should say anti-ideal predicate, and use separation or the dependent sum type: An anti-ideal predicate in an apartness ring $R$ is an $\#$-open predicate $x:R \vdash P(x)$ such that * $P(0)$ implies $\bot$ * $P(a + b)$ implies that $P(a)$ or $P(b)$ * $P(a \cdot b)$ implies that $P(a)$ and $P(b)$ An anti-ideal predicate in an apartness ring $R$ is an $\#$-open predicate $x:R \vdash P(x)$ such that * $P(a)$ implies $a \# 0$ * $P(a + b)$ implies that $P(a)$ or $P(b)$ * $P(a \cdot b)$ implies that $P(a)$ and $P(b)$ ... The reason why for the study of anti-ideals is because of the existence of local rings and ordered local rings means that one has apartness independent of equality. An apartness set $S$ is discrete if $a \in S, b \in S \vdash (a = b) \vee (a \# b)$ An anti-ideal in an apartness ring $R$ is an $\#$-open subset $A \subseteq R$ such that * $a \in A$ implies $a \# 0$ * $a + b \in A$ implies that $a \in A$ or $b \in A$ * $a \cdot b \in A$ implies that $a \in A$ and $b \in A$ A ring is local if the set of invertible elements forms an anti-ideal. A ring is a field if it is a discrete local ring. category: redirected to nlab