# Products of ideals of rings

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

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

module ring-theory.products-ideals-rings where

Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import ring-theory.ideals-generated-by-subsets-rings
open import ring-theory.ideals-rings
open import ring-theory.poset-of-ideals-rings
open import ring-theory.products-subsets-rings
open import ring-theory.rings
open import ring-theory.subsets-rings


## Idea

The product of two ideals I and J in a ring is the ideal generated by all products of elements in I and J.

## Definition

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

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

contains-product-ideal-Ring :
{l4 : Level} (K : ideal-Ring l4 R) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
contains-product-ideal-Ring K =
(x y : type-Ring R) →
is-in-ideal-Ring R I x → is-in-ideal-Ring R J y →
is-in-ideal-Ring R K (mul-Ring R x y)

is-product-ideal-Ring :
{l4 : Level} (K : ideal-Ring l4 R) → contains-product-ideal-Ring K → UUω
is-product-ideal-Ring K H =
{l5 : Level} (L : ideal-Ring l5 R) →
contains-product-ideal-Ring L → leq-ideal-Ring R K L


### The product of two ideals in a ring

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

generating-subset-product-ideal-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) R
generating-subset-product-ideal-Ring =
product-subset-Ring R
( subset-ideal-Ring R I)
( subset-ideal-Ring R J)

product-ideal-Ring : ideal-Ring (l1 ⊔ l2 ⊔ l3) R
product-ideal-Ring = ideal-subset-Ring R generating-subset-product-ideal-Ring

subset-product-ideal-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) R
subset-product-ideal-Ring = subset-ideal-Ring R product-ideal-Ring

is-in-product-ideal-Ring : type-Ring R → UU (l1 ⊔ l2 ⊔ l3)
is-in-product-ideal-Ring = is-in-ideal-Ring R product-ideal-Ring

contains-product-product-ideal-Ring :
(x y : type-Ring R) →
is-in-ideal-Ring R I x → is-in-ideal-Ring R J y →
is-in-product-ideal-Ring (mul-Ring R x y)
contains-product-product-ideal-Ring x y H K =
contains-subset-ideal-subset-Ring R
( generating-subset-product-ideal-Ring)
( mul-Ring R x y)
( unit-trunc-Prop ((x , H) , (y , K) , refl))

is-product-product-ideal-Ring :
is-product-ideal-Ring R I J
( product-ideal-Ring)
( contains-product-product-ideal-Ring)
is-product-product-ideal-Ring K H =
is-ideal-generated-by-subset-ideal-subset-Ring R
( generating-subset-product-ideal-Ring)
( K)
( λ x p →
apply-universal-property-trunc-Prop p
( subset-ideal-Ring R K x)
( λ ((r , p) , ((s , q) , z)) →
is-closed-under-eq-ideal-Ring R K (H r s p q) (inv z)))


## Properties

### The product of ideals preserves inequality of ideals

module _
{l1 l2 l3 l4 l5 : Level} (A : Ring l1)
(I : ideal-Ring l2 A)
(J : ideal-Ring l3 A)
(K : ideal-Ring l4 A)
(L : ideal-Ring l5 A)
where

preserves-leq-product-ideal-Ring :
leq-ideal-Ring A I J →
leq-ideal-Ring A K L →
leq-ideal-Ring A
( product-ideal-Ring A I K)
( product-ideal-Ring A J L)
preserves-leq-product-ideal-Ring p q =
is-product-product-ideal-Ring A I K
( product-ideal-Ring A J L)
( λ x y u v →
contains-product-product-ideal-Ring A J L _ _
( p x u)
( q y v))

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

preserves-leq-left-product-ideal-Ring :
leq-ideal-Ring A I J →
leq-ideal-Ring A
( product-ideal-Ring A I K)
( product-ideal-Ring A J K)
preserves-leq-left-product-ideal-Ring p =
preserves-leq-product-ideal-Ring A I J K K p
( refl-leq-ideal-Ring A K)

preserves-leq-right-product-ideal-Ring :
leq-ideal-Ring A J K →
leq-ideal-Ring A
( product-ideal-Ring A I J)
( product-ideal-Ring A I K)
preserves-leq-right-product-ideal-Ring =
preserves-leq-product-ideal-Ring A I I J K
( refl-leq-ideal-Ring A I)