Coordinates of matrix multiplication

• The coordinates matMulLeft n i j and matMulRight n j k are distinct and cover all inputs (sum_input); the outputs matMulOutput n i k cover all outputs (sum_output).
• matMul_output and matMul_matMulInput: the map multiplies matrices.
• Fixing a factor. With the second factor fixed to B₀, the product changes by shiftLeft B₀ d, whose output C i k is ∑ j, d (A i j) B₀ j k (matMul_sub_left); symmetrically with the first factor fixed (matMul_sub_right). The free coordinates are leftCoords n and rightCoords n.
• The quadratic form. For a matrix Λ, bilinForm Λ is the matrix of the quadratic form z ↦ ∑ i k, Λ i k C i k (quadForm_bilinForm). Its symmetrization H = M + Mᵀ pairs A i j with B j k through Λ i k (mulVec_add_transpose_left, mulVec_add_transpose_right).

Distinct coordinates

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulLeft_inj {n : ℕ} {i j i' j' : Fin n} : matMulLeft n i j = matMulLeft n i' j' ↔ i = i' ∧ j = j'

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulRight_inj {n : ℕ} {j k j' k' : Fin n} : matMulRight n j k = matMulRight n j' k' ↔ j = j' ∧ k = k'

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulLeft_ne_matMulRight {n : ℕ} (i j j' k : Fin n) : matMulLeft n i j ≠ matMulRight n j' k

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulOutput_inj {n : ℕ} {i k i' k' : Fin n} : matMulOutput n i k = matMulOutput n i' k' ↔ i = i' ∧ k = k'

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.input_cases {n : ℕ} (x : Fin (n * n + n * n)) : (∃ (i : Fin n) (j : Fin n), x = matMulLeft n i j) ∨ ∃ (j : Fin n) (k : Fin n), x = matMulRight n j k

Every input coordinate holds an entry of one of the factors.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.output_eq {n : ℕ} (o : Fin (n * n)) : o = matMulOutput n (finProdFinEquiv.symm o).1 (finProdFinEquiv.symm o).2

Every output coordinate holds an entry of the product.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_input {n : ℕ} {M : Type u_1} [AddCommMonoid M] (φ : Fin (n * n + n * n) → M) : ∑ x : Fin (n * n + n * n), φ x = ∑ i : Fin n, ∑ j : Fin n, φ (matMulLeft n i j) + ∑ j : Fin n, ∑ k : Fin n, φ (matMulRight n j k)

A sum over the input coordinates is a sum over the entries of the two factors.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.sum_output {n : ℕ} {M : Type u_1} [AddCommMonoid M] (φ : Fin (n * n) → M) : ∑ o : Fin (n * n), φ o = ∑ i : Fin n, ∑ k : Fin n, φ (matMulOutput n i k)

A sum over the output coordinates is a sum over the entries of the product.

The product

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMul_output {n : ℕ} {R : Type u_1} [Semiring R] (z : Fin (n * n + n * n) → R) (i k : Fin n) : matMul n z (matMulOutput n i k) = ∑ j : Fin n, z (matMulLeft n i j) * z (matMulRight n j k)

@[simp]

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulInput_left {n : ℕ} {R : Type u_1} (A B : Matrix (Fin n) (Fin n) R) (i j : Fin n) : matMulInput A B (matMulLeft n i j) = A i j

@[simp]

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulInput_right {n : ℕ} {R : Type u_1} (A B : Matrix (Fin n) (Fin n) R) (j k : Fin n) : matMulInput A B (matMulRight n j k) = B j k

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMul_matMulInput {n : ℕ} {R : Type u_1} [Semiring R] (A B : Matrix (Fin n) (Fin n) R) (i k : Fin n) : matMul n (matMulInput A B) (matMulOutput n i k) = (A * B) i k

matMul multiplies.

Fixing one factor

def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.leftCoords (n : ℕ) : Finset (Fin (n * n + n * n))

The coordinates of the first factor.

Equations

• Algebraic.Cutwidth.MultiOutput.MatMul.Internal.leftCoords n = Finset.image (fun (p : Fin n × Fin n) => Algebraic.Cutwidth.MultiOutput.matMulLeft n p.1 p.2) Finset.univ

def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.rightCoords (n : ℕ) : Finset (Fin (n * n + n * n))

The coordinates of the second factor.

Equations

• Algebraic.Cutwidth.MultiOutput.MatMul.Internal.rightCoords n = Finset.image (fun (p : Fin n × Fin n) => Algebraic.Cutwidth.MultiOutput.matMulRight n p.1 p.2) Finset.univ

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulLeft_mem_leftCoords {n : ℕ} (i j : Fin n) : matMulLeft n i j ∈ leftCoords n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulRight_mem_rightCoords {n : ℕ} (j k : Fin n) : matMulRight n j k ∈ rightCoords n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulRight_notMem_leftCoords {n : ℕ} (j k : Fin n) : matMulRight n j k ∉ leftCoords n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMulLeft_notMem_rightCoords {n : ℕ} (i j : Fin n) : matMulLeft n i j ∉ rightCoords n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_leftCoords {n : ℕ} : (leftCoords n).card = n * n

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.card_rightCoords {n : ℕ} : (rightCoords n).card = n * n

def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftLeft {n : ℕ} {R : Type u_1} [CommRing R] (B₀ : Matrix (Fin n) (Fin n) R) (d : Fin (n * n + n * n) → R) : Fin (n * n) → R

The change of the product when the input changes by d and the second factor is B₀.

Equations

• Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftLeft B₀ d o = ∑ j : Fin n, d (Algebraic.Cutwidth.MultiOutput.matMulLeft n (finProdFinEquiv.symm o).1 j) * B₀ j (finProdFinEquiv.symm o).2

def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftRight {n : ℕ} {R : Type u_1} [CommRing R] (A₀ : Matrix (Fin n) (Fin n) R) (d : Fin (n * n + n * n) → R) : Fin (n * n) → R

The change of the product when the input changes by d and the first factor is A₀.

Equations

• Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftRight A₀ d o = ∑ j : Fin n, A₀ (finProdFinEquiv.symm o).1 j * d (Algebraic.Cutwidth.MultiOutput.matMulRight n j (finProdFinEquiv.symm o).2)

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftLeft_output {n : ℕ} {R : Type u_1} [CommRing R] (B₀ : Matrix (Fin n) (Fin n) R) (d : Fin (n * n + n * n) → R) (i k : Fin n) : shiftLeft B₀ d (matMulOutput n i k) = ∑ j : Fin n, d (matMulLeft n i j) * B₀ j k

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftRight_output {n : ℕ} {R : Type u_1} [CommRing R] (A₀ : Matrix (Fin n) (Fin n) R) (d : Fin (n * n + n * n) → R) (i k : Fin n) : shiftRight A₀ d (matMulOutput n i k) = ∑ j : Fin n, A₀ i j * d (matMulRight n j k)

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMul_sub_left {n : ℕ} {R : Type u_1} [CommRing R] (B₀ : Matrix (Fin n) (Fin n) R) (z z' : Fin (n * n + n * n) → R) (hz : ∀ x ∉ leftCoords n, z x = matMulInput 0 B₀ x) (hz' : ∀ x ∉ leftCoords n, z' x = matMulInput 0 B₀ x) : matMul n z' - matMul n z = shiftLeft B₀ (z' - z)

With the second factor fixed to B₀, the product changes by shiftLeft B₀.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.matMul_sub_right {n : ℕ} {R : Type u_1} [CommRing R] (A₀ : Matrix (Fin n) (Fin n) R) (z z' : Fin (n * n + n * n) → R) (hz : ∀ x ∉ rightCoords n, z x = matMulInput A₀ 0 x) (hz' : ∀ x ∉ rightCoords n, z' x = matMulInput A₀ 0 x) : matMul n z' - matMul n z = shiftRight A₀ (z' - z)

With the first factor fixed to A₀, the product changes by shiftRight A₀.

The quadratic form

def Algebraic.Cutwidth.MultiOutput.MatMul.Internal.bilinForm {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) : Matrix (Fin (n * n + n * n)) (Fin (n * n + n * n)) R

The matrix of the quadratic form z ↦ ∑ i k, Λ i k C i k: it pairs the entry A i j with the entry B j k through Λ i k, and has no other nonzero entries.

Equations

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

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.bilinForm_left_right {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (i j j' k : Fin n) : bilinForm Λ (matMulLeft n i j) (matMulRight n j' k) = if j = j' then Λ i k else 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.bilinForm_left_left {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (i j i' j' : Fin n) : bilinForm Λ (matMulLeft n i j) (matMulLeft n i' j') = 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.bilinForm_right {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (j k : Fin n) (y : Fin (n * n + n * n)) : bilinForm Λ (matMulRight n j k) y = 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.mulVec_bilinForm_left {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (z : Fin (n * n + n * n) → R) (i j : Fin n) : (bilinForm Λ).mulVec z (matMulLeft n i j) = ∑ k : Fin n, Λ i k * z (matMulRight n j k)

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.mulVec_bilinForm_right {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (z : Fin (n * n + n * n) → R) (j k : Fin n) : (bilinForm Λ).mulVec z (matMulRight n j k) = 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.mulVec_transpose_bilinForm_left {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (z : Fin (n * n + n * n) → R) (i j : Fin n) : (bilinForm Λ).transpose.mulVec z (matMulLeft n i j) = 0

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.mulVec_transpose_bilinForm_right {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (z : Fin (n * n + n * n) → R) (j k : Fin n) : (bilinForm Λ).transpose.mulVec z (matMulRight n j k) = ∑ i : Fin n, Λ i k * z (matMulLeft n i j)

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.mulVec_add_transpose_left {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (z : Fin (n * n + n * n) → R) (i j : Fin n) : (bilinForm Λ + (bilinForm Λ).transpose).mulVec z (matMulLeft n i j) = ∑ k : Fin n, Λ i k * z (matMulRight n j k)

The symmetrized form at A i j.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.mulVec_add_transpose_right {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (z : Fin (n * n + n * n) → R) (j k : Fin n) : (bilinForm Λ + (bilinForm Λ).transpose).mulVec z (matMulRight n j k) = ∑ i : Fin n, Λ i k * z (matMulLeft n i j)

The symmetrized form at B j k.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.quadForm_bilinForm {n : ℕ} {R : Type u_1} [CommRing R] (Λ : Matrix (Fin n) (Fin n) R) (z : Fin (n * n + n * n) → R) : quadForm (bilinForm Λ) z = ∑ i : Fin n, ∑ k : Fin n, Λ i k * matMul n z (matMulOutput n i k)

The quadratic form of bilinForm Λ is the combination ∑ i k, Λ i k C i k of the outputs.