Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Tensor.DirectSum

Binary sums of finite coefficient tensors #

The coordinate types of the summands may differ. The identities below give the explicit changes of coordinates needed for the tensor semiring, together with the block-diagonal restriction maps.

source
def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumTensor {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) :
Foundation.Tensor K (X ⊕ U) (Y ⊕ V) (Z ⊕ W)

The binary direct sum, with each of its three block labels retained.

Equations
Instances For
    source
    def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumRestriction {K : Type u_1} {X : Type u_2} {U : Type u_5} [CommSemiring K] {X' : Type u_11} {U' : Type u_12} (f : X' → X → K) (g : U' → U → K) :
    X' ⊕ U' → X ⊕ U → K

    The block-diagonal sum of two restriction matrices.

    Equations
    Instances For
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumTensor_restrict {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] {X' : Type u_11} {Y' : Type u_12} {Z' : Type u_13} {U' : Type u_14} {V' : Type u_15} {W' : Type u_16} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (f : X' → X → K) (g : Y' → Y → K) (h : Z' → Z → K) (f' : U' → U → K) (g' : V' → V → K) (h' : W' → W → K) (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) :
      Foundation.Tensor.restrict (sumRestriction f f') (sumRestriction g g') (sumRestriction h h') (sumTensor T S) = sumTensor (Foundation.Tensor.restrict f g h T) (Foundation.Tensor.restrict f' g' h' S)

      Independent restrictions of both summands give a restriction of the sum.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumTensor_comm {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) :
      Foundation.Tensor.pullback (⇑(Equiv.sumComm X U)) (⇑(Equiv.sumComm Y V)) (⇑(Equiv.sumComm Z W)) (sumTensor S T) = sumTensor T S

      Exchanging the two blocks is a coordinate permutation.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumTensor_assoc {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommSemiring K] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) (R : Foundation.Tensor K A B C) :
      Foundation.Tensor.pullback (⇑(Equiv.sumAssoc X U A)) (⇑(Equiv.sumAssoc Y V B)) (⇑(Equiv.sumAssoc Z W C)) (sumTensor T (sumTensor S R)) = sumTensor (sumTensor T S) R

      Reassociating the three blocks is a coordinate permutation.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumTensor_empty_right {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] [IsEmpty U] [IsEmpty V] [IsEmpty W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) :
      Foundation.Tensor.pullback (⇑(Equiv.sumEmpty X U).symm) (⇑(Equiv.sumEmpty Y V).symm) (⇑(Equiv.sumEmpty Z W).symm) (sumTensor T S) = T

      An empty right summand disappears under its canonical coordinates.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumTensor_empty_left {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] [IsEmpty X] [IsEmpty Y] [IsEmpty Z] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) :
      Foundation.Tensor.pullback (⇑(Equiv.emptySum X U).symm) (⇑(Equiv.emptySum Y V).symm) (⇑(Equiv.emptySum Z W).symm) (sumTensor T S) = S

      An empty left summand disappears under its canonical coordinates.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sumTensor_product {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommSemiring K] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) (R : Foundation.Tensor K A B C) :
      Foundation.Tensor.pullback (⇑(Equiv.sumProdDistrib X U A).symm) (⇑(Equiv.sumProdDistrib Y V B).symm) (⇑(Equiv.sumProdDistrib Z W C).symm) ((sumTensor T S).product R) = sumTensor (T.product R) (S.product R)

      Tensor product distributes over the first binary sum by coordinate permutation.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.product_sumTensor {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommSemiring K] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) (R : Foundation.Tensor K A B C) :
      Foundation.Tensor.pullback (⇑(Equiv.prodSumDistrib X U A).symm) (⇑(Equiv.prodSumDistrib Y V B).symm) (⇑(Equiv.prodSumDistrib Z W C).symm) (T.product (sumTensor S R)) = sumTensor (T.product S) (T.product R)

      Tensor product distributes over the second binary sum by coordinate permutation.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensorProduct_comm {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) :
      Foundation.Tensor.pullback (⇑(Equiv.prodComm X U)) (⇑(Equiv.prodComm Y V)) (⇑(Equiv.prodComm Z W)) (S.product T) = T.product S

      Exchanging product factors is a coordinate permutation.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensorProduct_assoc {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} {A : Type u_8} {B : Type u_9} {C : Type u_10} [CommSemiring K] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) (R : Foundation.Tensor K A B C) :
      Foundation.Tensor.pullback (⇑(Equiv.prodAssoc X U A)) (⇑(Equiv.prodAssoc Y V B)) (⇑(Equiv.prodAssoc Z W C)) (T.product (S.product R)) = (T.product S).product R

      Reassociating product factors is a coordinate permutation.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensorProduct_one_right {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] (T : Foundation.Tensor K X Y Z) :
      Foundation.Tensor.pullback (⇑(Equiv.prodPUnit X).symm) (⇑(Equiv.prodPUnit Y).symm) (⇑(Equiv.prodPUnit Z).symm) (T.product fun (x : PUnit.{u_11 + 1}) (x_1 : PUnit.{u_12 + 1}) (x_2 : PUnit.{u_13 + 1}) => 1) = T

      Scalar multiplication by one is the right unit for tensor product.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tensorProduct_one_left {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] (T : Foundation.Tensor K X Y Z) :
      Foundation.Tensor.pullback (⇑(Equiv.punitProd X).symm) (⇑(Equiv.punitProd Y).symm) (⇑(Equiv.punitProd Z).symm) (Foundation.Tensor.product (fun (x : PUnit.{u_11 + 1}) (x_1 : PUnit.{u_12 + 1}) (x_2 : PUnit.{u_13 + 1}) => 1) T) = T

      Scalar multiplication by one is the left unit for tensor product.