[Merged by Bors] - feat(linear_algebra/tensor_product): tensor_product.map is bilinear in its two arguments

[antoinelab01]

---

[eric-wieser]

One thing we could consider doing is redefining map directly as the bilinear version. Here's one way to do that:

-- this belongs in `bilinear_map.lean`
/-- A bilinear version of `linear_map.compl₁₂`. -/
def _root_.linear_map.lcompl₁₂ (f : P →ₗ[R] Q →ₗ[R] S) :
  (M →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] (M →ₗ[R] N →ₗ[R] S) :=
begin
  refine linear_map.mk₂ R f.compl₁₂ _ _ _ _; sorry
end

/-- The tensor product of a pair of linear maps between modules, bilinear in both maps. -/
def map : (M →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] N →ₗ[R] P ⊗[R] Q) :=
(mk R P Q).lcompl₁₂.compr₂ $ uncurry R M N (P ⊗ Q)

If nothing breaks, then I think that would maybe be a good idea. Might be worth waiting for other reviewer opinions

[eric-wieser]

What do you (or other reviewers) think about renaming to something along the lines of:

• dual_tensor_dual_map to tensor_product.dual_distrib
• dual_tensor_dual_inv_of_basis to dual.tensor_product_distrib_of_basis
• dual_tensor_dual_equiv_of_basis to tensor_product.dual_distrib_equiv_of_basis

[antoinelab01]

What do you (or other reviewers) think about renaming to something along the lines of:

* `dual_tensor_dual_map` to `tensor_product.dual_distrib`

* `dual_tensor_dual_inv_of_basis` to `dual.tensor_product_distrib_of_basis`

* `dual_tensor_dual_equiv_of_basis` to `tensor_product.dual_distrib_equiv_of_basis`

Sounds fair, though don't it feels a bit weird to have a different prefix for the inverse function? Why not tensor_product.dual_distrib_inv_of_basis for the second one?

[antoinelab01]

One thing we could consider doing is redefining map directly as the bilinear version. Here's one way to do that:

-- this belongs in `bilinear_map.lean`
/-- A bilinear version of `linear_map.compl₁₂`. -/
def _root_.linear_map.lcompl₁₂ (f : P →ₗ[R] Q →ₗ[R] S) :
  (M →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] (M →ₗ[R] N →ₗ[R] S) :=
begin
  refine linear_map.mk₂ R f.compl₁₂ _ _ _ _; sorry
end

/-- The tensor product of a pair of linear maps between modules, bilinear in both maps. -/
def map : (M →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] N →ₗ[R] P ⊗[R] Q) :=
(mk R P Q).lcompl₁₂.compr₂ $ uncurry R M N (P ⊗ Q)

If nothing breaks, then I think that would maybe be a good idea. Might be worth waiting for other reviewer opinions

One reason I see for not doing that is that map_bilinear should have R, M, N, P, Q as explicit variables, while map has them implicit, so changing map to the bilinear version would require adding these variables everywhere map is used which doesn't seem like a good idea.

[dupuisf]

Looks good, thanks!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests