tensor product distributes over `prod`

Stream: Is there code for X?

[Kevin Buzzard]

I need that tensor product distributes over prod and over direct sums. I was on a plane so wrote the prod version ($M\oplus N)\otimes K\cong M\otimes K\oplus N\otimes K$) from first principles because I couldn't find it:

import linear_algebra.free_module.pid

lemma prod.fst_def {α β : Type*} {a : α} {b : β} : (a, b).fst = a := rfl
lemma prod.snd_def {α β : Type*} {a : α} {b : β} : (a, b).snd = b := rfl

variables (R : Type*) [comm_ring R]

open_locale tensor_product

def tensor_product.prod_tensor {M N : Type*} [add_comm_group M] [add_comm_group N] [module R M]
  [module R N] (K : Type*) [add_comm_group K] [module R K] :
  (M × N) ⊗[R] K ≃ₗ[R] (M ⊗[R] K) × (N ⊗[R] K) :=
{ to_fun := tensor_product.lift $ linear_map.coprod
      ((tensor_product.lift.equiv R M K _).symm (linear_map.inl _ _ _))
      ((tensor_product.lift.equiv R N K _).symm (linear_map.inr _ _ _)),
  map_add' := linear_map.map_add _,
  map_smul' := linear_map.map_smul _,
  inv_fun := linear_map.coprod (linear_map.rtensor K (linear_map.inl _ _ _))
    (linear_map.rtensor K (linear_map.inr _ _ _)),
  left_inv := λ x, begin
    rw ← linear_map.comp_apply,
    change _ = linear_map.id x,
    refine linear_map.ext_iff.1 (tensor_product.ext' _) x,
    rintros ⟨m, n⟩ k,
    simp only [linear_map.comp_apply, tensor_product.lift.tmul, linear_map.coprod_apply,
      linear_map.add_apply, tensor_product.lift.equiv_symm_apply, linear_map.inl_apply,
      linear_map.inr_apply, prod.mk_add_mk, add_zero, zero_add, linear_map.rtensor_tmul,
      linear_map.coe_inl, linear_map.coe_inr, linear_map.id_coe, id.def, ← tensor_product.add_tmul],
  end,
  right_inv := λ x, begin
    rw ← linear_map.comp_apply,
    change _ = linear_map.id x,
    refine linear_map.ext_iff.1 (linear_map.prod_ext (tensor_product.ext' (λ m k, _))
      (tensor_product.ext' (λ n k, _))) x,
    { rw [linear_map.comp_apply, linear_map.id_comp, linear_map.inl_apply, linear_map.comp_apply,
          linear_map.coprod_apply, prod.fst_def, linear_map.rtensor_tmul, linear_map.map_zero,
          add_zero, linear_map.inl_apply, tensor_product.lift.tmul, linear_map.coprod_apply,
          prod.fst_def, prod.snd_def, linear_map.map_zero, add_zero,
          tensor_product.lift.equiv_symm_apply, linear_map.inl_apply] },
    { rw [linear_map.comp_apply, linear_map.id_comp, linear_map.inr_apply, linear_map.comp_apply,
          linear_map.coprod_apply, prod.fst_def, linear_map.rtensor_tmul, linear_map.map_zero,
          zero_add, linear_map.inr_apply, tensor_product.lift.tmul, linear_map.coprod_apply,
          prod.fst_def, prod.snd_def, linear_map.map_zero, zero_add,
          tensor_product.lift.equiv_symm_apply, linear_map.inr_apply] },
  end }

It was a lot longer than I expected (simp would just time out so I had to work out the rewrites by hand). I suspect that $(\oplus_i M_i)\otimes K\cong \oplus_i (M_i \otimes K)$ will be even worse. Do we have these things already? Should I be using the category theory library and arguing that tensor products commute with these colimits or will that be even worse?

[Eric Wieser]

You can make that very slightly shorter by using (tensor_product.mk R N K).compr₂ instead of (tensor_product.lift.equiv R M K _).symm

[Eric Wieser]

I guess it's pretty annoying how awkward it is to construct M × N →ₗ[R] K →ₗ[R] M ⊗ K × N ⊗ K when you really just want to write λ (mn : M × N) k, (mn.1 ⊗ₜ[R] k, mn.2 ⊗ₜ[R] k) (which is also definitionally better than the coprod/inl/inr spelling)

[Kevin Buzzard]

Right, I could have done that but of course then I have to prove that everything is R-linear manually

[Adam Topaz]

@Kevin Buzzard we have something like this in LTE

[Adam Topaz]

(But maybe only for Ab?)

[Adam Topaz]

We also have docs#tensor_product.direct_sum

[Kevin Buzzard]

Oh thanks!

[Chris Hughes]

Would it have been feasible to prove this using the category theory library? Just by arguing tensor preserves colimits because it has a right adjoint?

[Adam Topaz]

Yes, but I don't think we have the adjunction in mathlib

[Adam Topaz]

Note that biproducts are both colimits and limits, so if you show that tensoring is a left adjoint, you get that it commutes with colimits for free and since biproducts are in particular colimits, you get that they commute with biproducts

[Antoine Labelle]

We do have that adjunction, it is docs#Module.category_theory.monoidal_closed

[Jack J Garzella]

Should be very similar to #new members > Using the fact that a functor preserves limits, for which the solution has two lines of code. I'm not sure if the same universe issue would show up.

[Eric Wieser]

Ugh, I just wrote this again without searching on Zulip first!

attribute [ext] TensorProduct.ext in
def TensorProduct.prodRight : M₁ ⊗[R] (M₂ × M₃) ≃ₗ[R] ((M₁ ⊗[R] M₂) × (M₁ ⊗[R] M₃)) :=
  LinearEquiv.ofLinear
    (TensorProduct.lift <|
      LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) R
        ∘ₗ LinearMap.prod (TensorProduct.mk _ _ _) (TensorProduct.mk _ _ _))
    (LinearMap.coprod
      (LinearMap.lTensor _ <| LinearMap.inl _ _ _)
      (LinearMap.lTensor _ <| LinearMap.inr _ _ _))
    (by ext <;> simp)
    (by ext <;> simp)

[Eric Wieser]

At least it's shorter than the previous version!

[Eric Wieser]

#7226

[Antoine Chambert-Loir]

Oh, that's a case where using docs#TensorProduct.comm seems to be useful to prove half of those left/right statements !