nLab anti-ideal predicate

Idea

In material set theory, an anti-ideal of a commutative ring $R$ with an apartness relation $\#$ is an $\#$-open subset $I \subseteq R$ which satisfies

• $\neg(0 \in I)$
• for all $x \in R$ and $y \in R$, $x + y \in I$ implies that $x \in I$ or $y \in I$
• for all $x \in R$ and $y \in R$, $x \in I$ and $y \in I$ implies that $x \cdot y \in I$

In dependently sorted set theory, where membership $x \in S$ is not a relation, the above statement that $x \in I$ for every element $x \in R$ in material set theory is equivalently a predicate in the logic $x \in R \vdash P_I(x)$. The given anti-ideal $I$ is then defined by restricted separation as the set $I \coloneqq \{x \in R \vert P_I(x)\}$, which in structural set theory automatically comes with an injection

$$i:\{x \in R \vert P_I(x)\} \hookrightarrow R$$

such that

$$\exists y \in \{x \in R \vert P_I(x)\}.x = i(y) \iff P(x)$$

Hence, the notion of anti-ideal predicate, a formulation of the notion of anti-ideal as a predicate rather than a subset.

Definition

Given a commutative ring $R$ with an apartness relation $\#$, an anti-ideal predicate on $R$ is an $\#$-open predicate $x \in R \vdash P_I(x)$ which satisfies

• $\neg P_I(0)$
• for all $x \in R$ and $y \in R$, $P_I(x + y)$ implies that $P_I(x)$ or $P_I(y)$
• for all $x \in R$ and $y \in R$, $P_I(x)$ and $P_I(y)$ implies that $P_I(x \cdot y)$

The anti-ideal $I$ is then defined by restricted separation as $I \coloneqq \{x \in R \vert P_I(x)\}$

Examples

The various definitions of anti-ideals translate over from material set theory to anti-ideal predicates in dependently sorted structural set theory by replacing $x \in I$ with $P_I(x)$ throughout the definition:

• A proper anti-ideal? predicate on a commutative ring $R$ with apartness relation $\#$ is an anti-ideal predicate $P_I$ where $P_I(1)$ is true.
• A anti-prime anti-ideal? predicate on a commutative ring $R$ with apartness relation $\#$ is a proper anti-ideal predicate $P_I$ where for all $x \in R$ and $y \in R$, $P_I(x)$ and $P_I(y)$ implies that $P_I(x \cdot y)$.
  $$\forall x \in R.\forall y \in R.P_I(x) \wedge P_I(y) \implies P_I(x \cdot y)$$
• A principal anti-ideal predicate on a commutative ring $R$ with apartness relation $\#$ anti-generated by an element $a \in R$ is an ideal predicate $P_I$ where for all $x \in R$ and for all $y \in R$, $P_I(x)$ implies that $x \# a \cdot y$.
  $$\forall x \in R.\forall y \in R.P_I(x) \implies x \# a \cdot y$$

See also

• anti-ideal
• predicate
• ideal predicate
• restricted separation
• antisubalgebra