# Products of left ideals of rings

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

Created on 2023-06-08.

module ring-theory.products-left-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.left-ideals-generated-by-subsets-rings
open import ring-theory.left-ideals-rings
open import ring-theory.poset-of-left-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 left ideals I and J in a ring is the left ideal generated by all products of elements in I and J.

## Definition

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

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

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

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


### The product of two left ideals in a ring

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

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

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

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

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

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

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


## Properties

### The product of left ideals preserves inequality of left ideals

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

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

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

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

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