# Intersections of radical ideals of commutative rings

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

Created on 2023-06-08.

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

Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.full-ideals-commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.intersections-ideals-commutative-rings
open import commutative-algebra.poset-of-ideals-commutative-rings
open import commutative-algebra.powers-of-elements-commutative-rings
open import commutative-algebra.products-ideals-commutative-rings

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

open import order-theory.greatest-lower-bounds-large-posets
open import order-theory.large-meet-semilattices


## Idea

The intersection of two radical ideals consists of the elements contained in both of them. Given two radical ideals I and J, their intersection can be computed as

  I ∩ J ＝ √ IJ,


where IJ is the product of I and J.

## Definition

### The universal property of intersections of radical ideals

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

{l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) → UUω
is-greatest-binary-lower-bound-Large-Poset
( I)
( J)
( K)


### The intersection of radical ideals

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

( intersection-ideal-Commutative-Ring A

intersection-ideal-Commutative-Ring A

ideal-Commutative-Ring (l2 ⊔ l3) A

is-intersection-intersection-ideal-Commutative-Ring A


### The large meet-semilattice of radical ideals in a commutative ring

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

meet-has-meets-Large-Poset
is-greatest-binary-lower-bound-meet-has-meets-Large-Poset

is-large-meet-semilattice-Large-Poset
has-meets-is-large-meet-semilattice-Large-Poset
has-top-element-is-large-meet-semilattice-Large-Poset

Large-Meet-Semilattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
large-poset-Large-Meet-Semilattice
is-large-meet-semilattice-Large-Meet-Semilattice


## Properties

### The radical ideal of an intersection is the intersection of the radicals of the ideals

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

leq-ideal-Commutative-Ring A
( intersection-ideal-Commutative-Ring A
( intersection-ideal-Commutative-Ring A I J))
forward-inclusion-intersection-radical-of-ideal-Commutative-Ring x (H , K) =
apply-universal-property-trunc-Prop H
( intersection-ideal-Commutative-Ring A I J)
( x))
( λ (n , H') →
apply-universal-property-trunc-Prop K
( intersection-ideal-Commutative-Ring A I J)
( x))
( λ (m , K') →
intro-exists
( ( is-closed-under-eq-ideal-Commutative-Ring A I
( is-closed-under-right-multiplication-ideal-Commutative-Ring
( A)
( I)
( power-Commutative-Ring A n x)
( power-Commutative-Ring A m x)
( H'))
( inv ( distributive-power-add-Commutative-Ring A n m))) ,
( is-closed-under-eq-ideal-Commutative-Ring A J
( is-closed-under-left-multiplication-ideal-Commutative-Ring
( A)
( J)
( power-Commutative-Ring A n x)
( power-Commutative-Ring A m x)
( K'))
( inv ( distributive-power-add-Commutative-Ring A n m))))))

leq-ideal-Commutative-Ring A
( intersection-ideal-Commutative-Ring A I J))
( intersection-ideal-Commutative-Ring A
apply-universal-property-trunc-Prop H
( subset-intersection-ideal-Commutative-Ring A
( x))
( λ (n , H' , K') →
( intro-exists n H' , intro-exists n K'))

( intersection-ideal-Commutative-Ring A
( intersection-ideal-Commutative-Ring A I J))
eq-has-same-elements-ideal-Commutative-Ring A
( intersection-ideal-Commutative-Ring A
( intersection-ideal-Commutative-Ring A I J))
( λ x →


### The intersection of radical ideals is the radical of the ideal generated by their product

Given two radical ideals I and J, we claim that

  I ∩ J ＝ √ IJ,


where IJ is the product of the ideals I and J. To prove this, it suffices to prove the inclusions

  IJ ⊆ I ∩ J ⊆ √ IJ.


Note that any product of elements in I and J is in the intersection I ∩ J. This settles the first inclusion. For the second inclusion, note that if x ∈ I ∩ J, then x² ∈ IJ so it follows that x ∈ √ IJ.

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

pr1 (contains-product-intersection-radical-ideal-Commutative-Ring x y p q) =
A I x y p
pr2 (contains-product-intersection-radical-ideal-Commutative-Ring x y p q) =
A J x y q

forward-inclusion-intersection-radical-ideal-Commutative-Ring x (H , K) =
( product-ideal-Commutative-Ring A
( x)
( 2)
( contains-product-product-radical-ideal-Commutative-Ring A I J x x H K)

( product-ideal-Commutative-Ring A
( is-product-product-ideal-Commutative-Ring A

is-product-intersection-radical-ideal-Commutative-Ring K H x p =
is-product-product-radical-ideal-Commutative-Ring A I J K H x

pr1 (is-intersection-product-radical-ideal-Commutative-Ring K) (L , M) x p =