Tensor Product

Stream: Is there code for X?

[Antoine Chambert-Loir]

I know how to prove this (I did it for polynomial in several variables, so I just need to copy that), but I would have preferred avoiding that. Does anybody have an idea of how to prove this easily within mathlib?

example (R S N : Type*) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommGroup N] [Module R N] :
    S[X] ⊗[R] N ≃ₗ[S] (ℕ →₀ S ⊗[R] N) := by sorry

(By the way, if mathlib knew what N[X] were, this would do most of the job…)

[Eric Wieser]

I think we're missing the Finsupp version of docs#TensorProduct.directSumLeft

[Eric Wieser]

From which that is a trivial consequence since polynomials are finsupps almost by definition

[Antoine Chambert-Loir]

wait, DirectSum isn't a Finsupp?

[Eric Wieser]

No, it's a DFinsupp

[Eric Wieser]

Because the pieces might be different types

[Eric Wieser]

Arguably we could try just dropping Finsupp altogether and using Dfinsupp everywhere, but that is a massive refactor

[Eric Wieser]

We do at least have that the two are isomorphic in the non-dependent case

[Antoine Chambert-Loir]

I'll write the Finsuppstuff and PR it… (Maybe one can rewrite Finsupp to DFinsupp and that's it!?)

[Eric Wieser]

Antoine Chambert-Loir said:

(Maybe one can rewrite Finsupp to DFinsupp and that's it!?)

If you mean for adding those results, probably yes. If you mean for merging the two into one; not a chance!

[Antoine Chambert-Loir]

I proved the various equiv I needed, I'll PR it this morning. You will probably have some comments to add. Basically, the definitions are :

variable {R M N : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]

section Finsupp

variable {ι : Type*} [DecidableEq ι]

noncomputable def Finsupp.tensorProductLeft :
    (ι →₀ M) ⊗[R] N ≃ₗ[R] ι →₀ (M ⊗[R] N) := sorry

-- variant for right

variable {S : Type*} [CommSemiring S] [Algebra R S]  [Module S M] [IsScalarTower R S M]

noncomputable def Finsupp.tensorProductLeft' :
    (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ (M ⊗[R] N) := sorry

end Finsupp

section MvPolynomial

variable (σ : Type u) [DecidableEq σ]

variable {S : Type*} [CommSemiring S] [Algebra R S]

noncomputable def MvPolynomial.tensorProductRight' :
    MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) := sorry

end MvPolynomial

section Polynomial

noncomputable def Polynomial.tensorProductRight :
    R[X] ⊗[R] N ≃ₗ[R] ℕ →₀ N := sorry

variable (S : Type*) [CommSemiring S] [Algebra R S]

def Polynomial.toFinsuppLinearEquiv :
    S[X] ≃ₗ[S] (ℕ →₀ S)

variable {S} (P : Type*) (e : M ≃ₗ[R] N) [AddCommMonoid P] [Module R P

noncomputable def LinearEquiv.rTensor  (e : M ≃ₗ[R] N) :
    M ⊗[R] P ≃ₗ[R] N ⊗[R] P := sorry

noncomputable def Polynomial.tensorProductRight' :
    Polynomial S ⊗[R] N ≃ₗ[S] ℕ →₀ (S ⊗[R] N) := sorry

[Eric Wieser]

At a glance those look reasonable; I assume you're aware we already have the version with a Finsupp on both sides of the tensor product?

[Eric Wieser]

It might be nice to extract an intermediate AddMonoidAlgebra version too, along the lines of

noncomputable def Polynomial.tensorProductRight' :
    AddMonoidAlgebra S A ⊗[R] N ≃ₗ[S] AddMonoidAlgebar (S ⊗[R] N) A := sorry

which might even be true as an AlgHom

[Eric Wieser]

Oh, I guess that only makes sense when N is an algebra

[Antoine Chambert-Loir]

Eric Wieser said:

At a glance those look reasonable; I assume you're aware we already have the version with a Finsupp on both sides of the tensor product?

I saw that, and I changed my proofs accordingly, except that the proof of docs#finsuppTensorFinsupp_apply is bizarrely complicated, and I try to fix that.
(Also, I generalized to CommSemiring, etc.)

[Antoine Chambert-Loir]

Also : I believe we miss finsupp_sum_tmul and finsupp_tmul_sum…

[Antoine Chambert-Loir]

(Well, what I wrote was proved by simp [Finsupp.sum, sum_tmul], so it's not a necessary addition.)

[Antoine Chambert-Loir]

Another question :
docs#TensorProduct.congr, docs#TensorProduct.map and docs#rTensor provide a linear equiv / a linear map between tensor products, but when the modules on the left have additional actions, then so do the tensor products, and the maps defined have extra linearity.
How should this be phrased? What do you think of this :

variable {R S M N : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
  [AddCommMonoid M]  [Module R M] [Module S M] [IsScalarTower R S M]
  [AddCommMonoid N] [Module R M] [Module S N] [IsScalarTower R S N]

variable (foo : LinearMap R M N)

lemma foo_isLinearMap'  : IsLinearMap S foo := by sorry

def foo' : LinearMap S M N := {
  foo with
  map_smul := (foo_isLinearMap' foo).map_smul }

[Antoine Chambert-Loir]

Eric Wieser said:

It might be nice to extract an intermediate AddMonoidAlgebra version too, along the lines of

noncomputable def Polynomial.tensorProductRight' :
    AddMonoidAlgebra S A ⊗[R] N ≃ₗ[S] AddMonoidAlgebar (S ⊗[R] N) A := sorry

which might even be true as an AlgHom

Might this wait for another occasion?

[Eric Wieser]

but when the modules on the left have additional actions, then so do the tensor products, and the maps defined have extra linearity.

Are you aware of docs#TensorProduct.AlgebraTensorModule.congr ?

[Antoine Chambert-Loir]

I was not…

[Antoine Chambert-Loir]

(but we miss the analogue for docs#TensorProduct.directSumLeft , so some thing needs to be done anyway…)

[Antoine Chambert-Loir]

#10824