Products of subsets of rings

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

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

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

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

Idea

The product of two subsets S and T of a ring R consists of elements of the form st where s ∈ S and t ∈ T.

Definition

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

  product-subset-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) A
  product-subset-Ring x =
    trunc-Prop
      ( Σ ( type-subtype S)
          ( λ s →
            Σ ( type-subtype T)
              ( λ t → x ＝ mul-Ring A (pr1 s) (pr1 t))))

Properties

Products distribute over unions of families of subsets

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

  abstract
    forward-inclusion-distributive-product-union-family-of-subsets-Ring :
      product-subset-Ring A S (union-family-of-subtypes T) ⊆
      union-family-of-subtypes (λ i → product-subset-Ring A S (T i))
    forward-inclusion-distributive-product-union-family-of-subsets-Ring x p =
      apply-universal-property-trunc-Prop p
        ( union-family-of-subtypes (λ i → product-subset-Ring A S (T i)) x)
        ( λ where
          ( ( s , Hs) , (t , Ht) , refl) →
            apply-universal-property-trunc-Prop Ht
              ( union-family-of-subtypes
                ( λ i → product-subset-Ring A S (T i))
                ( x))
              ( λ (i , Ht') →
                unit-trunc-Prop
                  ( i , unit-trunc-Prop ((s , Hs) , (t , Ht') , refl))))

  abstract
    backward-inclusion-distributive-product-union-family-of-subsets-Ring :
      union-family-of-subtypes (λ i → product-subset-Ring A S (T i)) ⊆
      product-subset-Ring A S (union-family-of-subtypes T)
    backward-inclusion-distributive-product-union-family-of-subsets-Ring x p =
      apply-universal-property-trunc-Prop p
        ( product-subset-Ring A S (union-family-of-subtypes T) x)
        ( λ (i , u) →
          apply-universal-property-trunc-Prop u
            ( product-subset-Ring A S (union-family-of-subtypes T) x)
            ( λ where
              ( ( s , Hs) , (t , Ht) , refl) →
                unit-trunc-Prop
                  ( (s , Hs) , (t , unit-trunc-Prop (i , Ht)) , refl)))

  distributive-product-union-family-of-subsets-Ring :
    product-subset-Ring A S (union-family-of-subtypes T) ＝
    union-family-of-subtypes (λ i → product-subset-Ring A S (T i))
  distributive-product-union-family-of-subsets-Ring =
    antisymmetric-leq-subtype
      ( product-subset-Ring A S (union-family-of-subtypes T))
      ( union-family-of-subtypes (λ i → product-subset-Ring A S (T i)))
      ( forward-inclusion-distributive-product-union-family-of-subsets-Ring)
      ( backward-inclusion-distributive-product-union-family-of-subsets-Ring)

The product of subsets of commutative rings is associative

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

  abstract
    forward-inclusion-associative-product-subset-Ring :
      ( product-subset-Ring A
        ( product-subset-Ring A R S)
        ( T)) ⊆
      ( product-subset-Ring A
        ( R)
        ( product-subset-Ring A S T))
    forward-inclusion-associative-product-subset-Ring x H =
      apply-universal-property-trunc-Prop H
        ( product-subset-Ring A R
          ( product-subset-Ring A S T)
          ( x))
        ( λ where
          ( ( u , K) , (t , Ht) , refl) →
            apply-universal-property-trunc-Prop K
              ( product-subset-Ring A R
                ( product-subset-Ring A S T)
                ( _))
              ( λ where
                ( ( r , Hr) , (s , Hs) , refl) →
                  unit-trunc-Prop
                    ( ( r , Hr) ,
                      ( ( mul-Ring A s t) ,
                        ( unit-trunc-Prop ((s , Hs) , (t , Ht) , refl))) ,
                      ( associative-mul-Ring A r s t))))

  abstract
    backward-inclusion-associative-product-subset-Ring :
      ( product-subset-Ring A
        ( R)
        ( product-subset-Ring A S T)) ⊆
      ( product-subset-Ring A
        ( product-subset-Ring A R S)
        ( T))
    backward-inclusion-associative-product-subset-Ring x H =
      apply-universal-property-trunc-Prop H
        ( product-subset-Ring A
          ( product-subset-Ring A R S)
          ( T)
          ( x))
        ( λ where
          ( ( r , Hr) , (v , K) , refl) →
            apply-universal-property-trunc-Prop K
              ( product-subset-Ring A
                ( product-subset-Ring A R S)
                ( T)
                ( _))
              ( λ where
                ( ( s , Hs) , (t , Ht) , refl) →
                  unit-trunc-Prop
                    ( ( ( mul-Ring A r s) ,
                        ( unit-trunc-Prop ((r , Hr) , (s , Hs) , refl))) ,
                      ( t , Ht) ,
                      ( inv (associative-mul-Ring A r s t)))))

  associative-product-subset-Ring :
    product-subset-Ring A
      ( product-subset-Ring A R S)
      ( T) ＝
    product-subset-Ring A
      ( R)
      ( product-subset-Ring A S T)
  associative-product-subset-Ring =
    eq-has-same-elements-subtype
      ( product-subset-Ring A
        ( product-subset-Ring A R S)
        ( T))
      ( product-subset-Ring A
        ( R)
        ( product-subset-Ring A S T))
      ( λ x →
        forward-inclusion-associative-product-subset-Ring x ,
        backward-inclusion-associative-product-subset-Ring x)

Recent changes