Products of right ideals of rings

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

Created on 2023-06-08.
Last modified on 2023-06-09.

module ring-theory.products-right-ideals-rings where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import ring-theory.poset-of-right-ideals-rings
open import ring-theory.products-subsets-rings
open import ring-theory.right-ideals-generated-by-subsets-rings
open import ring-theory.right-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings

Idea

The product of two right ideals I and J in a ring is the right ideal generated by all products of elements in I and J.

Definition

The universal property of the product of two right ideals in a ring

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

  contains-product-right-ideal-Ring :
    {l4 : Level} (K : right-ideal-Ring l4 R) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  contains-product-right-ideal-Ring K =
    (x y : type-Ring R) →
    is-in-right-ideal-Ring R I x → is-in-right-ideal-Ring R J y →
    is-in-right-ideal-Ring R K (mul-Ring R x y)

  is-product-right-ideal-Ring :
    {l4 : Level} (K : right-ideal-Ring l4 R) →
    contains-product-right-ideal-Ring K → UUω
  is-product-right-ideal-Ring K H =
    {l5 : Level} (L : right-ideal-Ring l5 R) →
    contains-product-right-ideal-Ring L → leq-right-ideal-Ring R K L

The product of two right ideals in a ring

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

  generating-subset-product-right-ideal-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) R
  generating-subset-product-right-ideal-Ring =
    product-subset-Ring R
      ( subset-right-ideal-Ring R I)
      ( subset-right-ideal-Ring R J)

  product-right-ideal-Ring : right-ideal-Ring (l1 ⊔ l2 ⊔ l3) R
  product-right-ideal-Ring =
    right-ideal-subset-Ring R generating-subset-product-right-ideal-Ring

  subset-product-right-ideal-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) R
  subset-product-right-ideal-Ring =
    subset-right-ideal-Ring R product-right-ideal-Ring

  is-in-product-right-ideal-Ring : type-Ring R → UU (l1 ⊔ l2 ⊔ l3)
  is-in-product-right-ideal-Ring =
    is-in-right-ideal-Ring R product-right-ideal-Ring

  contains-product-product-right-ideal-Ring :
    (x y : type-Ring R) →
    is-in-right-ideal-Ring R I x → is-in-right-ideal-Ring R J y →
    is-in-product-right-ideal-Ring (mul-Ring R x y)
  contains-product-product-right-ideal-Ring x y H K =
    contains-subset-right-ideal-subset-Ring R
      ( generating-subset-product-right-ideal-Ring)
      ( mul-Ring R x y)
      ( unit-trunc-Prop ((x , H) , (y , K) , refl))

  is-product-product-right-ideal-Ring :
    is-product-right-ideal-Ring R I J
      ( product-right-ideal-Ring)
      ( contains-product-product-right-ideal-Ring)
  is-product-product-right-ideal-Ring K H =
    is-right-ideal-generated-by-subset-right-ideal-subset-Ring R
      ( generating-subset-product-right-ideal-Ring)
      ( K)
      ( λ x p →
        apply-universal-property-trunc-Prop p
          ( subset-right-ideal-Ring R K x)
          ( λ ((r , p) , ((s , q) , z)) →
            is-closed-under-eq-right-ideal-Ring R K (H r s p q) (inv z)))

Properties

The product of right ideals preserves inequality of right ideals

module _
  {l1 l2 l3 l4 l5 : Level} (A : Ring l1)
  (I : right-ideal-Ring l2 A)
  (J : right-ideal-Ring l3 A)
  (K : right-ideal-Ring l4 A)
  (L : right-ideal-Ring l5 A)
  where

  preserves-leq-product-right-ideal-Ring :
    leq-right-ideal-Ring A I J →
    leq-right-ideal-Ring A K L →
    leq-right-ideal-Ring A
      ( product-right-ideal-Ring A I K)
      ( product-right-ideal-Ring A J L)
  preserves-leq-product-right-ideal-Ring p q =
    is-product-product-right-ideal-Ring A I K
      ( product-right-ideal-Ring A J L)
      ( λ x y u v →
        contains-product-product-right-ideal-Ring A J L _ _
          ( p x u)
          ( q y v))

module _
  {l1 l2 l3 l4 : Level} (A : Ring l1)
  (I : right-ideal-Ring l2 A)
  (J : right-ideal-Ring l3 A)
  (K : right-ideal-Ring l4 A)
  where

  preserves-leq-left-product-right-ideal-Ring :
    leq-right-ideal-Ring A I J →
    leq-right-ideal-Ring A
      ( product-right-ideal-Ring A I K)
      ( product-right-ideal-Ring A J K)
  preserves-leq-left-product-right-ideal-Ring p =
    preserves-leq-product-right-ideal-Ring A I J K K p
      ( refl-leq-right-ideal-Ring A K)

  preserves-leq-right-product-right-ideal-Ring :
    leq-right-ideal-Ring A J K →
    leq-right-ideal-Ring A
      ( product-right-ideal-Ring A I J)
      ( product-right-ideal-Ring A I K)
  preserves-leq-right-product-right-ideal-Ring =
    preserves-leq-product-right-ideal-Ring A I I J K
      ( refl-leq-right-ideal-Ring A I)

Recent changes