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 ofLeftto anRight-basis of the base changeLeft ⊗[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]
@[implicit_reducible]
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)
@[implicit_reducible]
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)
@[implicit_reducible]
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)
@[implicit_reducible]
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]
:
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.
Instances For
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.
Instances For
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 : ι)
:
@[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 : ι)
: