Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum {K : Type u_1} {S : Type u_2} [CommSemiring K] [DecidableEq S] {X : S → Type u_3} {Y : S → Type u_4} {Z : S → Type u_5} (T : (s : S) → Tensor K (X s) (Y s) (Z s)) : Tensor K ((s : S) × X s) ((s : S) × Y s) ((s : S) × Z s)

Direct sum of tensors whose coordinate spaces may depend on the summand.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_matching {K : Type u_1} {S : Type u_2} [CommSemiring K] [DecidableEq S] {X : S → Type u_3} {Y : S → Type u_4} {Z : S → Type u_5} (T : (s : S) → Tensor K (X s) (Y s) (Z s)) (s : S) (x : X s) (y : Y s) (z : Z s) : dependentDirectSum T ⟨s, x⟩ ⟨s, y⟩ ⟨s, z⟩ = T s x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_zero_of_left_ne {K : Type u_1} {S : Type u_2} [CommSemiring K] [DecidableEq S] {X : S → Type u_3} {Y : S → Type u_4} {Z : S → Type u_5} (T : (s : S) → Tensor K (X s) (Y s) (Z s)) (x : (s : S) × X s) (y : (s : S) × Y s) (z : (s : S) × Z s) (h : x.fst ≠ y.fst) : dependentDirectSum T x y z = 0

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSumCoordinateEquiv {S : Type u_2} {X : S → Type u_3} {A : Type u_6} (e : (s : S) → X s ≃ A) : (s : S) × X s ≃ S × A

Replace summand-dependent coordinates by a common coordinate type using chosen equivalences.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_reindex {K : Type u_1} {S : Type u_2} [CommSemiring K] [DecidableEq S] {X : S → Type u_3} {Y : S → Type u_4} {Z : S → Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} (T : (s : S) → Tensor K (X s) (Y s) (Z s)) (ex : (s : S) → X s ≃ A) (ey : (s : S) → Y s ≃ B) (ez : (s : S) → Z s ≃ C) : pullback (⇑(directSumCoordinateEquiv ex).symm) (⇑(directSumCoordinateEquiv ey).symm) (⇑(directSumCoordinateEquiv ez).symm) (dependentDirectSum T) = directSum fun (s : S) => pullback (⇑(ex s).symm) (⇑(ey s).symm) (⇑(ez s).symm) (T s)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.labelFiberTensor {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} (lx : X → S) (ly : Y → S) (T : Tensor ℂ X Y Z) (s : S) : Tensor ℂ { x : X // lx x = s } { y : Y // ly y = s } Z

Restrict the first two tensor legs to fibers with a specified common label.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.labelFiberTensor lx ly T s x y z = T (↑x) (↑y) z

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.fiberCoordinateEquiv {X : Type u_1} {S : Type u_4} {U : Type u_5} (lx : X → S) : (s : S) × { x : X // lx x = s } × U ≃ X × U

Identify labelled fiber coordinates with the original coordinates and an auxiliary factor.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.tagCoordinateEquiv {Z : Type u_3} {S : Type u_4} : (_ : S) × Z × Unit ≃ Z × S

Exchange a summand tag and its tensor coordinate, removing a singleton factor.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_eq_fiber_directSum {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) : Tensor.pullback (⇑(fiberCoordinateEquiv lx)) (⇑(fiberCoordinateEquiv ly)) (⇑tagCoordinateEquiv) (separatedTensor lx T) = Tensor.dependentDirectSum fun (s : S) => (labelFiberTensor lx ly T s).product (Tensor.dotPairing U)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.fiber_directSum_eq_separatedTensor {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) : Tensor.pullback (⇑(fiberCoordinateEquiv lx).symm) (⇑(fiberCoordinateEquiv ly).symm) (⇑tagCoordinateEquiv.symm) (Tensor.dependentDirectSum fun (s : S) => (labelFiberTensor lx ly T s).product (Tensor.dotPairing U)) = separatedTensor lx T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_rankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) {r : ℕ} (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (h : (separatedTensor lx T).RankAtMost r) : (Tensor.dependentDirectSum fun (s : S) => (labelFiberTensor lx ly T s).product (Tensor.dotPairing U)).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_rankAtMost_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) {r : ℕ} (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) : (separatedTensor lx T).RankAtMost r ↔ (Tensor.dependentDirectSum fun (s : S) => (labelFiberTensor lx ly T s).product (Tensor.dotPairing U)).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_borderRankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) {r : ℕ} (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (h : (separatedTensor lx T).BorderRankAtMost r) : (Tensor.dependentDirectSum fun (s : S) => (labelFiberTensor lx ly T s).product (Tensor.dotPairing U)).BorderRankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_uniform_directSum_rankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] {A : Type u_6} {B : Type u_7} (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (ex : (s : S) → { x : X // lx x = s } ≃ A) (ey : (s : S) → { y : Y // ly y = s } ≃ B) {r : ℕ} (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (h : (separatedTensor lx T).RankAtMost r) : (Tensor.directSum fun (s : S) => Tensor.pullback (⇑((ex s).prodCongr (Equiv.refl U)).symm) (⇑((ey s).prodCongr (Equiv.refl U)).symm) (⇑(Equiv.refl (Z × Unit)).symm) ((labelFiberTensor lx ly T s).product (Tensor.dotPairing U))).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_localModels_identity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] {A : Type u_6} {B : Type u_7} {C : Type u_8} (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (fx : S → A → X) (fy : S → B → Y) (fz : S → C → Z) (hfx : ∀ (s : S) (a : A), lx (fx s a) = s) (hfy : ∀ (s : S) (b : B), ly (fy s b) = s) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) : Tensor.pullback (fun (x : S × A × U) => (fx x.1 x.2.1, x.2.2)) (fun (y : S × B × U) => (fy y.1 y.2.1, y.2.2)) (fun (z : S × C × Unit) => (fz z.1 z.2.1, z.1)) (separatedTensor lx T) = Tensor.directSum fun (s : S) => (Tensor.pullback (fx s) (fy s) (fz s) T).product (Tensor.dotPairing U)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_localModels_rankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] {A : Type u_6} {B : Type u_7} {C : Type u_8} (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (fx : S → A → X) (fy : S → B → Y) (fz : S → C → Z) (hfx : ∀ (s : S) (a : A), lx (fx s a) = s) (hfy : ∀ (s : S) (b : B), ly (fy s b) = s) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) {r : ℕ} (h : (separatedTensor lx T).RankAtMost r) : (Tensor.directSum fun (s : S) => (Tensor.pullback (fx s) (fy s) (fz s) T).product (Tensor.dotPairing U)).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_localModels_borderRankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] {A : Type u_6} {B : Type u_7} {C : Type u_8} (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (fx : S → A → X) (fy : S → B → Y) (fz : S → C → Z) (hfx : ∀ (s : S) (a : A), lx (fx s a) = s) (hfy : ∀ (s : S) (b : B), ly (fy s b) = s) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) {r : ℕ} (h : (separatedTensor lx T).BorderRankAtMost r) : (Tensor.directSum fun (s : S) => (Tensor.pullback (fx s) (fy s) (fz s) T).product (Tensor.dotPairing U)).BorderRankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_scalar_identity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (sx : S → X) (sy : S → Y) (sz : S → Z) (hsx : ∀ (s : S), lx (sx s) = s) (hsy : ∀ (s : S), ly (sy s) = s) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hscalar : ∀ (s : S), T (sx s) (sy s) (sz s) = 1) : Tensor.pullback (fun (x : S × U) => (sx x.1, x.2)) (fun (y : S × U) => (sy y.1, y.2)) (fun (z : S × Unit) => (sz z.1, z.1)) (separatedTensor lx T) = Tensor.directSum fun (x : S) => Tensor.dotPairing U

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_scalar_rankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (sx : S → X) (sy : S → Y) (sz : S → Z) (hsx : ∀ (s : S), lx (sx s) = s) (hsy : ∀ (s : S), ly (sy s) = s) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hscalar : ∀ (s : S), T (sx s) (sy s) (sz s) = 1) {r : ℕ} (h : (separatedTensor lx T).RankAtMost r) : (Tensor.directSum fun (x : S) => Tensor.dotPairing U).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor_scalar_borderRankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (sx : S → X) (sy : S → Y) (sz : S → Z) (hsx : ∀ (s : S), lx (sx s) = s) (hsy : ∀ (s : S), ly (sy s) = s) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hscalar : ∀ (s : S), T (sx s) (sy s) (sz s) = 1) {r : ℕ} (h : (separatedTensor lx T).BorderRankAtMost r) : (Tensor.directSum fun (x : S) => Tensor.dotPairing U).BorderRankAtMost r