Products of subsets of commutative rings

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

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

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

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

open import ring-theory.products-subsets-rings

Idea

The product of two subsets S and T of a commutative ring A is the subset consistng of products xy where x ∈ S and y ∈ T.

Definition

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

  product-subset-Commutative-Ring : subset-Commutative-Ring (l1 ⊔ l2 ⊔ l3) A
  product-subset-Commutative-Ring =
    product-subset-Ring (ring-Commutative-Ring A) S T

Properties

The product of subsets of commutative rings is associative

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

  forward-inclusion-associative-product-subset-Commutative-Ring :
    ( product-subset-Commutative-Ring A
      ( product-subset-Commutative-Ring A R S)
      ( T)) ⊆
    ( product-subset-Commutative-Ring A
      ( R)
      ( product-subset-Commutative-Ring A S T))
  forward-inclusion-associative-product-subset-Commutative-Ring =
    forward-inclusion-associative-product-subset-Ring
      ( ring-Commutative-Ring A)
      ( R)
      ( S)
      ( T)

  backward-inclusion-associative-product-subset-Commutative-Ring :
    ( product-subset-Commutative-Ring A
      ( R)
      ( product-subset-Commutative-Ring A S T)) ⊆
    ( product-subset-Commutative-Ring A
      ( product-subset-Commutative-Ring A R S)
      ( T))
  backward-inclusion-associative-product-subset-Commutative-Ring =
    backward-inclusion-associative-product-subset-Ring
      ( ring-Commutative-Ring A)
      ( R)
      ( S)
      ( T)

  associative-product-subset-Commutative-Ring :
    product-subset-Commutative-Ring A
      ( product-subset-Commutative-Ring A R S)
      ( T) ＝
    product-subset-Commutative-Ring A
      ( R)
      ( product-subset-Commutative-Ring A S T)
  associative-product-subset-Commutative-Ring =
    associative-product-subset-Ring (ring-Commutative-Ring A) R S T

Products distribute over unions of families of subsets

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

  forward-inclusion-distributive-product-union-family-of-subsets-Commutative-Ring :
    product-subset-Commutative-Ring A S (union-family-of-subtypes T) ⊆
    union-family-of-subtypes (λ i → product-subset-Commutative-Ring A S (T i))
  forward-inclusion-distributive-product-union-family-of-subsets-Commutative-Ring =
    forward-inclusion-distributive-product-union-family-of-subsets-Ring
      ( ring-Commutative-Ring A)
      ( S)
      ( T)

  backward-inclusion-distributive-product-union-family-of-subsets-Commutative-Ring :
    union-family-of-subtypes
      ( λ i → product-subset-Commutative-Ring A S (T i)) ⊆
    product-subset-Commutative-Ring A S (union-family-of-subtypes T)
  backward-inclusion-distributive-product-union-family-of-subsets-Commutative-Ring =
    backward-inclusion-distributive-product-union-family-of-subsets-Ring
      ( ring-Commutative-Ring A)
      ( S)
      ( T)

  distributive-product-union-family-of-subsets-Commutative-Ring :
    product-subset-Commutative-Ring A S (union-family-of-subtypes T) ＝
    union-family-of-subtypes (λ i → product-subset-Commutative-Ring A S (T i))
  distributive-product-union-family-of-subsets-Commutative-Ring =
    distributive-product-union-family-of-subsets-Ring
      ( ring-Commutative-Ring A)
      ( S)
      ( T)

Recent changes