Maps from a tensor product of algebras

Stream: Is there code for X?

[Kevin Buzzard]

If $R$ is a commutative ring and $A_i$ are a family of commutative $R$-algebras (indexed by a finite type $\iota$) then I claim that to give an $R$-algebra map from $\otimes_i A_i$ to a commutative $R$-algebra $B$ is to give $R$-algebra maps from each $A_i$ to $B$. Does this sound right? If so, do we have it? I'd never used MultilinearMap and PiTensorProduct until ten minutes ago but I've come up with this where I think all data is there and the only sorrys are proofs. This might not be idiomatic (especially constructing the multilinear map from the collection of linear maps, here I just used the default constructor).

import Mathlib.RingTheory.PiTensorProduct

variable {R : Type*} [CommRing R]
    {ι : Type*} [Fintype ι] [DecidableEq ι] {A : ι → Type*}
    [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    (B : Type*) [CommRing B] [Algebra R B]

open TensorProduct PiTensorProduct

noncomputable def foo : ((⨂[R] i, A i) →ₐ[R] B) ≃ Π i, (A i) →ₐ[R] B where
  toFun f i := f.comp (singleAlgHom i)
  invFun g := liftAlgHom
    ⟨fun x ↦ ∏ (i : ι), g i (x i), sorry, sorry⟩ sorry sorry
  left_inv f := by sorry
  right_inv g := by sorry

[Eric Wieser]

docs#MultilinearMap.piFamily might be relevant

[Adam Topaz]

docs#PiTensorProduct.lift presumably?

[Adam Topaz]

Oh you already use that in liftAlgHom

[Kevin Buzzard]

That's the statement that $R$-linear maps from the tensor product are the same thing as multilinear maps from the factors. I want that $R$-algebra maps from the tensor product are the same thing as algebra maps from the factors.

[Adam Topaz]

yeah I see that.

[Kevin Buzzard]

(this is relevant for Grassmannians, is why I'm asking)

[Adam Topaz]

I'm guessing we don't have the thing you need on the MultiLinearMap side :-/

[Eric Wieser]

Note that there are open PRs about grassmanians that might already contain this in some form, such as #11155

[Adam Topaz]

I mean the statement is definitely correct because the tensor product is the coproduct in the category of algebras.

[Eric Wieser]

noncomputable def foo : ((⨂[R] i, A i) →ₐ[R] B) ≃ Π i, (A i) →ₐ[R] B where
  toFun f i := f.comp (singleAlgHom i)
  invFun g := liftAlgHom (MultilinearMap.mkPiAlgebra _ _ _ |>.compLinearMap (g · |>.toLinearMap))
    (by simp)
    (fun x y => by simp [Finset.prod_mul_distrib])
  left_inv f := by ext; simp; sorry
  right_inv g := by ext; simp; sorry

is close

[Aaron Liu]

import Mathlib.RingTheory.PiTensorProduct

variable {R : Type*} [CommRing R]
    {ι : Type*} [Fintype ι] [DecidableEq ι] {A : ι → Type*}
    [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    (B : Type*) [CommRing B] [Algebra R B]

open TensorProduct PiTensorProduct

noncomputable def foo : ((⨂[R] i, A i) →ₐ[R] B) ≃ Π i, (A i) →ₐ[R] B where
  toFun f i := f.comp (singleAlgHom i)
  invFun g := liftAlgHom (MultilinearMap.mkPiAlgebra _ _ _ |>.compLinearMap (g · |>.toLinearMap))
    (by simp)
    (fun x y => by simp [Finset.prod_mul_distrib])
  left_inv f := by
    ext
    simp [← map_prod, ← tprod_prod, Finset.univ_prod_mulSingle]
  right_inv g := by
    ext
    simp only [AlgHom.coe_comp, Function.comp_apply, singleAlgHom_apply, MonoidHom.mulSingle_apply,
      liftAlgHom_apply, lift.tprod, MultilinearMap.compLinearMap_apply, AlgHom.toLinearMap_apply,
      MultilinearMap.mkPiAlgebra_apply]
    simp_rw [Pi.apply_mulSingle (fun i x ↦ g i x) (by simp)]
    conv_lhs =>
      rhs
      intro
      rw [Pi.mulSingle_comm]
    simp

[Robert Maxton]

Adam Topaz said:

I mean the statement is definitely correct because the tensor product is the coproduct in the category of algebras.

Not having this def is in fact the reason I started writing colimits for RingCat!

(... and then got distracted by life before finishing, oops >.>;)