Radical ideals generated by subsets of commutative rings

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

Created on 2023-06-08.
Last modified on 2023-06-08.

module
  commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings
  where
Imports 
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.ideals-generated-by-subsets-commutative-rings
open import commutative-algebra.radical-ideals-commutative-rings
open import commutative-algebra.radicals-of-ideals-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.subtypes
open import foundation.universe-levels

Idea

The radical ideal generated by a subset S of a commutative ring is the least radical ideal I containing S.

Definitions

The universal property of the radical ideal generated by a subset

module _
  {l1 l2 l3 : Level} (A : Commutative-Ring l1)
  (S : subset-Commutative-Ring l2 A)
  (I : radical-ideal-Commutative-Ring l3 A)
  (H : S ⊆ subset-radical-ideal-Commutative-Ring A I)
  where

  is-radical-ideal-generated-by-subset-Commutative-Ring :
    (l : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l)
  is-radical-ideal-generated-by-subset-Commutative-Ring l =
    (J : radical-ideal-Commutative-Ring l A) →
    S ⊆ subset-radical-ideal-Commutative-Ring A J →
    subset-radical-ideal-Commutative-Ring A I ⊆
    subset-radical-ideal-Commutative-Ring A J

The radical ideal generated by a subset

module _
  {l1 l2 : Level} (A : Commutative-Ring l1) (S : subset-Commutative-Ring l2 A)
  where

  radical-ideal-subset-Commutative-Ring :
    radical-ideal-Commutative-Ring (l1 ⊔ l2) A
  radical-ideal-subset-Commutative-Ring =
    radical-of-ideal-Commutative-Ring A (ideal-subset-Commutative-Ring A S)

  ideal-radical-ideal-subset-Commutative-Ring :
    ideal-Commutative-Ring (l1 ⊔ l2) A
  ideal-radical-ideal-subset-Commutative-Ring =
    ideal-radical-ideal-Commutative-Ring A radical-ideal-subset-Commutative-Ring

  subset-radical-ideal-subset-Commutative-Ring :
    subset-Commutative-Ring (l1 ⊔ l2) A
  subset-radical-ideal-subset-Commutative-Ring =
    subset-radical-ideal-Commutative-Ring A
      radical-ideal-subset-Commutative-Ring

  contains-subset-radical-ideal-subset-Commutative-Ring :
    S ⊆ subset-radical-ideal-subset-Commutative-Ring
  contains-subset-radical-ideal-subset-Commutative-Ring x p =
    contains-ideal-radical-of-ideal-Commutative-Ring A
      ( ideal-subset-Commutative-Ring A S)
      ( x)
      ( contains-subset-ideal-subset-Commutative-Ring A S x p)

  is-radical-ideal-generated-by-subset-radical-ideal-subset-Commutative-Ring :
    {l : Level} →
    is-radical-ideal-generated-by-subset-Commutative-Ring A S
      ( radical-ideal-subset-Commutative-Ring)
      ( contains-subset-radical-ideal-subset-Commutative-Ring)
      ( l)
  is-radical-ideal-generated-by-subset-radical-ideal-subset-Commutative-Ring
    K H =
    is-radical-of-ideal-radical-of-ideal-Commutative-Ring A
      ( ideal-subset-Commutative-Ring A S)
      ( K)
      ( is-ideal-generated-by-subset-ideal-subset-Commutative-Ring A S
        ( ideal-radical-ideal-Commutative-Ring A K)
        ( H))

Recent changes