# Ideals of semirings

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

Created on 2023-03-18.

module ring-theory.ideals-semirings where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.submonoids

open import ring-theory.semirings
open import ring-theory.subsets-semirings


## Idea

An ideal (resp. a left/right ideal) of a semiring R is an additive submodule of R that is closed under multiplication by elements of R (from the left/right).

### Note

This is the standard definition of ideals in semirings. However, such two-sided ideals do not correspond uniquely to congruences on R. If we ask in addition that the underlying additive submodule is normal, then we get unique correspondence to congruences. We will call such ideals normal.

## Definitions

module _
{l1 : Level} (R : Semiring l1)
where

{l2 : Level} → subset-Semiring l2 R → UU (l1 ⊔ l2)


### Left ideals

module _
{l1 : Level} (R : Semiring l1)
where

is-left-ideal-subset-Semiring :
{l2 : Level} → subset-Semiring l2 R → UU (l1 ⊔ l2)
is-left-ideal-subset-Semiring P =
is-closed-under-left-multiplication-subset-Semiring R P

left-ideal-Semiring :
(l : Level) {l1 : Level} (R : Semiring l1) → UU (lsuc l ⊔ l1)
left-ideal-Semiring l R =
Σ (subset-Semiring l R) (is-left-ideal-subset-Semiring R)

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

subset-left-ideal-Semiring : subset-Semiring l2 R
subset-left-ideal-Semiring = pr1 I

is-in-left-ideal-Semiring : type-Semiring R → UU l2
is-in-left-ideal-Semiring x = type-Prop (subset-left-ideal-Semiring x)

type-left-ideal-Semiring : UU (l1 ⊔ l2)
type-left-ideal-Semiring = type-subset-Semiring R subset-left-ideal-Semiring

inclusion-left-ideal-Semiring : type-left-ideal-Semiring → type-Semiring R
inclusion-left-ideal-Semiring =
inclusion-subset-Semiring R subset-left-ideal-Semiring

ap-inclusion-left-ideal-Semiring :
(x y : type-left-ideal-Semiring) → x ＝ y →
inclusion-left-ideal-Semiring x ＝ inclusion-left-ideal-Semiring y
ap-inclusion-left-ideal-Semiring =
ap-inclusion-subset-Semiring R subset-left-ideal-Semiring

is-in-subset-inclusion-left-ideal-Semiring :
(x : type-left-ideal-Semiring) →
is-in-left-ideal-Semiring (inclusion-left-ideal-Semiring x)
is-in-subset-inclusion-left-ideal-Semiring =
is-in-subset-inclusion-subset-Semiring R subset-left-ideal-Semiring

is-closed-under-eq-left-ideal-Semiring :
{x y : type-Semiring R} → is-in-left-ideal-Semiring x →
(x ＝ y) → is-in-left-ideal-Semiring y
is-closed-under-eq-left-ideal-Semiring =
is-closed-under-eq-subset-Semiring R subset-left-ideal-Semiring

is-closed-under-eq-left-ideal-Semiring' :
{x y : type-Semiring R} → is-in-left-ideal-Semiring y →
(x ＝ y) → is-in-left-ideal-Semiring x
is-closed-under-eq-left-ideal-Semiring' =
is-closed-under-eq-subset-Semiring' R subset-left-ideal-Semiring

is-left-ideal-subset-left-ideal-Semiring :
is-left-ideal-subset-Semiring R subset-left-ideal-Semiring
is-left-ideal-subset-left-ideal-Semiring = pr2 I

pr1 is-left-ideal-subset-left-ideal-Semiring

contains-zero-left-ideal-Semiring :
is-in-left-ideal-Semiring (zero-Semiring R)
contains-zero-left-ideal-Semiring =

is-closed-under-left-multiplication-left-ideal-Semiring :
is-closed-under-left-multiplication-subset-Semiring R
subset-left-ideal-Semiring
is-closed-under-left-multiplication-left-ideal-Semiring =
pr2 is-left-ideal-subset-left-ideal-Semiring


### Right ideals

module _
{l1 : Level} (R : Semiring l1)
where

is-right-ideal-subset-Semiring :
{l2 : Level} → subset-Semiring l2 R → UU (l1 ⊔ l2)
is-right-ideal-subset-Semiring P =
is-closed-under-right-multiplication-subset-Semiring R P

right-ideal-Semiring :
(l : Level) {l1 : Level} (R : Semiring l1) → UU (lsuc l ⊔ l1)
right-ideal-Semiring l R =
Σ (subset-Semiring l R) (is-right-ideal-subset-Semiring R)

module _
{l1 l2 : Level} (R : Semiring l1) (I : right-ideal-Semiring l2 R)
where

subset-right-ideal-Semiring : subset-Semiring l2 R
subset-right-ideal-Semiring = pr1 I

is-in-right-ideal-Semiring : type-Semiring R → UU l2
is-in-right-ideal-Semiring x = type-Prop (subset-right-ideal-Semiring x)

type-right-ideal-Semiring : UU (l1 ⊔ l2)
type-right-ideal-Semiring =
type-subset-Semiring R subset-right-ideal-Semiring

inclusion-right-ideal-Semiring : type-right-ideal-Semiring → type-Semiring R
inclusion-right-ideal-Semiring =
inclusion-subset-Semiring R subset-right-ideal-Semiring

ap-inclusion-right-ideal-Semiring :
(x y : type-right-ideal-Semiring) → x ＝ y →
inclusion-right-ideal-Semiring x ＝ inclusion-right-ideal-Semiring y
ap-inclusion-right-ideal-Semiring =
ap-inclusion-subset-Semiring R subset-right-ideal-Semiring

is-in-subset-inclusion-right-ideal-Semiring :
(x : type-right-ideal-Semiring) →
is-in-right-ideal-Semiring (inclusion-right-ideal-Semiring x)
is-in-subset-inclusion-right-ideal-Semiring =
is-in-subset-inclusion-subset-Semiring R subset-right-ideal-Semiring

is-closed-under-eq-right-ideal-Semiring :
{x y : type-Semiring R} → is-in-right-ideal-Semiring x →
(x ＝ y) → is-in-right-ideal-Semiring y
is-closed-under-eq-right-ideal-Semiring =
is-closed-under-eq-subset-Semiring R subset-right-ideal-Semiring

is-closed-under-eq-right-ideal-Semiring' :
{x y : type-Semiring R} → is-in-right-ideal-Semiring y →
(x ＝ y) → is-in-right-ideal-Semiring x
is-closed-under-eq-right-ideal-Semiring' =
is-closed-under-eq-subset-Semiring' R subset-right-ideal-Semiring

is-right-ideal-subset-right-ideal-Semiring :
is-right-ideal-subset-Semiring R subset-right-ideal-Semiring
is-right-ideal-subset-right-ideal-Semiring = pr2 I

pr1 is-right-ideal-subset-right-ideal-Semiring

contains-zero-right-ideal-Semiring :
is-in-right-ideal-Semiring (zero-Semiring R)
contains-zero-right-ideal-Semiring =

is-closed-under-right-multiplication-right-ideal-Semiring :
is-closed-under-right-multiplication-subset-Semiring R
subset-right-ideal-Semiring
is-closed-under-right-multiplication-right-ideal-Semiring =
pr2 is-right-ideal-subset-right-ideal-Semiring


### Two-sided ideals

is-ideal-subset-Semiring :
{l1 l2 : Level} (R : Semiring l1) (P : subset-Semiring l2 R) → UU (l1 ⊔ l2)
is-ideal-subset-Semiring R P =
( is-closed-under-left-multiplication-subset-Semiring R P ×
is-closed-under-right-multiplication-subset-Semiring R P)

ideal-Semiring :
(l : Level) {l1 : Level} (R : Semiring l1) → UU (lsuc l ⊔ l1)
ideal-Semiring l R =
Σ (subset-Semiring l R) (is-ideal-subset-Semiring R)

module _
{l1 l2 : Level} (R : Semiring l1) (I : ideal-Semiring l2 R)
where

subset-ideal-Semiring : subset-Semiring l2 R
subset-ideal-Semiring = pr1 I

is-in-ideal-Semiring : type-Semiring R → UU l2
is-in-ideal-Semiring =
is-in-subset-Semiring R subset-ideal-Semiring

is-prop-is-in-ideal-Semiring :
(x : type-Semiring R) → is-prop (is-in-ideal-Semiring x)
is-prop-is-in-ideal-Semiring =
is-prop-is-in-subset-Semiring R subset-ideal-Semiring

type-ideal-Semiring : UU (l1 ⊔ l2)
type-ideal-Semiring =
type-subset-Semiring R subset-ideal-Semiring

inclusion-ideal-Semiring :
type-ideal-Semiring → type-Semiring R
inclusion-ideal-Semiring =
inclusion-subset-Semiring R subset-ideal-Semiring

ap-inclusion-ideal-Semiring :
(x y : type-ideal-Semiring) → x ＝ y →
inclusion-ideal-Semiring x ＝ inclusion-ideal-Semiring y
ap-inclusion-ideal-Semiring =
ap-inclusion-subset-Semiring R subset-ideal-Semiring

is-in-subset-inclusion-ideal-Semiring :
(x : type-ideal-Semiring) →
is-in-ideal-Semiring (inclusion-ideal-Semiring x)
is-in-subset-inclusion-ideal-Semiring =
is-in-subset-inclusion-subset-Semiring R subset-ideal-Semiring

is-closed-under-eq-ideal-Semiring :
{x y : type-Semiring R} → is-in-ideal-Semiring x →
(x ＝ y) → is-in-ideal-Semiring y
is-closed-under-eq-ideal-Semiring =
is-closed-under-eq-subset-Semiring R subset-ideal-Semiring

is-closed-under-eq-ideal-Semiring' :
{x y : type-Semiring R} → is-in-ideal-Semiring y →
(x ＝ y) → is-in-ideal-Semiring x
is-closed-under-eq-ideal-Semiring' =
is-closed-under-eq-subset-Semiring' R subset-ideal-Semiring

is-ideal-subset-ideal-Semiring :
is-ideal-subset-Semiring R subset-ideal-Semiring
is-ideal-subset-ideal-Semiring = pr2 I

pr1 is-ideal-subset-ideal-Semiring

contains-zero-ideal-Semiring :
is-in-ideal-Semiring (zero-Semiring R)
contains-zero-ideal-Semiring =

is-closed-under-left-multiplication-ideal-Semiring :
is-closed-under-left-multiplication-subset-Semiring R subset-ideal-Semiring
is-closed-under-left-multiplication-ideal-Semiring =
pr1 (pr2 is-ideal-subset-ideal-Semiring)

is-closed-under-right-multiplication-ideal-Semiring :
is-closed-under-right-multiplication-subset-Semiring R subset-ideal-Semiring
is-closed-under-right-multiplication-ideal-Semiring =
pr2 (pr2 is-ideal-subset-ideal-Semiring)

submonoid-ideal-Semiring : Submonoid l2 (additive-monoid-Semiring R)
pr1 submonoid-ideal-Semiring = subset-ideal-Semiring
pr1 (pr2 submonoid-ideal-Semiring) = contains-zero-ideal-Semiring