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 $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 ring, 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)
open Module hiding (module R ; module G)

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}$.

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 , 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 $\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   = 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 : 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)
}