Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.composeRestrictionMatrix {K : Type u_1} {X : Type u_2} {X' : Type u_5} {X'' : Type u_8} [CommSemiring K] [Fintype X'] (D : X'' → X' → K) (A : X' → X → K) : X'' → X → K

Matrix composition for two consecutive linear restrictions of one tensor leg.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.composeRestrictionMatrix D A x'' x = ∑ x' : X', D x'' x' * A x' x

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict_restrict {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} {X'' : Type u_8} {Y'' : Type u_9} {Z'' : Type u_10} [CommSemiring K] [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (D : X'' → X' → K) (E : Y'' → Y' → K) (F : Z'' → Z' → K) (T : Tensor K X Y Z) : restrict D E F (restrict A B C T) = restrict (composeRestrictionMatrix D A) (composeRestrictionMatrix E B) (composeRestrictionMatrix F C) T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict_product {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [CommSemiring K] {U : Type u_11} {V : Type u_12} {W : 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] (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (D : U' → U → K) (E : V' → V → K) (F : W' → W → K) (T : Tensor K X Y Z) (S : Tensor K U V W) : restrict (fun (x : X' × U') (u : X × U) => A x.1 u.1 * D x.2 u.2) (fun (y : Y' × V') (v : Y × V) => B y.1 v.1 * E y.2 v.2) (fun (z : Z' × W') (w : Z × W) => C z.1 w.1 * F z.2 w.2) (T.product S) = (restrict A B C T).product (restrict D E F S)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict_identity {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] [Fintype X] [Fintype Y] [Fintype Z] [DecidableEq X] [DecidableEq Y] [DecidableEq Z] (T : Tensor K X Y Z) : restrict (fun (x' x : X) => if x = x' then 1 else 0) (fun (y' y : Y) => if y = y' then 1 else 0) (fun (z' z : Z) => if z = z' then 1 else 0) T = T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.degeneratesTo_restrict {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] (T : Tensor ℂ X Y Z) (A : X' → X → ℂ) (B : Y' → Y → ℂ) (C : Z' → Z → ℂ) : T.DegeneratesTo (restrict A B C T)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.refl {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Tensor ℂ X Y Z) : T.DegeneratesTo T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.mem_restrictionOrbit_restrict {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} {X'' : Type u_7} {Y'' : Type u_8} {Z'' : Type u_9} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] {T : Tensor ℂ X Y Z} {U : Tensor ℂ X' Y' Z'} (h : U ∈ T.restrictionOrbit) (D : X'' → X' → ℂ) (E : Y'' → Y' → ℂ) (F : Z'' → Z' → ℂ) : restrict D E F U ∈ T.restrictionOrbit

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.restrict {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} {X'' : Type u_7} {Y'' : Type u_8} {Z'' : Type u_9} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] {T : Tensor ℂ X Y Z} {U : Tensor ℂ X' Y' Z'} (h : T.DegeneratesTo U) (D : X'' → X' → ℂ) (E : Y'' → Y' → ℂ) (F : Z'' → Z' → ℂ) : T.DegeneratesTo (Tensor.restrict D E F U)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} {X'' : Type u_7} {Y'' : Type u_8} {Z'' : Type u_9} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] {T : Tensor ℂ X Y Z} {U : Tensor ℂ X' Y' Z'} {V : Tensor ℂ X'' Y'' Z''} (hTU : T.DegeneratesTo U) (hUV : U.DegeneratesTo V) : T.DegeneratesTo V

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo.of_restrict {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} {X'' : Type u_7} {Y'' : Type u_8} {Z'' : Type u_9} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] {T : Tensor ℂ X Y Z} {V : Tensor ℂ X'' Y'' Z''} (A : X' → X → ℂ) (B : Y' → Y → ℂ) (C : Z' → Z → ℂ) (h : (Tensor.restrict A B C T).DegeneratesTo V) : T.DegeneratesTo V