# Nilradical of a commutative ring

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Maša Žaucer and maybemabeline.

Created on 2022-10-04.

module commutative-algebra.nilradical-commutative-rings where

Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.prime-ideals-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import ring-theory.nilpotent-elements-rings


## Idea

The nilradical of a commutative ring is the ideal consisting of all nilpotent elements.

## Definitions

subset-nilradical-Commutative-Ring :
{l : Level} (A : Commutative-Ring l) → subset-Commutative-Ring l A
is-nilpotent-element-ring-Prop (ring-Commutative-Ring A)


## Properties

contains-zero-nilradical-Commutative-Ring :
{l : Level} (A : Commutative-Ring l) →
contains-zero-subset-Commutative-Ring A
contains-zero-nilradical-Commutative-Ring A = intro-exists 1 refl


is-closed-under-addition-nilradical-Commutative-Ring :
{l : Level} (A : Commutative-Ring l) →
( ring-Commutative-Ring A)
( x)
( y)
( commutative-mul-Commutative-Ring A x y)


### The nilradical is closed under negatives

is-closed-under-negatives-nilradical-Commutative-Ring :
{l : Level} (A : Commutative-Ring l) →
is-closed-under-negatives-subset-Commutative-Ring A
is-nilpotent-element-neg-Ring (ring-Commutative-Ring A) x


### The nilradical is closed under multiplication with ring elements

module _
{l : Level} (A : Commutative-Ring l)
where

is-closed-under-right-multiplication-subset-Commutative-Ring A
is-nilpotent-element-mul-Ring
( ring-Commutative-Ring A)
( x)
( y)
( commutative-mul-Commutative-Ring A x y)

is-closed-under-left-multiplication-subset-Commutative-Ring A
is-nilpotent-element-mul-Ring'
( ring-Commutative-Ring A)
( y)
( x)
( commutative-mul-Commutative-Ring A y x)


nilradical-Commutative-Ring :
{l : Level} (A : Commutative-Ring l) → ideal-Commutative-Ring l A
ideal-right-ideal-Commutative-Ring A


is-in-nilradical-Commutative-Ring :
{l : Level} (R : Commutative-Ring l) → type-Commutative-Ring R → UU l

{l : Level} (R : Commutative-Ring l)
(I : radical-ideal-Commutative-Ring l R) (x : type-Commutative-Ring R) →
apply-universal-property-trunc-Prop p


### The nilradical is contained in every prime ideal

is-contained-in-prime-ideal-nilradical-Commutative-Ring :
{l : Level} (R : Commutative-Ring l)
(P : prime-ideal-Commutative-Ring l R) (x : type-Commutative-Ring R) →