# Radical ideals generated by subsets of commutative rings

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

Created on 2023-06-08.

module
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.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)
(H : S ⊆ subset-radical-ideal-Commutative-Ring A I)
where

(l : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l)
(J : radical-ideal-Commutative-Ring l A) →
S ⊆ 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

ideal-Commutative-Ring (l1 ⊔ l2) A

subset-Commutative-Ring (l1 ⊔ l2) A

( ideal-subset-Commutative-Ring A S)
( x)
( contains-subset-ideal-subset-Commutative-Ring A S x p)

{l : Level} →