Ideals generated by subsets of commutative rings

Content created by Fredrik Bakke, Egbert Rijke and Maša Žaucer.

Created on 2023-05-04.
Last modified on 2023-06-09.

module commutative-algebra.ideals-generated-by-subsets-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.poset-of-ideals-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.identity-types
open import foundation.subtypes
open import foundation.universe-levels

open import lists.concatenation-lists

open import ring-theory.ideals-generated-by-subsets-rings

Idea

The ideal generated by a subset S of a commutative ring R is the least ideal that contains S.

Definitions

The universal property of the ideal generated by a subset

module _
  {l1 l2 l3 : Level} (R : Commutative-Ring l1)
  (S : subset-Commutative-Ring l2 R)
  (I : ideal-Commutative-Ring l3 R) (H : S ⊆ subset-ideal-Commutative-Ring R I)
  where

  is-ideal-generated-by-subset-Commutative-Ring :
    (l : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l)
  is-ideal-generated-by-subset-Commutative-Ring l =
    (J : ideal-Commutative-Ring l R) →
    S ⊆ subset-ideal-Commutative-Ring R J →
    subset-ideal-Commutative-Ring R I ⊆ subset-ideal-Commutative-Ring R J

The ideal generated by a subset

module _
  {l1 l2 : Level} (R : Commutative-Ring l1) (S : subset-Commutative-Ring l2 R)
  where

  formal-combination-subset-Commutative-Ring : UU (l1 ⊔ l2)
  formal-combination-subset-Commutative-Ring =
    formal-combination-subset-Ring (ring-Commutative-Ring R) S

  ev-formal-combination-subset-Commutative-Ring :
    formal-combination-subset-Commutative-Ring → type-Commutative-Ring R
  ev-formal-combination-subset-Commutative-Ring =
    ev-formal-combination-subset-Ring (ring-Commutative-Ring R) S

  preserves-concat-ev-formal-combination-subset-Commutative-Ring :
    (u v : formal-combination-subset-Commutative-Ring) →
    ( ev-formal-combination-subset-Commutative-Ring (concat-list u v)) ＝
    ( add-Commutative-Ring R
      ( ev-formal-combination-subset-Commutative-Ring u)
      ( ev-formal-combination-subset-Commutative-Ring v))
  preserves-concat-ev-formal-combination-subset-Commutative-Ring =
    preserves-concat-ev-formal-combination-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  mul-formal-combination-subset-Commutative-Ring :
    type-Commutative-Ring R →
    formal-combination-subset-Commutative-Ring →
    type-Commutative-Ring R →
    formal-combination-subset-Commutative-Ring
  mul-formal-combination-subset-Commutative-Ring =
    mul-formal-combination-subset-Ring (ring-Commutative-Ring R) S

  preserves-mul-ev-formal-combination-subset-Commutative-Ring :
    (r : type-Commutative-Ring R)
    (u : formal-combination-subset-Commutative-Ring)
    (t : type-Commutative-Ring R) →
    ev-formal-combination-subset-Commutative-Ring
      ( mul-formal-combination-subset-Commutative-Ring r u t) ＝
    mul-Commutative-Ring R
      ( mul-Commutative-Ring R r
        ( ev-formal-combination-subset-Commutative-Ring u))
      ( t)
  preserves-mul-ev-formal-combination-subset-Commutative-Ring =
    preserves-mul-ev-formal-combination-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  subset-ideal-subset-Commutative-Ring' : type-Commutative-Ring R → UU (l1 ⊔ l2)
  subset-ideal-subset-Commutative-Ring' =
    subset-ideal-subset-Ring'
      ( ring-Commutative-Ring R)
      ( S)

  subset-ideal-subset-Commutative-Ring : subset-Commutative-Ring (l1 ⊔ l2) R
  subset-ideal-subset-Commutative-Ring =
    subset-ideal-subset-Ring (ring-Commutative-Ring R) S

  is-in-ideal-subset-Commutative-Ring : type-Commutative-Ring R → UU (l1 ⊔ l2)
  is-in-ideal-subset-Commutative-Ring =
    is-in-ideal-subset-Ring (ring-Commutative-Ring R) S

  contains-zero-ideal-subset-Commutative-Ring :
    contains-zero-subset-Commutative-Ring R subset-ideal-subset-Commutative-Ring
  contains-zero-ideal-subset-Commutative-Ring =
    contains-zero-ideal-subset-Ring (ring-Commutative-Ring R) S

  is-closed-under-addition-ideal-subset-Commutative-Ring :
    is-closed-under-addition-subset-Commutative-Ring R
      subset-ideal-subset-Commutative-Ring
  is-closed-under-addition-ideal-subset-Commutative-Ring =
    is-closed-under-addition-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  is-closed-under-left-multiplication-ideal-subset-Commutative-Ring :
    is-closed-under-left-multiplication-subset-Commutative-Ring R
      subset-ideal-subset-Commutative-Ring
  is-closed-under-left-multiplication-ideal-subset-Commutative-Ring =
    is-closed-under-left-multiplication-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  is-closed-under-right-multiplication-ideal-subset-Commutative-Ring :
    is-closed-under-right-multiplication-subset-Commutative-Ring R
      subset-ideal-subset-Commutative-Ring
  is-closed-under-right-multiplication-ideal-subset-Commutative-Ring =
    is-closed-under-right-multiplication-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  is-closed-under-negatives-ideal-subset-Commutative-Ring :
    is-closed-under-negatives-subset-Commutative-Ring R
      subset-ideal-subset-Commutative-Ring
  is-closed-under-negatives-ideal-subset-Commutative-Ring =
    is-closed-under-negatives-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  ideal-subset-Commutative-Ring : ideal-Commutative-Ring (l1 ⊔ l2) R
  ideal-subset-Commutative-Ring =
    ideal-subset-Ring (ring-Commutative-Ring R) S

  contains-subset-ideal-subset-Commutative-Ring :
    S ⊆ subset-ideal-subset-Commutative-Ring
  contains-subset-ideal-subset-Commutative-Ring =
    contains-subset-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  contains-formal-combinations-ideal-subset-Commutative-Ring :
    {l3 : Level} (I : ideal-Commutative-Ring l3 R) →
    S ⊆ subset-ideal-Commutative-Ring R I →
    (x : formal-combination-subset-Commutative-Ring) →
    is-in-ideal-Commutative-Ring R I
      ( ev-formal-combination-subset-Commutative-Ring x)
  contains-formal-combinations-ideal-subset-Commutative-Ring I =
    contains-formal-combinations-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)
      ( I)

  is-ideal-generated-by-subset-ideal-subset-Commutative-Ring :
    {l : Level} →
    is-ideal-generated-by-subset-Commutative-Ring R S
      ( ideal-subset-Commutative-Ring)
      ( contains-subset-ideal-subset-Commutative-Ring)
      ( l)
  is-ideal-generated-by-subset-ideal-subset-Commutative-Ring I =
    is-ideal-generated-by-subset-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)
      ( I)

  is-closed-under-eq-ideal-subset-Commutative-Ring :
    {x y : type-Commutative-Ring R} → is-in-ideal-subset-Commutative-Ring x →
    (x ＝ y) → is-in-ideal-subset-Commutative-Ring y
  is-closed-under-eq-ideal-subset-Commutative-Ring =
    is-closed-under-eq-ideal-Commutative-Ring R ideal-subset-Commutative-Ring

  is-closed-under-eq-ideal-subset-Commutative-Ring' :
    {x y : type-Commutative-Ring R} → is-in-ideal-subset-Commutative-Ring y →
    (x ＝ y) → is-in-ideal-subset-Commutative-Ring x
  is-closed-under-eq-ideal-subset-Commutative-Ring' =
    is-closed-under-eq-ideal-Commutative-Ring' R ideal-subset-Commutative-Ring

Properties

The subset relation is preserved by generating ideals

module _
  {l1 l2 l3 : Level} (A : Commutative-Ring l1)
  (S : subset-Commutative-Ring l2 A) (T : subset-Commutative-Ring l3 A)
  where

  preserves-order-ideal-subset-Commutative-Ring :
    S ⊆ T →
    leq-ideal-Commutative-Ring A
      ( ideal-subset-Commutative-Ring A S)
      ( ideal-subset-Commutative-Ring A T)
  preserves-order-ideal-subset-Commutative-Ring =
    preserves-order-ideal-subset-Ring (ring-Commutative-Ring A) S T

The ideal generated by the underlying set of an ideal I is I itself

module _
  {l1 l2 : Level} (A : Commutative-Ring l1) (I : ideal-Commutative-Ring l2 A)
  where

  forward-inclusion-idempotent-ideal-subset-Commutative-Ring :
    leq-ideal-Commutative-Ring A
      ( ideal-subset-Commutative-Ring A (subset-ideal-Commutative-Ring A I))
      ( I)
  forward-inclusion-idempotent-ideal-subset-Commutative-Ring =
    forward-inclusion-idempotent-ideal-subset-Ring (ring-Commutative-Ring A) I

  backward-inclusion-idempotent-ideal-subset-Commutative-Ring :
    leq-ideal-Commutative-Ring A
      ( I)
      ( ideal-subset-Commutative-Ring A (subset-ideal-Commutative-Ring A I))
  backward-inclusion-idempotent-ideal-subset-Commutative-Ring =
    backward-inclusion-idempotent-ideal-subset-Ring (ring-Commutative-Ring A) I

  idempotent-ideal-subset-Commutative-Ring :
    has-same-elements-ideal-Commutative-Ring A
      ( ideal-subset-Commutative-Ring A (subset-ideal-Commutative-Ring A I))
      ( I)
  idempotent-ideal-subset-Commutative-Ring =
    idempotent-ideal-subset-Ring (ring-Commutative-Ring A) I

Recent changes