The nilradical of a commutative semiring

Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.

Created on 2023-03-18.

module commutative-algebra.nilradicals-commutative-semirings where

Imports
open import commutative-algebra.commutative-semirings
open import commutative-algebra.subsets-commutative-semirings

open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.universe-levels

open import ring-theory.nilpotent-elements-semirings


Idea

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

Definitions

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


Properties

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


is-closed-under-add-nilradical-Commutative-Semiring :
{l : Level} (A : Commutative-Semiring l) →
( semiring-Commutative-Semiring A)
( x)
( y)
( commutative-mul-Commutative-Semiring A x y)


The nilradical is closed under multiplication with ring elements

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

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