Descent of exact tensor decompositions to a smaller field

Let E / P be a finite field extension of degree m. A decomposition of T ⊗_P E into R simple tensors over E gives one of T into m³ R simple tensors over P: expand every coefficient in a P-basis of E and apply a P-linear functional π : E → P with π 1 = 1.

A decomposition over an algebraic extension K / P only uses finitely many coefficients, which generate a finite subextension; this reduces the general algebraic case to the finite one.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.matMul_map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (a b c : ℕ) : (fun (x : Fin a × Fin b) (y : Fin b × Fin c) (z : Fin c × Fin a) => f (Foundation.Tensor.matMul R a b c x y z)) = Foundation.Tensor.matMul S a b c

The matrix multiplication tensor is defined over the prime ring: ring homomorphisms map it to itself.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.rankAtMost_matMul_pow {R : Type u_1} [CommSemiring R] {u r : ℕ} (h : (Foundation.Tensor.matMul R u u u).RankAtMost r) (j : ℕ) : (Foundation.Tensor.matMul R (u ^ j) (u ^ j) (u ^ j)).RankAtMost (r ^ j)

Tensor powers of ⟨u,u,u⟩ are ⟨u^j,u^j,u^j⟩, so rank is submultiplicative along powers, over any coefficient semiring.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.exists_functional_one {P : Type u_1} {E : Type u_2} [Field P] [Field E] [Algebra P E] : ∃ (π : E →ₗ[P] P), π 1 = 1

A P-linear functional on E that is the identity on P.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.functional_mul_mul_eq_sum {P : Type u_1} {E : Type u_2} [Field P] [Field E] [Algebra P E] {ι : Type u_3} [Fintype ι] (bs : Module.Basis ι P E) (π : E →ₗ[P] P) (e₁ e₂ e₃ : E) : π (e₁ * e₂ * e₃) = ∑ w : ι, ∑ t : ι, ∑ s : ι, (bs.repr e₁) s * (bs.repr e₂) t * (bs.repr e₃) w * π (bs s * bs t * bs w)

A trilinear expansion of π (e₁ e₂ e₃) in a basis.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.rankAtMost_of_map {P : Type u_1} {E : Type u_2} [Field P] [Field E] [Algebra P E] [FiniteDimensional P E] {X : Type u_3} {Y : Type u_4} {Z : Type u_5} {T : Foundation.Tensor P X Y Z} {R : ℕ} (h : Foundation.Tensor.RankAtMost (fun (x : X) (y : Y) (z : Z) => (algebraMap P E) (T x y z)) R) : T.RankAtMost (Module.finrank P E ^ 3 * R)

Descent. If T has coefficients in P and T ⊗ E has rank at most R over a finite extension E / P of degree m, then T has rank at most m³ R over P.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.exists_finiteDimensional_rankAtMost {P : Type u_1} {K : Type u_2} [Field P] [Field K] [Algebra P K] [Algebra.IsAlgebraic P K] {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [Finite X] [Finite Y] [Finite Z] {T : Foundation.Tensor P X Y Z} {R : ℕ} (h : Foundation.Tensor.RankAtMost (fun (x : X) (y : Y) (z : Z) => (algebraMap P K) (T x y z)) R) : ∃ (E : IntermediateField P K), FiniteDimensional P ↥E ∧ Foundation.Tensor.RankAtMost (fun (x : X) (y : Y) (z : Z) => (algebraMap P ↥E) (T x y z)) R

A decomposition over an algebraic extension K / P uses finitely many coefficients; they generate a finite-dimensional intermediate field E, over which the same decomposition already exists.