Nilpotent elements in rings

module ring-theory.nilpotent-elements-rings where

Imports

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.universe-levels

open import ring-theory.nilpotent-elements-semirings
open import ring-theory.powers-of-elements-rings
open import ring-theory.rings
open import ring-theory.subsets-rings

Idea

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

Definition

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

  is-nilpotent-element-ring-Prop : type-Ring R → Prop l
  is-nilpotent-element-ring-Prop =
    is-nilpotent-element-semiring-Prop (semiring-Ring R)

  is-nilpotent-element-Ring : type-Ring R → UU l
  is-nilpotent-element-Ring = is-nilpotent-element-Semiring (semiring-Ring R)

  is-prop-is-nilpotent-element-Ring :
    (x : type-Ring R) → is-prop (is-nilpotent-element-Ring x)
  is-prop-is-nilpotent-element-Ring =
    is-prop-is-nilpotent-element-Semiring (semiring-Ring R)

Properties

Zero is nilpotent

is-nilpotent-zero-Ring :
  {l : Level} (R : Ring l) → is-nilpotent-element-Ring R (zero-Ring R)
is-nilpotent-zero-Ring R = is-nilpotent-zero-Semiring (semiring-Ring R)

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

is-nilpotent-add-Ring :
  {l : Level} (R : Ring l) →
  (x y : type-Ring R) → (mul-Ring R x y ＝ mul-Ring R y x) →
  is-nilpotent-element-Ring R x → is-nilpotent-element-Ring R y →
  is-nilpotent-element-Ring R (add-Ring R x y)
is-nilpotent-add-Ring R = is-nilpotent-add-Semiring (semiring-Ring R)

If `x` is nilpotent, then so is `-x`

is-nilpotent-element-neg-Ring :
  {l : Level} (R : Ring l) →
  is-closed-under-negatives-subset-Ring R (is-nilpotent-element-ring-Prop R)
is-nilpotent-element-neg-Ring R x H =
  apply-universal-property-trunc-Prop H
    ( is-nilpotent-element-ring-Prop R (neg-Ring R x))
    ( λ (n , p) →
      intro-∃ n
        ( ( power-neg-Ring R n x) ∙
          ( ( ap (mul-Ring R (power-Ring R n (neg-one-Ring R))) p) ∙
            ( right-zero-law-mul-Ring R (power-Ring R n (neg-one-Ring R))))))

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

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

  is-nilpotent-element-mul-Ring :
    (x y : type-Ring R) →
    mul-Ring R x y ＝ mul-Ring R y x →
    is-nilpotent-element-Ring R x →
    is-nilpotent-element-Ring R (mul-Ring R x y)
  is-nilpotent-element-mul-Ring =
    is-nilpotent-element-mul-Semiring (semiring-Ring R)

  is-nilpotent-element-mul-Ring' :
    (x y : type-Ring R) →
    mul-Ring R x y ＝ mul-Ring R y x →
    is-nilpotent-element-Ring R x →
    is-nilpotent-element-Ring R (mul-Ring R y x)
  is-nilpotent-element-mul-Ring' =
    is-nilpotent-element-mul-Semiring' (semiring-Ring R)