feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of `PiTensorProduct`

[smorel394]

trafficstars

Construct a basis of a PiTensorProduct of modules given bases of the modules, and relationship between the dual of a PiTensorProduct and the PiTensorProduct of the duals.

Main results:

• Basis.piTensorProduct (in LinearAlgebra/TensorProductBasis.lean): Let ι be a Fintype and M be a family of modules indexed by ι. If b i : κ i → M i is a basis for every i in ι, then fun (p : Π i, κ i) ↦ ⨂ₜ[R] i, b i (p i) is a basis of ⨂[R] i, M i.
• PiTensorProduct.dualDistrib (in LinearAlgebra/Dual.lean): The canonical linear map from ⨂[R] i, Dual R (M i) to Dual R (⨂[R] i, M i), sending ⨂ₜ[R] i, f i to the composition of PiTensorProduct.map f with the linear equivalence ⨂[R] i, R →ₗ R given by multiplication.
• PiTensorProduct.dualDistribEquiv (also in LinearAlgebra/Dual.lean): A linear equivalence between ⨂[R] i, Dual R (M i) and Dual R (⨂[R] i, M i) when all M i are finite free modules. If f : (i : ι) → Dual R (M i), then this equivalence sends ⨂ₜ[R] i, f i to the composition of PiTensorProduct.map f with the natural isomorphism ⨂[R] i, R ≃ R given by multiplication.

• [ ] depends on: #11155

---

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• leanprover-community/mathlib4#11155 By Dependent Issues (🤖). Happy coding!