Interaction`MvPolynomial` and `TensorProduct`

Stream: Is there code for X?

[Christian Merten]

I was looking for interactions of MvPolynomial and TensorProduct but could not find any. Did I miss something? For example, I was looking for:

import Mathlib

universe u v w

open TensorProduct

variable (σ : Type v)
variable (R : Type u) [CommRing R]
variable (A : Type w) [CommRing A] [Algebra R A]

private noncomputable def MvPolynomial.baseChangeAux :
    A ⊗[R] (MvPolynomial σ R) →ₐ[A] MvPolynomial σ A :=
  Algebra.TensorProduct.lift
    (Algebra.ofId A (MvPolynomial σ A))
    (mapAlgHom <| Algebra.ofId R A) <| by
  intro a P
  exact Algebra.commutes a (eval₂ (RingHom.comp C (algebraMap R A)) X P)

private noncomputable def MvPolynomial.baseChangeAuxInv :
    MvPolynomial σ A →ₐ[A] A ⊗[R] (MvPolynomial σ R) :=
  MvPolynomial.aeval (fun s ↦ 1 ⊗ₜ X s)

noncomputable def MvPolynomial.baseChange :
    A ⊗[R] MvPolynomial σ R ≃ₐ[A] MvPolynomial σ A := AlgEquiv.ofAlgHom
  (baseChangeAux σ R A)
  (baseChangeAuxInv σ R A)
  (by ext s; simp [baseChangeAux, baseChangeAuxInv])
  (by ext s; simp [baseChangeAux, baseChangeAuxInv])

[Jz Pan]

Maybe it's work in progress: #10824

[Junyan Xu]

This gives the LinearEquiv (up to defeq) but not AlgEquiv

[Christian Merten]

Thanks for the pointers!