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

In the $\mathbf{Ab}\text{-enriched}$ setting, however, there are some more operations that leaves us in the same $\mathbf{Hom}\text{-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)

  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) ∈ 𝔞

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

  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 $a:R$ generates an ideal: that of its multiples, which we denote $(a)\text{.}$ You’ll note that we have to use the $\exists$ quantifier (rather than the $\sigma$ quantifier) to define $(a)\text{,}$ since in an arbitrary ring, multiplication by $a$ may fail to be injective, so, given $a,b:R$ $b=ca=c^{\prime }a\text{,}$ we can’t in general conclude that $c=c^{\prime }\text{.}$ 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)
    }