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 Cat.Functor.FullSubcategory open import Data.Power open import Meta.Bind 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
ring, 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) open Module hiding (module R ; module G) 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) β π

**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}$.

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 , mod where open make-group open is-ideal x gr : Group-on _ gr = rep-subgroupβgroup-on π has-rep-subgroup g = restrict (el! _ , gr) Ξ» x y β Ξ£-prop-path (Ξ» _ β π _ .is-tr) R.+-commutes mod : Module-on R g mod .Module-on._β_ x y = _ , has-*β x (y .snd) mod .Module-on.β-id x = Ξ£-prop-path (Ξ» _ β π _ .is-tr) R.*-idl mod .Module-on.β-add-r r x y = Ξ£-prop-path (Ξ» _ β π _ .is-tr) R.*-distribl mod .Module-on.β-add-l x r s = Ξ£-prop-path (Ξ» _ β π _ .is-tr) R.*-distribr mod .Module-on.β-assoc r s x = Ξ£-prop-path (Ξ» _ β π _ .is-tr) R.*-associative

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 = record { map = fst ; linear = Ξ» r m s n β refl } ; monic = Ξ» {c = c} g h x β Linear-map-path $ embeddingβmonic (Subset-proj-embedding Ξ» _ β π _ .is-tr) (g .map) (h .map) (ap map 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) }