Generalized Tensor Algebra and Dual View

This file develops the algebraic theory of the tensor product algebra A := R ⊗[K] C for arbitrary field extensions R/K and C/K, upon the existing TensorProduct module.

Main Definitions

• Basis.baseChangeRight : the lift of a basis of Left to an Right-basis of the base change Left ⊗[K] Right.

TODOs

• multilinear bases of tensor algebra over binary tower subfields
• Proximity Gap for Tensor Algebras

References

• [Lang, S., Algebra][Lan02]
• [Diamond, B.E. and Posen, J., Polylogarithmic Proofs for Multilinears over Binary Towers][DP24]
• [Diamond, B.E. and Posen, J., Succinct arguments over towers of binary fields][DP23]

noncomputable instance instCommSemiringTensorProduct_compPoly {K : Type u_1} {Left : Type u_2} {Right : Type u_3} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] : CommSemiring (TensorProduct K Left Right)

noncomputable instance instAlgebraTensorProduct_compPoly {K : Type u_1} {Left : Type u_2} {Right : Type u_3} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] : Algebra K (TensorProduct K Left Right)

noncomputable instance instAlgebraTensorProduct_compPoly_1 {K : Type u_1} {Left : Type u_2} {Right : Type u_3} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] : Algebra Left (TensorProduct K Left Right)

noncomputable instance instAlgebraTensorProduct_compPoly_2 {K : Type u_1} {Left : Type u_2} {Right : Type u_3} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] : Algebra Right (TensorProduct K Left Right)

theorem comm_map_smul_tmul {K : Type u_1} {Left : Type u_2} {Right : Type u_3} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (s s' : Right) (m : Left) : (Algebra.TensorProduct.comm K Right Left) (s • s' ⊗ₜ[K] m) = s • (Algebra.TensorProduct.comm K Right Left) (s' ⊗ₜ[K] m)

theorem comm_map_smul_add {K : Type u_1} {Left : Type u_2} {Right : Type u_3} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (s : Right) (x y : TensorProduct K Right Left) (hx : (Algebra.TensorProduct.comm K Right Left) (s • x) = s • (Algebra.TensorProduct.comm K Right Left) x) (hy : (Algebra.TensorProduct.comm K Right Left) (s • y) = s • (Algebra.TensorProduct.comm K Right Left) y) : (Algebra.TensorProduct.comm K Right Left) (s • x) + (Algebra.TensorProduct.comm K Right Left) (s • y) = s • (Algebra.TensorProduct.comm K Right Left) x + s • (Algebra.TensorProduct.comm K Right Left) y

noncomputable def commSEquiv {K : Type u_1} {Left : Type u_2} {Right : Type u_3} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] : TensorProduct K Right Left ≃ₗ[Right] TensorProduct K Left Right

A helper definition to package Algebra.TensorProduct.comm as an Right-linear equivalence. It takes the existing K-algebra equivalence and adds a proof that it is also Right-linear. We make the types explicit arguments to avoid type inference issues.

noncomputable def Basis.baseChangeRight {K : Type u_1} {Left : Type u_2} {Right : Type u_3} {ι : Type u_4} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (b : Module.Basis ι K Left) : Module.Basis ι Right (TensorProduct K Left Right)

The lift of an K-basis of Left to an Right-basis of the base change Left ⊗[K] Right. This is the right-sided counterpart to Basis.baseChange.

theorem Basis.baseChangeRight_repr_tmul {K : Type u_1} {Left : Type u_2} {Right : Type u_3} {ι : Type u_4} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (b : Module.Basis ι K Left) (x : Left) (y : Right) (i : ι) : ((baseChangeRight b).repr (x ⊗ₜ[K] y)) i = (b.repr x) i • y

@[simp]

theorem Basis.baseChangeRight_apply {K : Type u_1} {Left : Type u_2} {Right : Type u_3} {ι : Type u_4} [CommSemiring K] [CommSemiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (b : Module.Basis ι K Left) (i : ι) : (baseChangeRight b) i = b i ⊗ₜ[K] 1