module Algebra.Ring.Ideal where

Ideals in ringsπŸ”—

An ideal in a ring is the analogue of a sieve, when is considered as an with a single object, in that it picks out a sub- of considered as a representable module, in exactly the same way that a sieve on an object picks out a subfunctor of Since we know that composition is given by multiplication, and sieves are subsets closed under precomposition, we instantly deduce that ideals are closed under multiplication.

In the setting, however, there are some more operations that leaves us in the same 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)

  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) ∈ π”ž

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 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 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 is a sub- of

    : {π”ž : β„™ ⌞ 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 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.

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