open import Algebra.Ring.Module.Action
open import Algebra.Group.Subgroup
open import Algebra.Ring.Module
open import Algebra.Group.Ab
open import Algebra.Prelude
open import Algebra.Group
open import Algebra.Ring

open import Data.Power

module Algebra.Ring.Ideal where


# Ideals in ringsπ

An ideal in a ring $R$ is the $\mathbf{Ab}$-enriched analogue of a sieve, when $R$ is considered as an $\mathbf{Ab}$-category with a single object, in that it picks out a sub-$R$-module of $R$, considered as a representable module, in exactly the same way that a sieve on an object $x : \mathcal{C}$ picks out a subfunctor of $γ(x)$. Since we know that $\operatorname*{\mathbf{B}}R$βs composition is given by $R$βs multiplication, and sieves are subsets closed under precomposition, we instantly deduce that ideals are closed under multiplication.

In the $\mathbf{Ab}$-enriched setting, however, there are some more operations that leaves us in the same $\mathbf{Hom}$-group: addition! More generally, the abelian group operations, i.e.Β addition, inverse, and the zero morphism. Putting these together we conclude that an ideal in $R$ is a subset of $R$ containing the identity, which is closed under multiplication and addition.

module _ {β} (R : Ring β) where
private module R = Ring-on (R .snd)

record is-ideal (π : β β R β) : Type (lsuc β) where
no-eta-equality
field

-- Note: these are named after the side the scalar acts on.
has-*β : β x {y} β y β π β (x R.* y) β π
has-*α΅£ : β x {y} β y β π β (y R.* x) β π

Note

Since most of the rings over which we want to consider ideals are commutative rings, we will limit ourselves to the definition of two-sided ideals: Those for which we have, for $y \in \mathfrak{a}$ and any element $x : R$, $xy \in \mathfrak{a}$ and $yx \in \mathfrak{a}$.

    open represents-subgroup has-rep-subgroup
renaming ( has-unit to has-0 ; has-β to has-+ ; has-inv to has-neg )
public

idealβnormal .normal-subgroup.has-rep = has-rep-subgroup
idealβnormal .normal-subgroup.has-conjugate {y = y} xβπ =
subst (_β π) (sym (ap (y R.+_) R.+-commutes β R.cancell R.+-invr)) xβπ

open normal-subgroup idealβnormal hiding (has-rep) public


Since an ideal is a subgroup of $R$βs additive group, its total space inherits a group structure, and since multiplication in $R$ distributes over addition in $R$, the group structure induced on $\mathfrak{a}$ carries a canonical $R$-module structure.

  idealβmodule : (π : β β R β) β is-ideal π β Module R β
idealβmodule π x = g .fst , mod where
open Ring-action
open is-ideal x
gr : Group-on _
gr = rep-subgroupβgroup-on π has-rep-subgroup

g = from-commutative-group (el! _ , gr) Ξ» x y β Ξ£-prop-path! R.+-commutes

mod : Module-on R β g β
mod = ActionβModule-on R {G = g .snd} Ξ» where
._β_ r (a , b) β _ , has-*β r b
.β-distribl r x y β Ξ£-prop-path! R.*-distribl
.β-distribr r s x β Ξ£-prop-path! R.*-distribr
.β-assoc r s x    β Ξ£-prop-path! R.*-associative
.β-id x           β Ξ£-prop-path! R.*-idl


Since a map between modules is a monomorphism when its underlying function is injective, and the first projection from a subset is always injective, we can quickly conclude that the module structure on $\mathfrak{a}$ is a sub-$R$-module of $R$:

  idealβsubmodule
: {π : β β R β} (idl : is-ideal π)
β idealβmodule π idl R-Mod.βͺ representable-module R
idealβsubmodule {π = π} idl = record
{ mor   = total-hom fst (record { linear = Ξ» _ _ _ β refl })
; monic = Ξ» {c = c} g h x β Structured-hom-path (R-Mod-structure R) \$
embeddingβmonic (Subset-proj-embedding Ξ» _ β π _ .is-tr) (g .hom) (h .hom) (ap hom x)
}


## Principal idealsπ

Every element $a : R$ generates an ideal: that of its multiples, which we denote $(a)$. Youβll note that we have to use the $\exists$ quantifier (rather than the $\sigma$ quantifier) to define $(a)$, since in an arbitrary ring, multiplication by $a$ may fail to be injective, so, given $a, b : R$ $b = ca = c'a$, we canβt in general conclude that $c = c'$. Of course, in any ring, multiplication by zero is never injective.

Note that, since our ideals are all two-sided (for simplicity) but our rings may not be commutative (for expressiveness), if we want the ideal generated by an element to be two-sided, then our ring must be commutative.

  principal-ideal
: (β x y β x R.* y β‘ y R.* x)
β (a : β R β)
β is-ideal Ξ» b β elΞ© (Ξ£ _ Ξ» c β b β‘ c R.* a)
principal-ideal comm a = record
{ has-rep-subgroup = record
{ has-unit = pure (_ , sym R.*-zerol)
; has-β    = Ξ» x y β do
(xi , p) β x
(yi , q) β y
pure (xi R.+ yi , apβ R._+_ p q β sym R.*-distribr)
; has-inv  = Ξ» x β do
(xi , p) β x
pure (R.- xi , ap R.-_ p β R.neg-*-l)
}
; has-*β = Ξ» x y β do
(yi , q) β y
pure (x R.* yi , ap (x R.*_) q β R.*-associative)
; has-*α΅£ = Ξ» x y β do
(yi , q) β y
pure ( yi R.* x
, ap (R._* x) q Β·Β· sym R.*-associative Β·Β· ap (yi R.*_) (comm a x)
β R.*-associative)
}