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}$-enriched analogue of a sieve, when $R$ is considered as an $\mathbf{Ab}$-category with a single object, in that it picks out a sub-$R$-module of $R$, 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)$. Since we know that $\operatorname*{\mathbf{B}}R$’s composition is given by $R$’s multiplication, and sieves are subsets closed under precomposition, we instantly deduce that ideals are closed under multiplication.

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

-- 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 \in \mathfrak{a}$ and any element $x : R$, $xy \in \mathfrak{a}$ and $yx \in \mathfrak{a}$.

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

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

  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)
}