module Algebra.Ring.Ideal where
Ideals in ringsπ
An ideal in a ring is the -enriched analogue of a sieve, when is considered as an -category with a single object, in that it picks out a sub--module of , considered as a representable ring, in exactly the same way that a sieve on an object picks out a subfunctor of . Since we know that βs composition is given by βs multiplication, and sieves are subsets closed under precomposition, we instantly deduce that ideals are closed under multiplication.
In the -enriched setting, however, there are some more operations that leaves us in the same -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 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 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 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 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 βs 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 -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 is a sub--module 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) }