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 RR is the Ab{{\mathbf{Ab}}}-enriched analogue of a sieve, when RR is considered as an Ab{{\mathbf{Ab}}}-category with a single object, in that it picks out a sub-RR-module of RR, considered as a representable ring, in exactly the same way that a sieve on an object x:Cx : \mathcal{C} picks out a subfunctor of γ‚ˆ(x){γ‚ˆ}(x). Since we know that B⁑R\operatorname*{\mathbf{B}}R’s composition is given by RR’s multiplication, and sieves are subsets closed under precomposition, we instantly deduce that ideals are closed under multiplication.

In the Ab{{\mathbf{Ab}}}-enriched setting, however, there are some more operations that leaves us in the same Hom{\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 RR is a subset of RR 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
      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∈ay \in \mathfrak{a} and any element x:Rx : R, xy∈axy \in \mathfrak{a} and yx∈ayx \in \mathfrak{a}.

Since an ideal is a subgroup of RR’s additive group, its total space inherits a group structure, and since multiplication in RR distributes over addition in RR, the group structure induced on a\mathfrak{a} carries a canonical RR-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 a\mathfrak{a} is a sub-RR-module of RR:

    : {π”ž : β„™ ⌞ 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:Ra : R generates an ideal: that of its multiples, which we denote (a)(a). You’ll note that we have to use the βˆƒ\exists quantifier (rather than the Οƒ\sigma quantifier) to define (a)(a), since in an arbitrary ring, multiplication by aa may fail to be injective, so, given a,b:Ra, b : R b=ca=cβ€²ab = ca = c'a, we can’t in general conclude that c=cβ€²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.

    : (βˆ€ 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)