The terminals of matrix multiplication

• Distinct terminals (terminal_injective). The 3 n² terminals lie on distinct wires, where E i k is the matrix unit: the outputs C i k and C i' k' differ on A = 1, B = E i k; an input A i j and an output differ on A = E i j, B = 0; an input B j k and an output differ on A = 0, B = E j k.
• One component (mem_component_of_trace). The component of the output C 0 0 is closed, so it is crossed by no signal, and by apply_eq_zero_of_closed_of_trace the linear maps obtained by fixing one factor send vectors supported inside it to vectors vanishing outside it, and vice versa. With the factor B = E j k the unit vector at A i j moves the output C i k, and with A = E i j the unit vector at B j k moves C i k; spreading from C 0 0, the component holds the row A 0 ·, the row C 0 ·, all of B, all of C and all of A.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftLeft_single_single {n : ℕ} {F : Type u_1} [Field F] (i j k : Fin n) : shiftLeft (Matrix.single j k 1) (Pi.single (matMulLeft n i j) 1) (matMulOutput n i k) = 1

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.shiftRight_single_single {n : ℕ} {F : Type u_1} [Field F] (i j k : Fin n) : shiftRight (Matrix.single i j 1) (Pi.single (matMulRight n j k) 1) (matMulOutput n i k) = 1

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.out_injective {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] {p : Program σ (n * n + n * n) s} {I : Interpretation σ F} {out : Fin (n * n) → Wire (n * n + n * n) s} (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) : Function.Injective out

Distinct outputs lie on distinct wires.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.out_ne_termA {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] {p : Program σ (n * n + n * n) s} {I : Interpretation σ F} {out : Fin (n * n) → Wire (n * n + n * n) s} (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) (i j i' k' : Fin n) : out (matMulOutput n i' k') ≠ Wire.input (matMulLeft n i j)

No output lies on the wire of an input A i j.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.out_ne_termB {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] {p : Program σ (n * n + n * n) s} {I : Interpretation σ F} {out : Fin (n * n) → Wire (n * n + n * n) s} (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) (j k i' k' : Fin n) : out (matMulOutput n i' k') ≠ Wire.input (matMulRight n j k)

No output lies on the wire of an input B j k.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.terminal_injective {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] {p : Program σ (n * n + n * n) s} {I : Interpretation σ F} {out : Fin (n * n) → Wire (n * n + n * n) s} (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) : Function.Injective (Sum.elim (matMulTermA n s) (Sum.elim (matMulTermB n s) (matMulTermC out)))

Distinct terminals. The inputs A i j, B j k and the outputs C i k lie on 3 n² distinct wires.

One component

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.single_supported {F : Type u_1} [Field F] {N : ℕ} {x : Fin N} {P : Finset (Fin N)} (hx : x ∈ P) (y : Fin N) : y ∉ P → Pi.single x 1 y = 0

A unit vector is supported on any set containing its coordinate.

theorem Algebraic.Cutwidth.MultiOutput.MatMul.Internal.mem_component_of_trace {σ : Signature} {n s : ℕ} {F : Type u_1} [Field F] {p : Program σ (n * n + n * n) s} {I : Interpretation σ F} {out : Fin (n * n) → Wire (n * n + n * n) s} (hn : 0 < n) (hf : ∀ (z : Fin (n * n + n * n) → F) (o : Fin (n * n)), p.trace I z (out o) = matMul n z o) : (∀ (x : Fin (n * n + n * n)), Wire.input x ∈ component p (out (matMulOutput n ⟨0, hn⟩ ⟨0, hn⟩))) ∧ ∀ (o : Fin (n * n)), out o ∈ component p (out (matMulOutput n ⟨0, hn⟩ ⟨0, hn⟩))

All terminals lie in one component. If the wires out of a program over any field carry matMul n and n ≥ 1, the component of the output C 0 0 contains every input and every output.