# Intersections of ideals of rings

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

Created on 2023-06-08.

module ring-theory.intersections-ideals-rings where

Imports
open import foundation.dependent-pair-types
open import foundation.intersections-subtypes
open import foundation.universe-levels

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

open import ring-theory.ideals-rings
open import ring-theory.poset-of-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings


## Idea

The intersection of two ideals of a ring R consists of the elements contained in both of them.

## Definitions

### The universal property of intersections of ideals in rings

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

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


### Intersections of ideals in rings

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

subset-intersection-ideal-Ring : subset-Ring (l2 ⊔ l3) R
subset-intersection-ideal-Ring =
intersection-subtype (subset-ideal-Ring R I) (subset-ideal-Ring R J)

contains-zero-intersection-ideal-Ring :
contains-zero-subset-Ring R subset-intersection-ideal-Ring
pr1 contains-zero-intersection-ideal-Ring =
contains-zero-ideal-Ring R I
pr2 contains-zero-intersection-ideal-Ring =
contains-zero-ideal-Ring R J

subset-intersection-ideal-Ring
is-closed-under-addition-ideal-Ring R I (pr1 H) (pr1 K)
is-closed-under-addition-ideal-Ring R J (pr2 H) (pr2 K)

is-closed-under-negatives-intersection-ideal-Ring :
is-closed-under-negatives-subset-Ring R
subset-intersection-ideal-Ring
pr1 (is-closed-under-negatives-intersection-ideal-Ring H) =
is-closed-under-negatives-ideal-Ring R I (pr1 H)
pr2 (is-closed-under-negatives-intersection-ideal-Ring H) =
is-closed-under-negatives-ideal-Ring R J (pr2 H)

is-closed-under-left-multiplication-intersection-ideal-Ring :
is-closed-under-left-multiplication-subset-Ring R
subset-intersection-ideal-Ring
pr1 (is-closed-under-left-multiplication-intersection-ideal-Ring x y H) =
is-closed-under-left-multiplication-ideal-Ring R I x y (pr1 H)
pr2 (is-closed-under-left-multiplication-intersection-ideal-Ring x y H) =
is-closed-under-left-multiplication-ideal-Ring R J x y (pr2 H)

is-closed-under-right-multiplication-intersection-ideal-Ring :
is-closed-under-right-multiplication-subset-Ring R
subset-intersection-ideal-Ring
pr1 (is-closed-under-right-multiplication-intersection-ideal-Ring x y H) =
is-closed-under-right-multiplication-ideal-Ring R I x y (pr1 H)
pr2 (is-closed-under-right-multiplication-intersection-ideal-Ring x y H) =
is-closed-under-right-multiplication-ideal-Ring R J x y (pr2 H)

contains-zero-intersection-ideal-Ring
is-closed-under-negatives-intersection-ideal-Ring

is-ideal-intersection-ideal-Ring :
is-ideal-subset-Ring R subset-intersection-ideal-Ring
pr1 is-ideal-intersection-ideal-Ring =
pr1 (pr2 is-ideal-intersection-ideal-Ring) =
is-closed-under-left-multiplication-intersection-ideal-Ring
pr2 (pr2 is-ideal-intersection-ideal-Ring) =
is-closed-under-right-multiplication-intersection-ideal-Ring

intersection-ideal-Ring : ideal-Ring (l2 ⊔ l3) R
pr1 intersection-ideal-Ring = subset-intersection-ideal-Ring
pr2 intersection-ideal-Ring = is-ideal-intersection-ideal-Ring

is-intersection-intersection-ideal-Ring :
is-intersection-ideal-Ring R I J intersection-ideal-Ring
is-intersection-intersection-ideal-Ring K =
is-greatest-binary-lower-bound-intersection-subtype
( subset-ideal-Ring R I)
( subset-ideal-Ring R J)
( subset-ideal-Ring R K)