Nilpotent elements in semirings

module ring-theory.nilpotent-elements-semirings where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

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

open import ring-theory.binomial-theorem-semirings
open import ring-theory.powers-of-elements-semirings
open import ring-theory.semirings

Idea

A nilpotent element in a semiring is an element x for which there is a natural number n such that x^n = 0.

Definition

is-nilpotent-element-semiring-Prop :
  {l : Level} (R : Semiring l)  type-Semiring R  Prop l
is-nilpotent-element-semiring-Prop R x =
  ∃-Prop   n  power-Semiring R n x  zero-Semiring R)

is-nilpotent-element-Semiring :
  {l : Level} (R : Semiring l)  type-Semiring R  UU l
is-nilpotent-element-Semiring R x =
  type-Prop (is-nilpotent-element-semiring-Prop R x)

is-prop-is-nilpotent-element-Semiring :
  {l : Level} (R : Semiring l) (x : type-Semiring R) 
  is-prop (is-nilpotent-element-Semiring R x)
is-prop-is-nilpotent-element-Semiring R x =
  is-prop-type-Prop (is-nilpotent-element-semiring-Prop R x)

Properties

Zero is nilpotent

is-nilpotent-zero-Semiring :
  {l : Level} (R : Semiring l) 
  is-nilpotent-element-Semiring R (zero-Semiring R)
is-nilpotent-zero-Semiring R = intro-∃ 1 refl

If x and y commute and are both nilpotent, then x + y is nilpotent

is-nilpotent-add-Semiring :
  {l : Level} (R : Semiring l) 
  (x y : type-Semiring R)  (mul-Semiring R x y  mul-Semiring R y x) 
  is-nilpotent-element-Semiring R x  is-nilpotent-element-Semiring R y 
  is-nilpotent-element-Semiring R (add-Semiring R x y)
is-nilpotent-add-Semiring R x y H f h =
  apply-universal-property-trunc-Prop f
    ( is-nilpotent-element-semiring-Prop R (add-Semiring R x y))
    ( λ (n , p) 
      apply-universal-property-trunc-Prop h
        ( is-nilpotent-element-semiring-Prop R (add-Semiring R x y))
        ( λ (m , q) 
          intro-∃
            ( n +ℕ m)
            ( ( is-linear-combination-power-add-Semiring R n m x y H) 
              ( ( ap-add-Semiring R
                  ( ( ap (mul-Semiring' R _) q) 
                    ( left-zero-law-mul-Semiring R _))
                  ( ( ap (mul-Semiring' R _) p) 
                    ( left-zero-law-mul-Semiring R _))) 
                ( left-unit-law-add-Semiring R (zero-Semiring R))))))

If x is nilpotent and y commutes with x, then xy is also nilpotent

module _
  {l : Level} (R : Semiring l)
  where

  is-nilpotent-element-mul-Semiring :
    (x y : type-Semiring R) 
    mul-Semiring R x y  mul-Semiring R y x 
    is-nilpotent-element-Semiring R x 
    is-nilpotent-element-Semiring R (mul-Semiring R x y)
  is-nilpotent-element-mul-Semiring x y H f =
    apply-universal-property-trunc-Prop f
      ( is-nilpotent-element-semiring-Prop R (mul-Semiring R x y))
      ( λ (n , p) 
        intro-∃ n
          ( ( distributive-power-mul-Semiring R n H) 
            ( ( ap (mul-Semiring' R (power-Semiring R n y)) p) 
              ( left-zero-law-mul-Semiring R
                ( power-Semiring R n y)))))

  is-nilpotent-element-mul-Semiring' :
    (x y : type-Semiring R) 
    mul-Semiring R x y  mul-Semiring R y x 
    is-nilpotent-element-Semiring R x 
    is-nilpotent-element-Semiring R (mul-Semiring R y x)
  is-nilpotent-element-mul-Semiring' x y H f =
    is-closed-under-eq-subtype
      ( is-nilpotent-element-semiring-Prop R)
      ( is-nilpotent-element-mul-Semiring x y H f)
      ( H)