Finite coefficient tensors and their algebraic transformations.

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor (K : Type u_1) (X : Type u_2) (Y : Type u_3) (Z : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A three-legged coefficient array over the given scalar type.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor K X Y Z = (X → Y → Z → K)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rankOne {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] (a : X → K) (b : Y → K) (c : Z → K) : Tensor K X Y Z

Tensor formed by multiplying one coefficient function from each leg.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rankOne a b c x y z = a x * b y * c z

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] (T : Tensor K X Y Z) (r : ℕ) : Prop

Existence of a decomposition as a sum of r rank-one tensors.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.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} [CommSemiring K] [Fintype X] [Fintype Y] [Fintype Z] (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (T : Tensor K X Y Z) : Tensor K X' Y' Z'

Apply a linear coordinate map independently to each of the three tensor legs.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict A B C T x' y' z' = ∑ x : X, ∑ y : Y, ∑ z : Z, A x' x * B y' y * C z' z * T x y z

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.contract {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] (T : Tensor K X Y Z) [Fintype X] [Fintype Y] (a : X → K) (b : Y → K) : Z → K

Contract the first two tensor legs against coefficient functions.

Equations

• T.contract a b z = ∑ x : X, ∑ y : Y, T x y z * a x * b y

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.product {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {U : Type u_8} {V : Type u_9} {W : Type u_10} (T : Tensor K X Y Z) (S : Tensor K U V W) : Tensor K (X × U) (Y × V) (Z × W)

Tensor product with paired coordinates on each of the three legs.

Equations

• T.product S x y z = T x.1 y.1 z.1 * S x.2 y.2 z.2

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] (T : ι → Tensor K X Y Z) : Tensor K (ι × X) (ι × Y) (ι × Z)

Block-diagonal direct sum retaining a common summand tag on all three legs.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum T x y z = if x.1 = y.1 ∧ x.1 = z.1 then T x.1 x.2 y.2 z.2 else 0

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.power {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] (T : Tensor K X Y Z) (n : ℕ) : Tensor K (Fin n → X) (Fin n → Y) (Fin n → Z)

The n-fold tensor product, indexed by words of length n on each leg.

Equations

• T.power n x y z = ∏ i : Fin n, T (x i) (y i) (z i)

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum_matching {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] (T : ι → Tensor K X Y Z) (i : ι) (x : X) (y : Y) (z : Z) : directSum T (i, x) (i, y) (i, z) = T i x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum_zero_of_left_ne {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] (T : ι → Tensor K X Y Z) (x : ι × X) (y : ι × Y) (z : ι × Z) (h : x.1 ≠ y.1) : directSum T x y z = 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rankAtMost_zero {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] : RankAtMost 0 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rankOne_rankAtMost {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] (a : X → K) (b : Y → K) (c : Z → K) : (rankOne a b c).RankAtMost 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.map {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {L : Type u_8} [CommSemiring L] (f : K →+* L) {T : Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) : RankAtMost (fun (x : X) (y : Y) (z : Z) => f (T x y z)) r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.scale {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {T : Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) (u : K) : RankAtMost (fun (x : X) (y : Y) (z : Z) => u * T x y z) r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rankAtMost_sum_rankOne {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [Fintype ι] (a : ι → X → K) (b : ι → Y → K) (c : ι → Z → K) : RankAtMost (fun (x : X) (y : Y) (z : Z) => ∑ i : ι, rankOne (a i) (b i) (c i) x y z) (Fintype.card ι)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.product {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {U : Type u_8} {V : Type u_9} {W : Type u_10} {T : Tensor K X Y Z} {S : Tensor K U V W} {r s : ℕ} (hT : T.RankAtMost r) (hS : S.RankAtMost s) : (T.product S).RankAtMost (r * s)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.power {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {T : Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) (n : ℕ) : (T.power n).RankAtMost (r ^ n)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict_rankOne {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] [Fintype X] [Fintype Y] [Fintype Z] (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (a : X → K) (b : Y → K) (c : Z → K) : restrict A B C (rankOne a b c) = rankOne (fun (x' : X') => ∑ x : X, A x' x * a x) (fun (y' : Y') => ∑ y : Y, B y' y * b y) fun (z' : Z') => ∑ z : Z, C z' z * c z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict_sum {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] [Fintype X] [Fintype Y] [Fintype Z] {ι : Type u_8} [Fintype ι] (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (T : ι → Tensor K X Y Z) : (restrict A B C fun (x : X) (y : Y) (z : Z) => ∑ i : ι, T i x y z) = fun (x' : X') (y' : Y') (z' : Z') => ∑ i : ι, restrict A B C (T i) x' y' z'

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.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} [CommSemiring K] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) : (Tensor.restrict A B C T).RankAtMost r

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pullback {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} (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) (T : Tensor K X Y Z) : Tensor K X' Y' Z'

Precompose each tensor coordinate with a map of its index set.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pullback fx fy fz T x y z = T (fx x) (fy y) (fz z)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.pullback_eq_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} [CommSemiring K] [Fintype X] [Fintype Y] [Fintype Z] [DecidableEq X] [DecidableEq Y] [DecidableEq Z] (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) (T : Tensor K X Y Z) : pullback fx fy fz T = restrict (fun (x' : X') (x : X) => if x = fx x' then 1 else 0) (fun (y' : Y') (y : Y) => if y = fy y' then 1 else 0) (fun (z' : Z') (z : Z) => if z = fz z' then 1 else 0) T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.pullback {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] {T : Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : (Tensor.pullback fx fy fz T).RankAtMost r

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (T : Tensor ℂ X Y Z) (r : ℕ) : Prop

Membership in the topological closure of tensors of rank at most r.

Equations

• T.BorderRankAtMost r = (T ∈ closure {S : MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor ℂ X Y Z | S.RankAtMost r})

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrictionOrbit {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) : Set (Tensor ℂ X' Y' Z')

Tensors obtainable by applying three linear coordinate maps to a fixed tensor.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.DegeneratesTo {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) (U : Tensor ℂ X' Y' Z') : Prop

Membership in the topological closure of a tensor's restriction orbit.

Equations

• T.DegeneratesTo U = (U ∈ closure T.restrictionOrbit)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.borderRankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Tensor ℂ X Y Z} {r : ℕ} (h : T.RankAtMost r) : T.BorderRankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.pullback {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} {T : Tensor ℂ X Y Z} {r : ℕ} (h : T.BorderRankAtMost r) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : (Tensor.pullback fx fy fz T).BorderRankAtMost r

Pulling back coordinates preserves border-rank bounds, without finiteness assumptions.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.continuous_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] (A : X' → X → ℂ) (B : Y' → Y → ℂ) (C : Z' → Z → ℂ) : Continuous (restrict A B C)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.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} {r : ℕ} (h : T.BorderRankAtMost r) (A : X' → X → ℂ) (B : Y' → Y → ℂ) (C : Z' → Z → ℂ) : (Tensor.restrict A B C T).BorderRankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.continuous_product_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_7} {V : Type u_8} {W : Type u_9} (S : Tensor ℂ U V W) : Continuous fun (T : Tensor ℂ X Y Z) => T.product S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.continuous_product_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_7} {V : Type u_8} {W : Type u_9} (T : Tensor ℂ X Y Z) : Continuous fun (S : Tensor ℂ U V W) => T.product S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.product {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_7} {V : Type u_8} {W : Type u_9} {T : Tensor ℂ X Y Z} {S : Tensor ℂ U V W} {r s : ℕ} (hT : T.BorderRankAtMost r) (hS : S.BorderRankAtMost s) : (T.product S).BorderRankAtMost (r * s)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.BorderRankAtMost.of_degeneration {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} {U : Tensor ℂ X' Y' Z'} {r : ℕ} (hT : T.BorderRankAtMost r) (hTU : T.DegeneratesTo U) : U.BorderRankAtMost r