The tensor product of hom modules is the hom module of the tensor products #
Mathlib's PiTensorProduct.piTensorHomMap is the canonical comparison map
⨂ᵢ (Mᵢ →ₗ Nᵢ) → (⨂ᵢ Mᵢ →ₗ ⨂ᵢ Nᵢ), ⨂ᵢ fᵢ ↦ ⨂ᵢ mᵢ ↦ ⨂ᵢ fᵢ mᵢ,
defined for arbitrary families of modules over a commutative semiring. This file proves that it is
bijective as soon as the index type is finite and every Mᵢ is finite projective, with the
Nᵢ arbitrary, and packages the result as the linear equivalence
PiTensorProduct.piTensorHomEquiv. This is the ι-ary form of Mathlib's
TensorProduct.homTensorHomEquiv, under the same hypotheses.
For finite free Mᵢ the proof is a basis computation: a basis bᵢ of Mᵢ indexed by a finite
κᵢ identifies Mᵢ →ₗ Nᵢ with the functions κᵢ → Nᵢ, the tensored basis identifies
⨂ᵢ Mᵢ →ₗ ⨂ᵢ Nᵢ with the functions (∀ i, κᵢ) → ⨂ᵢ Nᵢ, and under these identifications the
comparison map is the distributivity of the tensor product over finite direct sums,
PiTensorProduct.ofDFinsuppEquiv. A finite projective module is a retract of a finite free one,
and precomposition with the retraction data transports bijectivity. This step adapts the retract
argument in the proof of Mathlib's dualTensorHom_bijective
(Mathlib/LinearAlgebra/Contraction.lean).
Taking Nᵢ = Mᵢ this identifies End (⨂ᵢ Mᵢ) with ⨂ᵢ End Mᵢ, compatibly with composition
(PiTensorProduct.piTensorHomEquiv_tprod_comp_tprod). That identification is the shape in which the
commutant computations of Schur-Weyl duality are run: the endomorphisms of a tensor power commuting
with the permutations of the factors are the invariants of the permutation action on the tensor
power of the endomorphism algebra.
Main definitions #
PiTensorProduct.piTensorHomEquiv: the comparison map as a linear equivalence, for a finite index type and finite projective source modules.
Main results #
PiTensorProduct.piTensorHomMap_bijective_of_basis: bijectivity of the comparison map from a family of finite bases of the source modules.PiTensorProduct.piTensorHomMap_bijective: bijectivity for finite projective source modules.PiTensorProduct.piTensorHomEquiv_tprod_comp_tprod: the equivalence turns the factorwise composition of two pure tensors of linear maps into the composition of their images.
References #
- W. Fulton and J. Harris, Representation Theory: A First Course, Appendix B.1.
The comparison map is bijective, given a finite basis of every Mᵢ; the Nᵢ are
arbitrary.
The comparison map ⨂ᵢ (Mᵢ →ₗ Nᵢ) → (⨂ᵢ Mᵢ →ₗ ⨂ᵢ Nᵢ) is bijective over a finite index
type when every Mᵢ is finite projective; the Nᵢ are arbitrary.
The tensor product of the hom modules is the hom module of the tensor products. The
underlying map is PiTensorProduct.piTensorHomMap, so this is a statement about a canonical map
and not about a choice of bases, even though the proof makes one.
Instances For
The equivalence acts as the comparison map it is built from. The priority is low so that the
more specific PiTensorProduct.piTensorHomEquiv_tprod still reaches its own normal form
PiTensorProduct.map on a pure tensor, which this rule would otherwise strand at
PiTensorProduct.piTensorHomMap.
The equivalence and the comparison map have the same underlying function.
On a pure tensor of linear maps the equivalence is PiTensorProduct.map.
The inverse of the equivalence takes the factorwise map back to the pure tensor.
The equivalence is functorial on pure tensors: composing factorwise and then comparing is
comparing and then composing. For Nᵢ = Pᵢ = Mᵢ this is multiplicativity on pure tensors of
endomorphisms, which is what makes the identification usable on the subalgebras of
End (⨂ᵢ Mᵢ) that Schur-Weyl duality is about.