module Algebra.Ring.Ideal where

# Ideals in ringsπ

An **ideal** in a ring
$R$
is the $Ab-enriched$
analogue of a sieve, when
$R$
is considered as an
$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:C$
picks out a subfunctor of
$γ(x).$
Since we know that
$BRβ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 $Ab-enriched$ setting, however, there are some more operations that leaves us in the same $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βa$
and any element
$x:R,$
$xyβa$
and
$yxβ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 $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 $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
$β$
quantifier (rather than the
$Ο$
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) }