# Products of radical ideals of a commutative ring

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

Created on 2023-06-08.

module commutative-algebra.products-radical-ideals-commutative-rings where

Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.powers-of-elements-commutative-rings
open import commutative-algebra.products-ideals-commutative-rings
open import commutative-algebra.subsets-commutative-rings

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


## Idea

The product of two radical ideals I and J is the radical of the product of I and J. In other words, the product of two radical ideals I and J is the least radical ideal that contains the products of elements in I and in J.

## Definitions

### The universal property of the product of two radical ideals in a commutative ring

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

{l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) →
UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
contains-product-ideal-Commutative-Ring A

{l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) →
{l5 : Level} (L : radical-ideal-Commutative-Ring l5 A) →


### The product of two radical ideals in a commutative ring

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

subset-Commutative-Ring (l1 ⊔ l2 ⊔ l3) A
generating-subset-product-ideal-Commutative-Ring A

radical-ideal-Commutative-Ring (l1 ⊔ l2 ⊔ l3) A
( product-ideal-Commutative-Ring A

ideal-Commutative-Ring (l1 ⊔ l2 ⊔ l3) A

type-Commutative-Ring A → UU (l1 ⊔ l2 ⊔ l3)

contains-product-product-radical-ideal-Commutative-Ring x y H K =
( product-ideal-Commutative-Ring A
( mul-Commutative-Ring A x y)
( contains-product-product-ideal-Commutative-Ring A
( x)
( y)
( H)
( K))

( product-ideal-Commutative-Ring A
( K)
( is-product-product-ideal-Commutative-Ring A
( H))


## Properties

### Radical laws for products of ideals

#### √ (I · √ J) ＝ √ IJ

For the forward inclusion, assume that x ∈ I and y ∈ √ J. Then there exists an n such that yⁿ ∈ J. It follows that

  (xy)ⁿ⁺¹ ＝ xⁿ⁺¹yⁿ⁺¹ = (xxⁿ)(yⁿy) ＝ (xyⁿ)(xⁿy) ∈ IJ,


and hence xy ∈ √ IJ. The backwards inclusion is clear, since J ⊆ √ J.

module _
{l1 l2 l3 : Level} (A : Commutative-Ring l1)
(J : ideal-Commutative-Ring l3 A)
where

( I)
( product-ideal-Commutative-Ring A
( J)))
( product-ideal-Commutative-Ring A
( J)))
( λ x y H K →
apply-universal-property-trunc-Prop K
( product-ideal-Commutative-Ring A
( J))
( mul-Commutative-Ring A x y))
( λ (n , p) →
intro-exists
( succ-ℕ n)
( is-closed-under-eq-ideal-Commutative-Ring' A
( product-ideal-Commutative-Ring A
( J))
( is-closed-under-right-multiplication-ideal-Commutative-Ring A
( product-ideal-Commutative-Ring A
( J))
( mul-Commutative-Ring A x (power-Commutative-Ring A n y))
( mul-Commutative-Ring A (power-Commutative-Ring A n x) y)
( contains-product-product-ideal-Commutative-Ring A
( J)
( x)
( power-Commutative-Ring A n y)
( H)
( p)))
( ( distributive-power-mul-Commutative-Ring A (succ-ℕ n) x y) ∙
( ( ap-mul-Commutative-Ring A
( power-succ-Commutative-Ring' A n x)
( power-succ-Commutative-Ring A n y)) ∙
( interchange-mul-mul-Commutative-Ring A x
( power-Commutative-Ring A n x)
( power-Commutative-Ring A n y)
( y)))))))

( product-ideal-Commutative-Ring A
( J)))
( I)
( product-ideal-Commutative-Ring A
( J))
( I)
( is-product-product-ideal-Commutative-Ring A
( J)
( λ x y p q →
( product-ideal-Commutative-Ring A
( mul-Commutative-Ring A x y)
( contains-product-product-ideal-Commutative-Ring A
( x)
( y)
( p)
( contains-ideal-radical-of-ideal-Commutative-Ring A J y q))))

( I)
( product-ideal-Commutative-Ring A
( J))