Natural numbers and rank in the tensor semiring

The natural number r is the class of the diagonal scalar tensor with r terms. Consequently, comparison with r in the restriction order is exactly the existence of a rank decomposition with r terms.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.scalarTensor_add_reindex {K : Type} [Field K] (m n : ℕ) : Foundation.Tensor.pullback (⇑finSumFinEquiv) (⇑finSumFinEquiv) (⇑finSumFinEquiv) (scalarTensor K (m + n)) = sumTensor (scalarTensor K m) (scalarTensor K n)

Splitting the diagonal index set splits its scalar tensor into two blocks.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.scalarTensor_rankAtMost {K : Type} [Field K] (r : ℕ) : (scalarTensor K r).RankAtMost r

A diagonal scalar tensor has its evident decomposition into simple terms.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank_scalarTensor {K : Type} [Field K] (r : ℕ) : exactRank (scalarTensor K r) = r

The diagonal flattening also gives the matching lower bound.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor_add {K : Type} [Field K] (m n : ℕ) : classOf (scalarTensor K (m + n)) = classOf (scalarTensor K m) + classOf (scalarTensor K n)

Addition of the diagonal index sets is semiring addition.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor_zero {K : Type} [Field K] : classOf (scalarTensor K 0) = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor_one {K : Type} [Field K] : classOf (scalarTensor K 1) = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor {K : Type} [Field K] (r : ℕ) : classOf (scalarTensor K r) = ↑r

Natural numbers in the quotient semiring have their intended tensor meaning.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rankAtMost_iff_isRestriction_scalarTensor {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Finite X] [Finite Y] [Finite Z] (T : Foundation.Tensor K X Y Z) (r : ℕ) : T.RankAtMost r ↔ IsRestriction T (scalarTensor K r)

Exact rank decompositions are precisely restrictions of diagonal tensors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_le_nat_iff_rankAtMost {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) (r : ℕ) : classOf T ≤ ↑r ↔ T.RankAtMost r

The restriction order below a natural number is exactly the usual rank bound.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_natCast {K : Type} [Field K] (r : ℕ) : rank ↑r = r

Rank takes its usual value on natural numbers in the tensor semiring.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.le_rank {K : Type} [Field K] (T : TensorClass K) : T ≤ ↑(rank T)

The rank is a natural-number upper bound in the restriction order.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.natCast_le_natCast_iff {K : Type} [Field K] (m n : ℕ) : ↑m ≤ ↑n ↔ m ≤ n

The tensor restriction order induces the usual order on natural numbers.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.le_nat_mul_of_ne_zero {K : Type} [Field K] (T S : TensorClass K) (hS : S ≠ 0) : T ≤ ↑(rank T) * S

A natural multiple of any nonzero tensor contains any prescribed tensor by restriction.