DirectSum.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

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.

def OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor line 22

Source documentation

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

def sumTensor (T : Tensor K X Y Z) (S : Tensor K U V W) :
    Tensor K (X ⊕ U) (Y ⊕ V) (Z ⊕ W)
  | .inl x, .inl y, .inl z => T x y z
  | .inr u, .inr v, .inr w => S u v w
  | _, _, _ => 0

/-- The block-diagonal sum of two restriction matrices. -/

def OAI.MatrixMultiplication.AuxiliarySeparation.sumRestriction line 29

Source documentation

The block-diagonal sum of two restriction matrices.

def sumRestriction {X' U' : Type*} (f : X' → X → K) (g : U' → U → K) :
    (X' ⊕ U') → (X ⊕ U) → K
  | .inl x', .inl x => f x' x
  | .inr u', .inr u => g u' u
  | _, _ => 0

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

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor_restrict line 36

Source documentation

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

theorem sumTensor_restrict
    {X' Y' Z' U' V' W' : Type*}
    [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 : Tensor K X Y Z) (S : Tensor K U V W) :
    Tensor.restrict (sumRestriction f f') (sumRestriction g g')
      (sumRestriction h h') (sumTensor T S) =
      sumTensor (Tensor.restrict f g h T) (Tensor.restrict f' g' h' S) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sumRestriction, OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor_comm line 50
Source documentation
Exchanging the two blocks is a coordinate permutation.
```
theorem sumTensor_comm (T : Tensor K X Y Z) (S : Tensor K U V W) :
    Tensor.pullback (Equiv.sumComm X U) (Equiv.sumComm Y V)
      (Equiv.sumComm Z W) (sumTensor S T) = sumTensor T S := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor_assoc line 57

Source documentation

Reassociating the three blocks is a coordinate permutation.

theorem sumTensor_assoc (T : Tensor K X Y Z) (S : Tensor K U V W)
    (R : Tensor K A B C) :
    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 := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor_empty_right line 68

Source documentation

An empty right summand disappears under its canonical coordinates.

theorem sumTensor_empty_right [IsEmpty U] [IsEmpty V] [IsEmpty W]
    (T : Tensor K X Y Z) (S : Tensor K U V W) :
    Tensor.pullback (Equiv.sumEmpty X U).symm (Equiv.sumEmpty Y V).symm
      (Equiv.sumEmpty Z W).symm (sumTensor T S) = T := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor_empty_left line 75

Source documentation

An empty left summand disappears under its canonical coordinates.

theorem sumTensor_empty_left [IsEmpty X] [IsEmpty Y] [IsEmpty Z]
    (T : Tensor K X Y Z) (S : Tensor K U V W) :
    Tensor.pullback (Equiv.emptySum X U).symm (Equiv.emptySum Y V).symm
      (Equiv.emptySum Z W).symm (sumTensor T S) = S := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor_product line 83

Source documentation

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

theorem sumTensor_product (T : Tensor K X Y Z) (S : Tensor K U V W)
    (R : Tensor K A B C) :
    Tensor.pullback (Equiv.sumProdDistrib X U A).symm
      (Equiv.sumProdDistrib Y V B).symm (Equiv.sumProdDistrib Z W C).symm
      (Tensor.product (sumTensor T S) R) =
      sumTensor (Tensor.product T R) (Tensor.product S R) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.product_sumTensor line 95

Source documentation

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

theorem product_sumTensor (T : Tensor K X Y Z) (S : Tensor K U V W)
    (R : Tensor K A B C) :
    Tensor.pullback (Equiv.prodSumDistrib X U A).symm
      (Equiv.prodSumDistrib Y V B).symm (Equiv.prodSumDistrib Z W C).symm
      (Tensor.product T (sumTensor S R)) =
      sumTensor (Tensor.product T S) (Tensor.product T R) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensorProduct_comm line 106

Source documentation

Exchanging product factors is a coordinate permutation.

theorem tensorProduct_comm (T : Tensor K X Y Z) (S : Tensor K U V W) :
    Tensor.pullback (Equiv.prodComm X U) (Equiv.prodComm Y V)
      (Equiv.prodComm Z W) (Tensor.product S T) = Tensor.product T S := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensorProduct_assoc line 113

Source documentation

Reassociating product factors is a coordinate permutation.

theorem tensorProduct_assoc (T : Tensor K X Y Z) (S : Tensor K U V W)
    (R : Tensor K A B C) :
    Tensor.pullback (Equiv.prodAssoc X U A) (Equiv.prodAssoc Y V B)
      (Equiv.prodAssoc Z W C) (Tensor.product T (Tensor.product S R)) =
      Tensor.product (Tensor.product T S) R := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensorProduct_one_right line 122

Source documentation

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

theorem tensorProduct_one_right (T : Tensor K X Y Z) :
    Tensor.pullback (Equiv.prodPUnit X).symm (Equiv.prodPUnit Y).symm
      (Equiv.prodPUnit Z).symm
      (Tensor.product T (fun (_ _ _ : PUnit) => (1 : K))) = T := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensorProduct_one_left line 130

Source documentation

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

theorem tensorProduct_one_left (T : Tensor K X Y Z) :
    Tensor.pullback (Equiv.punitProd X).symm (Equiv.punitProd Y).symm
      (Equiv.punitProd Z).symm
      (Tensor.product (fun (_ _ _ : PUnit) => (1 : K)) T) = T := by
…