Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixX (U : Type u_2) : Unit × U ≃ U

Remove the singleton factor from the first leg of a dot-pairing matrix tensor.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixX U = { toFun := fun (x : Unit × U) => x.2, invFun := fun (x : U) => ((), x), left_inv := ⋯, right_inv := ⋯ }

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixY (U : Type u_2) : U × Unit ≃ U

Remove the singleton factor from the second leg of a dot-pairing matrix tensor.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixY U = { toFun := fun (y : U × Unit) => y.1, invFun := fun (y : U) => (y, ()), left_inv := ⋯, right_inv := ⋯ }

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixZ : Unit × Unit ≃ Unit

Identify the singleton third-leg coordinate spaces of the dot-pairing matrix tensor.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairing_matrixCoefficients {K : Type u_1} [CommSemiring K] (U : Type u_2) [DecidableEq U] : pullback (⇑(dotPairingMatrixX U)) (⇑(dotPairingMatrixY U)) (⇑dotPairingMatrixZ) (dotPairing U) = matrixCoefficients Unit U Unit

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_dotPairing {K : Type u_1} [CommSemiring K] {U : Type u_2} [DecidableEq U] {r : ℕ} (h : (dotPairing U).RankAtMost r) : (matrixCoefficients Unit U Unit).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_borderRank_of_dotPairing {U : Type u_2} [DecidableEq U] {r : ℕ} (h : (dotPairing U).BorderRankAtMost r) : (matrixCoefficients Unit U Unit).BorderRankAtMost r

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pairingTriple {K : Type u_1} [CommSemiring K] (A : Type u_2) (B : Type u_3) (C : Type u_4) [DecidableEq A] [DecidableEq B] [DecidableEq C] : Tensor K ((B × A) × Unit) ((B × Unit) × C) ((Unit × A) × C)

Product of three cyclically positioned dot-pairing tensors.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pairingTripleMatrixX (A : Type u_2) (B : Type u_3) : A × B ≃ (B × A) × Unit

Reindex the first matrix-coordinate pair for the triple dot-pairing representation.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pairingTripleMatrixY (B : Type u_2) (C : Type u_3) : B × C ≃ (B × Unit) × C

Reindex the second matrix-coordinate pair for the triple dot-pairing representation.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pairingTripleMatrixZ (C : Type u_2) (A : Type u_3) : C × A ≃ (Unit × A) × C

Reindex the third matrix-coordinate pair for the triple dot-pairing representation.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pairingTriple_matrixCoefficients {K : Type u_1} [CommSemiring K] {A : Type u_2} {B : Type u_3} {C : Type u_4} [DecidableEq A] [DecidableEq B] [DecidableEq C] : pullback (⇑(pairingTripleMatrixX A B)) (⇑(pairingTripleMatrixY B C)) (⇑(pairingTripleMatrixZ C A)) (pairingTriple A B C) = matrixCoefficients A B C

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_pairingTriple {K : Type u_1} [CommSemiring K] {A : Type u_2} {B : Type u_3} {C : Type u_4} [DecidableEq A] [DecidableEq B] [DecidableEq C] {r : ℕ} (h : (pairingTriple A B C).RankAtMost r) : (matrixCoefficients A B C).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_borderRank_of_pairingTriple {A : Type u_2} {B : Type u_3} {C : Type u_4} [DecidableEq A] [DecidableEq B] [DecidableEq C] {r : ℕ} (h : (pairingTriple A B C).BorderRankAtMost r) : (matrixCoefficients A B C).BorderRankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_pairingTriple {K : Type u_1} [CommSemiring K] {A : Type u_2} {B : Type u_3} {C : Type u_4} [DecidableEq A] [DecidableEq B] [DecidableEq C] {ι : Type u_5} [DecidableEq ι] {r : ℕ} (h : (directSum fun (x : ι) => pairingTriple A B C).RankAtMost r) : (directSum fun (x : ι) => matrixCoefficients A B C).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_borderRank_of_pairingTriple {A : Type u_2} {B : Type u_3} {C : Type u_4} [DecidableEq A] [DecidableEq B] [DecidableEq C] {ι : Type u_5} [DecidableEq ι] {r : ℕ} (h : (directSum fun (x : ι) => pairingTriple A B C).BorderRankAtMost r) : (directSum fun (x : ι) => matrixCoefficients A B C).BorderRankAtMost r