nLab ideal predicate

Idea

In material set theory, an ideal of a commutative ring $R$ is a subset $I \subseteq R$ which satisfies

• $0 \in I$
• for all $x \in R$ and $y \in R$, $x \in I$ and $y \in I$ implies that $x + y \in I$
• for all $x \in R$ and $y \in R$, $x \cdot y \in I$ implies that $x \in I$ or $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 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 ideal predicate, a formulation of the notion of ideal as a predicate rather than a subset.

Definition

Given a commutative ring $R$, an ideal predicate on $R$ is a predicate $x \in R \vdash P_I(x)$ which satisfies

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

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

Examples

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

• A proper ideal predicate on a commutative ring $R$ is an ideal predicate $P_I$ where $P_I(1)$ is false.

• A maximal ideal predicate on a commutative ring $R$ is an ideal predicate $P_I$ where for all $x \in R$, $P_I(x)$ being false implies that $x$ is an invertible element.

  $$\forall x \in R.(\neg P_I(x)) \implies \exists y \in R.x \cdot y = 1$$

• A prime ideal predicate on a commutative ring $R$ is a proper ideal predicate $P_I$ where for all $x \in R$ and $y \in R$, $P_I(x \cdot y)$ implies that $P_I(x)$ or $P_I(y)$.

  $$\forall x \in R.\forall y \in R.P_I(x \cdot y) \implies P_I(x) \vee P_I(y)$$

• A principal ideal predicate on a commutative ring $R$ generated by an element $a \in R$ is an ideal predicate $P_I$ where for all $x \in R$, $P_I(a \cdot x)$.

 See also

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