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 is the analogue of a sieve, when is considered as an with a single object, in that it picks out a sub- of considered as a representable module, in exactly the same way that a sieve on an object picks out a subfunctor of Since we know that composition is given by multiplication, and sieves are subsets closed under precomposition, we instantly deduce that ideals are closed under multiplication.

In the setting, however, there are some more operations that leaves us in the same addition! More generally, the abelian group operations, i.e.Β addition, inverse, and the zero morphism. Putting these together we conclude that an ideal in is a subset of 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 and any element and

    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 additive group, its total space inherits a group structure, and since multiplication in distributes over addition in the group structure induced on carries a canonical 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 is a sub- of

  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 generates an ideal: that of its multiples, which we denote Youβll note that we have to use the quantifier (rather than the quantifier) to define since in an arbitrary ring, multiplication by may fail to be injective, so, given we canβt in general conclude that 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)
}