Nil ideals

module ring-theory.nil-ideals-rings where

open import foundation.propositions
open import foundation.universe-levels

open import ring-theory.ideals-rings
open import ring-theory.nilpotent-elements-rings
open import ring-theory.rings

Idea

A nil ideal in a ring is an ideal in which every element is nilpotent

Definition

Nil left ideals

module _
  {l1 l2 : Level} (R : Ring l1) (I : left-ideal-Ring l2 R)
  where

  is-nil-left-ideal-ring-Prop : Prop (l1 ⊔ l2)
  is-nil-left-ideal-ring-Prop =
    Π-Prop
      ( type-left-ideal-Ring R I)
      ( λ x →
        is-nilpotent-element-ring-Prop R (inclusion-left-ideal-Ring R I x))

  is-nil-left-ideal-Ring : UU (l1 ⊔ l2)
  is-nil-left-ideal-Ring = type-Prop is-nil-left-ideal-ring-Prop

  is-prop-is-nil-left-ideal-Ring : is-prop is-nil-left-ideal-Ring
  is-prop-is-nil-left-ideal-Ring =
    is-prop-type-Prop is-nil-left-ideal-ring-Prop

Nil right ideals

module _
  {l1 l2 : Level} (R : Ring l1) (I : right-ideal-Ring l2 R)
  where

  is-nil-right-ideal-ring-Prop : Prop (l1 ⊔ l2)
  is-nil-right-ideal-ring-Prop =
    Π-Prop
      ( type-right-ideal-Ring R I)
      ( λ x →
        is-nilpotent-element-ring-Prop R (inclusion-right-ideal-Ring R I x))

  is-nil-right-ideal-Ring : UU (l1 ⊔ l2)
  is-nil-right-ideal-Ring = type-Prop is-nil-right-ideal-ring-Prop

  is-prop-is-nil-right-ideal-Ring : is-prop is-nil-right-ideal-Ring
  is-prop-is-nil-right-ideal-Ring =
    is-prop-type-Prop is-nil-right-ideal-ring-Prop

Nil ideals

module _
  {l1 l2 : Level} (R : Ring l1) (I : ideal-Ring l2 R)
  where

  is-nil-ideal-ring-Prop : Prop (l1 ⊔ l2)
  is-nil-ideal-ring-Prop =
    Π-Prop
      ( type-ideal-Ring R I)
      ( λ x →
        is-nilpotent-element-ring-Prop R (inclusion-ideal-Ring R I x))

  is-nil-ideal-Ring : UU (l1 ⊔ l2)
  is-nil-ideal-Ring = type-Prop is-nil-ideal-ring-Prop

  is-prop-is-nil-ideal-Ring : is-prop is-nil-ideal-Ring
  is-prop-is-nil-ideal-Ring =
    is-prop-type-Prop is-nil-ideal-ring-Prop