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 has-rep-subgroup : represents-subgroup R.additive-group π -- 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) β π

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 R.additive-group π 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) }