Characters of finite tensors over K

The tensor operations in this file are the coefficient operations from MatrixMultiplication.Foundation.Tensor. A character is an assumption on those operations, not an assertion that a character exists. Restriction monotonicity forces invariance under independent invertible changes of coordinates, so this interface descends to the mutual-restriction classes of Section 3 of the paper.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.unitTensor (K : Type) [Field K] : Foundation.Tensor K PUnit.{u_1 + 1} PUnit.{u_2 + 1} PUnit.{u_3 + 1}

The scalar multiplication tensor, the multiplicative unit.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.unitTensor K x✝² x✝¹ x✝ = 1

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.scalarTensor (K : Type) [Field K] (r : ℕ) : Foundation.Tensor K (Fin r) (Fin r) (Fin r)

The direct sum of r scalar multiplication tensors, in diagonal coordinates.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.scalarTensor K r i j k = if i = j ∧ i = k then 1 else 0

structure MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character (K : Type) [Field K] : Type 1

A normalized, additive, multiplicative, restriction-monotone tensor valuation.

Index types vary over all finite types in Type. No character-existence result is included among the fields or claimed by this definition.

• value {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] : Foundation.Tensor K X Y Z → ℝ

  The nonnegative real value assigned to a finite tensor by the character.

• nonneg {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : 0 ≤ self.value T
• map_zero {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] : self.value 0 = 0
• map_one : self.value (unitTensor K) = 1
• map_directSum {ι X Y Z : Type} [Fintype ι] [DecidableEq ι] [Fintype X] [Fintype Y] [Fintype Z] (T : ι → Foundation.Tensor K X Y Z) : self.value (Foundation.Tensor.directSum T) = ∑ i : ι, self.value (T i)
• map_product {X Y Z U V W : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : self.value (T.product S) = self.value T * self.value S
• monotone {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (T : Foundation.Tensor K X Y Z) (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) : self.value (Foundation.Tensor.restrict A B C T) ≤ self.value T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_pullback_le {K : Type} [Field K] (χ : Character K) {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (T : Foundation.Tensor K X Y Z) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : χ.value (Foundation.Tensor.pullback fx fy fz T) ≤ χ.value T

Coordinate pullbacks are restrictions.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_reindex {K : Type} [Field K] (χ : Character K) {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (T : Foundation.Tensor K X Y Z) (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) : χ.value (Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) T) = χ.value T

Independent coordinate bijections preserve a character.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_eq_of_mutual_restriction {K : Type} [Field K] (χ : Character K) {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K X' Y' Z') (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (A' : X → X' → K) (B' : Y → Y' → K) (C' : Z → Z' → K) (hS : S = Foundation.Tensor.restrict A B C T) (hT : T = Foundation.Tensor.restrict A' B' C' S) : χ.value T = χ.value S

The character has the same value on mutually restricting tensors.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_scalarTensor {K : Type} [Field K] (χ : Character K) (r : ℕ) : χ.value (scalarTensor K r) = ↑r

An integer scalar tensor has its expected character value.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.restrict_scalarTensor {K : Type} [Field K] {X Y Z : Type} (r : ℕ) (a : Fin r → X → K) (b : Fin r → Y → K) (c : Fin r → Z → K) : Foundation.Tensor.restrict (fun (x : X) (i : Fin r) => a i x) (fun (y : Y) (i : Fin r) => b i y) (fun (z : Z) (i : Fin r) => c i z) (scalarTensor K r) = fun (x : X) (y : Y) (z : Z) => ∑ i : Fin r, Foundation.Tensor.rankOne (a i) (b i) (c i) x y z

Restricting a diagonal scalar tensor realizes a rank decomposition.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_le_rank {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) : χ.value T ≤ ↑r

Character values are bounded by every exact rank decomposition size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.one_le_value {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} (hT : T ≠ 0) : 1 ≤ χ.value T

Every nonzero tensor restricts to the scalar multiplication tensor.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_eq_zero_iff {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : χ.value T = 0 ↔ T = 0

Normalization and restriction monotonicity make the character faithful.