Linear combinations of tuples of vectors in left modules over rings

Content created by Fredrik Bakke and Šimon Brandner.

Created on 2025-09-12.
Last modified on 2025-09-24.

module linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.left-modules-rings

open import lists.concatenation-tuples
open import lists.functoriality-tuples
open import lists.tuples

open import ring-theory.rings

Idea

Let M be a left module over a ring R. For any n-tuple of vectors (elements of M) (x_1, ..., x_n) and any n-tuple of coefficients (elements of R) (r_1, ..., r_n), we may form the linear combination r_1 * x_1 + ... + r_n * x_n.

The proposition of being a linear combination is formalized as being an element of a linear span.

Definitions

Linear combinations of tuples of vectors in a left module over a ring

module _
  {l1 l2 : Level}
  (R : Ring l1)
  (M : left-module-Ring l2 R)
  where

  linear-combination-tuple-left-module-Ring :
    {n : ℕ} →
    tuple (type-Ring R) n →
    tuple (type-left-module-Ring R M) n →
    type-left-module-Ring R M
  linear-combination-tuple-left-module-Ring empty-tuple empty-tuple =
    zero-left-module-Ring R M
  linear-combination-tuple-left-module-Ring (r ∷ scalars) (x ∷ vectors) =
    add-left-module-Ring R M
      ( linear-combination-tuple-left-module-Ring scalars vectors)
      ( mul-left-module-Ring R M r x)

Properties

Left distributivity law for multiplication

module _
  {l1 l2 : Level}
  (R : Ring l1)
  (M : left-module-Ring l2 R)
  where

  left-distributive-mul-linear-combination-tuple-left-module-Ring :
    {n : ℕ}
    (r : type-Ring R) →
    (scalars : tuple (type-Ring R) n) →
    (vectors : tuple (type-left-module-Ring R M) n) →
    mul-left-module-Ring R M
      ( r)
      ( linear-combination-tuple-left-module-Ring R M scalars vectors) ＝
    linear-combination-tuple-left-module-Ring R M
      ( map-tuple (mul-Ring R r) scalars)
      ( vectors)
  left-distributive-mul-linear-combination-tuple-left-module-Ring
    r empty-tuple empty-tuple =
    equational-reasoning
      mul-left-module-Ring R M r
        ( linear-combination-tuple-left-module-Ring R M empty-tuple empty-tuple)
      ＝ mul-left-module-Ring R M r (zero-left-module-Ring R M)
        by refl
      ＝ zero-left-module-Ring R M
        by right-zero-law-mul-left-module-Ring R M r
      ＝ linear-combination-tuple-left-module-Ring R M empty-tuple empty-tuple
        by refl
  left-distributive-mul-linear-combination-tuple-left-module-Ring
    r (s ∷ scalars) (x ∷ vectors) =
    equational-reasoning
      mul-left-module-Ring R M r
        ( linear-combination-tuple-left-module-Ring R M
          ( s ∷ scalars)
          ( x ∷ vectors))
      ＝ mul-left-module-Ring R M r
          ( add-left-module-Ring R M
            ( linear-combination-tuple-left-module-Ring R M scalars vectors)
            ( mul-left-module-Ring R M s x))
        by refl
      ＝ add-left-module-Ring R M
          ( mul-left-module-Ring R M r
            ( linear-combination-tuple-left-module-Ring R M scalars vectors))
          ( mul-left-module-Ring R M r (mul-left-module-Ring R M s x))
        by
          left-distributive-mul-add-left-module-Ring R M r
            ( linear-combination-tuple-left-module-Ring R M scalars vectors)
            ( mul-left-module-Ring R M s x)
      ＝ add-left-module-Ring R M
          ( mul-left-module-Ring R M r
            ( linear-combination-tuple-left-module-Ring R M scalars vectors))
          ( mul-left-module-Ring R M (mul-Ring R r s) x)
        by
          ap
            ( λ y →
              add-left-module-Ring R M
                ( mul-left-module-Ring R M r
                  ( linear-combination-tuple-left-module-Ring R M
                    ( scalars)
                    ( vectors)))
                ( y))
            ( inv (associative-mul-left-module-Ring R M r s x))
      ＝ add-left-module-Ring R M
          ( linear-combination-tuple-left-module-Ring R M
            ( map-tuple (mul-Ring R r) scalars)
            ( vectors))
          ( mul-left-module-Ring R M (mul-Ring R r s) x)
        by
          ap
            ( λ y →
              add-left-module-Ring R M
                ( y)
                ( mul-left-module-Ring R M (mul-Ring R r s) x))
            ( left-distributive-mul-linear-combination-tuple-left-module-Ring r
              ( scalars)
              ( vectors))
      ＝ linear-combination-tuple-left-module-Ring R M
          ( map-tuple (mul-Ring R r) (s ∷ scalars))
          ( x ∷ vectors)
        by refl

Concatenation is addition

module _
  {l1 l2 : Level}
  (R : Ring l1)
  (M : left-module-Ring l2 R)
  where

  add-concat-linear-combination-tuple-left-module-Ring :
    {n m : ℕ} →
    (scalars-a : tuple (type-Ring R) n) →
    (vectors-a : tuple (type-left-module-Ring R M) n) →
    (scalars-b : tuple (type-Ring R) m) →
    (vectors-b : tuple (type-left-module-Ring R M) m) →
    linear-combination-tuple-left-module-Ring R M
      ( concat-tuple scalars-a scalars-b)
      ( concat-tuple vectors-a vectors-b) ＝
    add-left-module-Ring R M
      ( linear-combination-tuple-left-module-Ring R M scalars-a vectors-a)
      ( linear-combination-tuple-left-module-Ring R M scalars-b vectors-b)
  add-concat-linear-combination-tuple-left-module-Ring
    empty-tuple empty-tuple scalars-b vectors-b =
    equational-reasoning
      linear-combination-tuple-left-module-Ring R M
        ( concat-tuple empty-tuple scalars-b)
        ( concat-tuple empty-tuple vectors-b)
      ＝ linear-combination-tuple-left-module-Ring R M scalars-b vectors-b
        by refl
      ＝ add-left-module-Ring R M
          ( zero-left-module-Ring R M)
          ( linear-combination-tuple-left-module-Ring R M scalars-b vectors-b)
        by
          inv
            ( left-unit-law-add-left-module-Ring R M
              ( linear-combination-tuple-left-module-Ring R M
                ( scalars-b)
                ( vectors-b)))
      ＝ add-left-module-Ring R M
          ( linear-combination-tuple-left-module-Ring R M
            ( empty-tuple)
            ( empty-tuple))
          ( linear-combination-tuple-left-module-Ring R M scalars-b vectors-b)
        by refl
  add-concat-linear-combination-tuple-left-module-Ring
    (r ∷ scalars-a) (x ∷ vectors-a) scalars-b vectors-b =
    equational-reasoning
      linear-combination-tuple-left-module-Ring R M
        ( concat-tuple (r ∷ scalars-a) scalars-b)
        ( concat-tuple (x ∷ vectors-a) vectors-b)
      ＝ linear-combination-tuple-left-module-Ring R M
          ( r ∷ (concat-tuple scalars-a scalars-b))
          ( x ∷ (concat-tuple vectors-a vectors-b))
        by refl
      ＝ add-left-module-Ring R M
          ( linear-combination-tuple-left-module-Ring R M
            ( concat-tuple scalars-a scalars-b)
            ( concat-tuple vectors-a vectors-b))
          ( mul-left-module-Ring R M r x)
        by refl
      ＝ add-left-module-Ring R M
          ( add-left-module-Ring R M
            ( linear-combination-tuple-left-module-Ring R M
              ( scalars-a)
              ( vectors-a))
            ( linear-combination-tuple-left-module-Ring R M
              ( scalars-b)
              ( vectors-b)))
          ( mul-left-module-Ring R M r x)
        by
          ap
            ( λ z → add-left-module-Ring R M z (mul-left-module-Ring R M r x))
            ( add-concat-linear-combination-tuple-left-module-Ring
              ( scalars-a)
              ( vectors-a)
              ( scalars-b)
              ( vectors-b))
      ＝ add-left-module-Ring R M
          ( mul-left-module-Ring R M r x)
          ( add-left-module-Ring R M
            ( linear-combination-tuple-left-module-Ring R M
              ( scalars-a)
              ( vectors-a))
            ( linear-combination-tuple-left-module-Ring R M
              ( scalars-b)
              ( vectors-b)))
        by
          commutative-add-left-module-Ring R M
            ( add-left-module-Ring R M
              ( linear-combination-tuple-left-module-Ring R M
                ( scalars-a)
                ( vectors-a))
              ( linear-combination-tuple-left-module-Ring R M
                ( scalars-b)
                ( vectors-b)))
            ( mul-left-module-Ring R M r x)
      ＝ add-left-module-Ring R M
          ( add-left-module-Ring R M
            ( mul-left-module-Ring R M r x)
            ( linear-combination-tuple-left-module-Ring R M
              ( scalars-a)
              ( vectors-a)))
          ( linear-combination-tuple-left-module-Ring R M
            ( scalars-b)
            ( vectors-b))
        by
          inv
            ( associative-add-left-module-Ring R M
              ( mul-left-module-Ring R M r x)
              ( linear-combination-tuple-left-module-Ring R M
                ( scalars-a)
                ( vectors-a))
              ( linear-combination-tuple-left-module-Ring R M
                ( scalars-b)
                ( vectors-b)))
      ＝ add-left-module-Ring R M
          ( add-left-module-Ring R M
            ( linear-combination-tuple-left-module-Ring R M
              ( scalars-a)
              ( vectors-a))
            ( mul-left-module-Ring R M r x))
          ( linear-combination-tuple-left-module-Ring R M
            ( scalars-b)
            ( vectors-b))
        by
          ap
            ( λ y → add-left-module-Ring R M y
              ( linear-combination-tuple-left-module-Ring R M
                ( scalars-b)
                ( vectors-b)))
            ( commutative-add-left-module-Ring R M
              ( mul-left-module-Ring R M r x)
              ( linear-combination-tuple-left-module-Ring R M
                ( scalars-a)
                ( vectors-a)))
      ＝ add-left-module-Ring R M
          ( linear-combination-tuple-left-module-Ring R M
            ( r ∷ scalars-a)
            ( x ∷ vectors-a))
          ( linear-combination-tuple-left-module-Ring R M
            ( scalars-b)
            ( vectors-b))
        by refl

Recent changes