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 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) 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 and any element , and .
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 , 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 is a sub--module of :
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 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) }