The nilradical of a commutative semiring

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
subset-nilradical-Commutative-Semiring A =
  is-nilpotent-element-semiring-Prop (semiring-Commutative-Semiring A)

Properties

The nilradical contains zero

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

The nilradical is closed under addition

is-closed-under-add-nilradical-Commutative-Semiring :
  {l : Level} (A : Commutative-Semiring l) →
  is-closed-under-addition-subset-Commutative-Semiring A
    ( subset-nilradical-Commutative-Semiring A)
is-closed-under-add-nilradical-Commutative-Semiring A x y =
  is-nilpotent-add-Semiring
    ( 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-mul-right-nilradical-Commutative-Semiring :
    is-closed-under-right-multiplication-subset-Commutative-Semiring A
      ( subset-nilradical-Commutative-Semiring A)
  is-closed-under-mul-right-nilradical-Commutative-Semiring x y =
    is-nilpotent-element-mul-Semiring
      ( semiring-Commutative-Semiring A)
      ( x)
      ( y)
      ( commutative-mul-Commutative-Semiring A x y)

  is-closed-under-mul-left-nilradical-Commutative-Semiring :
    is-closed-under-left-multiplication-subset-Commutative-Semiring A
      ( subset-nilradical-Commutative-Semiring A)
  is-closed-under-mul-left-nilradical-Commutative-Semiring x y =
    is-nilpotent-element-mul-Semiring'
      ( semiring-Commutative-Semiring A)
      ( y)
      ( x)
      ( commutative-mul-Commutative-Semiring A y x)