Ideals in commutative rings

module commutative-algebra.ideals-commutative-rings where
Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

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

Idea

An ideal in a commutative ring is a two-sided ideal in the underlying ring.

Definitions

Ideals in commutative rings

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

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

  is-left-ideal-subset-Commutative-Ring : UU (l1  l2)
  is-left-ideal-subset-Commutative-Ring =
    is-left-ideal-subset-Ring (ring-Commutative-Ring R) S

  is-right-ideal-subset-Commutative-Ring : UU (l1  l2)
  is-right-ideal-subset-Commutative-Ring =
    is-right-ideal-subset-Ring (ring-Commutative-Ring R) S

ideal-Commutative-Ring :
  {l1 : Level} (l2 : Level)  Commutative-Ring l1  UU (l1  lsuc l2)
ideal-Commutative-Ring l2 R = ideal-Ring l2 (ring-Commutative-Ring R)

left-ideal-Commutative-Ring :
  {l1 : Level} (l2 : Level)  Commutative-Ring l1  UU (l1  lsuc l2)
left-ideal-Commutative-Ring l2 R =
  left-ideal-Ring l2 (ring-Commutative-Ring R)

right-ideal-Commutative-Ring :
  {l1 : Level} (l2 : Level)  Commutative-Ring l1  UU (l1  lsuc l2)
right-ideal-Commutative-Ring l2 R =
  right-ideal-Ring l2 (ring-Commutative-Ring R)

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

  subset-ideal-Commutative-Ring : subset-Commutative-Ring l2 R
  subset-ideal-Commutative-Ring = pr1 I

  is-in-ideal-Commutative-Ring : type-Commutative-Ring R  UU l2
  is-in-ideal-Commutative-Ring x = type-Prop (subset-ideal-Commutative-Ring x)

  type-ideal-Commutative-Ring : UU (l1  l2)
  type-ideal-Commutative-Ring =
    type-subset-Commutative-Ring R subset-ideal-Commutative-Ring

  inclusion-ideal-Commutative-Ring :
    type-ideal-Commutative-Ring  type-Commutative-Ring R
  inclusion-ideal-Commutative-Ring =
    inclusion-subset-Commutative-Ring R subset-ideal-Commutative-Ring

  ap-inclusion-ideal-Commutative-Ring :
    (x y : type-ideal-Commutative-Ring)  x  y 
    inclusion-ideal-Commutative-Ring x  inclusion-ideal-Commutative-Ring y
  ap-inclusion-ideal-Commutative-Ring =
    ap-inclusion-subset-Commutative-Ring R subset-ideal-Commutative-Ring

  is-in-subset-inclusion-ideal-Commutative-Ring :
    (x : type-ideal-Commutative-Ring) 
    is-in-ideal-Commutative-Ring (inclusion-ideal-Commutative-Ring x)
  is-in-subset-inclusion-ideal-Commutative-Ring =
    is-in-subset-inclusion-subset-Commutative-Ring R
      subset-ideal-Commutative-Ring

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

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

  is-ideal-ideal-Commutative-Ring :
    is-ideal-subset-Commutative-Ring R subset-ideal-Commutative-Ring
  is-ideal-ideal-Commutative-Ring =
    is-ideal-ideal-Ring (ring-Commutative-Ring R) I

  is-additive-subgroup-ideal-Commutative-Ring :
    is-additive-subgroup-subset-Ring
      ( ring-Commutative-Ring R)
      ( subset-ideal-Commutative-Ring)
  is-additive-subgroup-ideal-Commutative-Ring =
    is-additive-subgroup-ideal-Ring (ring-Commutative-Ring R) I

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

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

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

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

  left-ideal-ideal-Commutative-Ring : left-ideal-Commutative-Ring l2 R
  left-ideal-ideal-Commutative-Ring =
    left-ideal-ideal-Ring (ring-Commutative-Ring R) I

  right-ideal-ideal-Commutative-Ring : right-ideal-Commutative-Ring l2 R
  right-ideal-ideal-Commutative-Ring =
    right-ideal-ideal-Ring (ring-Commutative-Ring R) I

ideal-left-ideal-Commutative-Ring :
  {l1 l2 : Level} (R : Commutative-Ring l1) (S : subset-Commutative-Ring l2 R) 
  contains-zero-subset-Commutative-Ring R S 
  is-closed-under-addition-subset-Commutative-Ring R S 
  is-closed-under-negatives-subset-Commutative-Ring R S 
  is-closed-under-left-multiplication-subset-Commutative-Ring R S 
  ideal-Commutative-Ring l2 R
pr1 (ideal-left-ideal-Commutative-Ring R S z a n m) = S
pr1 (pr1 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m))) = z
pr1 (pr2 (pr1 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m)))) = a
pr2 (pr2 (pr1 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m)))) = n
pr1 (pr2 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m))) = m
pr2 (pr2 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m))) x y H =
  is-closed-under-eq-subset-Commutative-Ring R S
    ( m y x H)
    ( commutative-mul-Commutative-Ring R y x)

ideal-right-ideal-Commutative-Ring :
  {l1 l2 : Level} (R : Commutative-Ring l1) (S : subset-Commutative-Ring l2 R) 
  contains-zero-subset-Commutative-Ring R S 
  is-closed-under-addition-subset-Commutative-Ring R S 
  is-closed-under-negatives-subset-Commutative-Ring R S 
  is-closed-under-right-multiplication-subset-Commutative-Ring R S 
  ideal-Commutative-Ring l2 R
pr1 (ideal-right-ideal-Commutative-Ring R S z a n m) = S
pr1 (pr1 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m))) = z
pr1 (pr2 (pr1 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m)))) = a
pr2 (pr2 (pr1 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m)))) = n
pr1 (pr2 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m))) x y H =
  is-closed-under-eq-subset-Commutative-Ring R S
    ( m y x H)
    ( commutative-mul-Commutative-Ring R y x)
pr2 (pr2 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m))) = m

Characterizing equality of ideals in commutative rings

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

  has-same-elements-ideal-Commutative-Ring :
    (J : ideal-Commutative-Ring l3 R)  UU (l1  l2  l3)
  has-same-elements-ideal-Commutative-Ring =
    has-same-elements-ideal-Ring (ring-Commutative-Ring R) I

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

  refl-has-same-elements-ideal-Commutative-Ring :
    has-same-elements-ideal-Commutative-Ring R I I
  refl-has-same-elements-ideal-Commutative-Ring =
    refl-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I

  is-contr-total-has-same-elements-ideal-Commutative-Ring :
    is-contr
      ( Σ ( ideal-Commutative-Ring l2 R)
          ( has-same-elements-ideal-Commutative-Ring R I))
  is-contr-total-has-same-elements-ideal-Commutative-Ring =
    is-contr-total-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I

  has-same-elements-eq-ideal-Commutative-Ring :
    (J : ideal-Commutative-Ring l2 R) 
    (I  J)  has-same-elements-ideal-Commutative-Ring R I J
  has-same-elements-eq-ideal-Commutative-Ring =
    has-same-elements-eq-ideal-Ring (ring-Commutative-Ring R) I

  is-equiv-has-same-elements-eq-ideal-Commutative-Ring :
    (J : ideal-Commutative-Ring l2 R) 
    is-equiv (has-same-elements-eq-ideal-Commutative-Ring J)
  is-equiv-has-same-elements-eq-ideal-Commutative-Ring =
    is-equiv-has-same-elements-eq-ideal-Ring (ring-Commutative-Ring R) I

  extensionality-ideal-Commutative-Ring :
    (J : ideal-Commutative-Ring l2 R) 
    (I  J)  has-same-elements-ideal-Commutative-Ring R I J
  extensionality-ideal-Commutative-Ring =
    extensionality-ideal-Ring (ring-Commutative-Ring R) I

  eq-has-same-elements-ideal-Commutative-Ring :
    (J : ideal-Commutative-Ring l2 R) 
    has-same-elements-ideal-Commutative-Ring R I J  I  J
  eq-has-same-elements-ideal-Commutative-Ring =
    eq-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I