[Merged by Bors] - feat(linear_algebra/multilinear/basis): multilinear maps on basis vectors

[jsm28]

Add two versions of the fact that a multilinear map on finitely many
arguments is determined by its values on basis vectors. The precise
requirements for each version follow from the results used in the
proof: basis.ext_multilinear_fin uses the curry and uncurry
results to deduce it from basis.ext and thus works for multilinear
maps on a family of modules indexed by fin n, while
basis.ext_multilinear works for an arbitrary fintype index type
but is limited to the case where the modules for all the arguments
(and the bases used for those modules) are the same, since it's
derived from the previous result using dom_dom_congr which only
handles the case where all the modules are the same.

This is in preparation for proving a corresponding result for
alternating maps, for which the case of all argument modules the same
suffices.

There is probably room for making results more general.

---

[eric-wieser]

If the dependency of linear_algebra.multilinear.basic on
linear_algebra.basis isn't desired, this code could of course go in
a separate file.

In the interest of not letting basic.lean expand too much, I think a new multilinear/basis file would be a good idea.

[jsm28]

I've now moved the lemmas to such a new file.

[eric-wieser]

Suggested change

	{ rw [←f.uncurry_curry_left, ←g.uncurry_curry_left],
	congr' 1,
	{ apply function.left_inverse.injective uncurry_curry_left,

although it might be better to add a standalone

lemma multilinear_map.curry_left_left_inverse :
  left_inverse (linear_map.uncurry_left : _ → multilinear_map R M M₂) multilinear_map.curry_left :=
multilinear_map.uncurry_curry_left

next to uncurry_curry_left first

[jsm28]

I've applied that change (I've not done anything about adding that separate lemma).

[ocfnash]

Could we add the following:

def basis.pi {ι₁ : fin n → Type*} (e : Π i, basis (ι₁ i) R (M i)) :
  basis (Π i, ι₁ i) R (Π i, M i) :=
sorry

and obtain this result as a corollary?

[jsm28]

I don't think that basis.pi is quite what's wanted. Equivalence of multilinear maps to linear maps on the tensor product (and the corresponding basis for the tensor product) would be, but it looks like we only have that for bilinear maps and the tensor product of two modules.

[eric-wieser]

Aren't you describing https://leanprover-community.github.io/mathlib_docs/linear_algebra/pi_tensor_product.html#pi_tensor_product.lift?

[jsm28]

Yes (the separate files for the different cases of tensor product confused me), but as well as the pi_tensor_product not having bases, it also seems to be missing equivalents of most of the API used to define basis.tensor_product.

[ocfnash]

I don't think that basis.pi is quite what's wanted. Equivalence of multilinear maps to linear maps on the tensor product (and the corresponding basis for the tensor product) would be

Oops, yes of course.

Yes (the separate files for the different cases of tensor product confused me), but as well as the pi_tensor_product not having bases, it also seems to be missing equivalents of most of the API used to define basis.tensor_product.

I think situations like this are the perfect time to fill in the missing bits of an API but I can appreciate you might feel this is too much of a diversion. Maybe at least add a TODO in the doc string, saying that this should eventually be refactored through the an API for bases of tensor products?

[jsm28]

I've added that TODO.

[ocfnash]

I've added that TODO.

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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