Commit 2024-03-08 09:46 099074e1

View on Github →

feat(LinearAlgebra/PiTensorProduct): some more functoriality properties of PiTensorProduct (#11152)

Prove some properties of PiTensorProduct.map, for example the compatibility with composition and reindeixing, and the fact that it sends the identity to the identity.
Construct PiTensorProduct.map as a MultilinearMap on the family of linear maps.
Upgrade PiTensorProduct.map f to a linear equivalence called PiTensorProduct.congr f when f is a family of linear equivalences.
For ι a Fintype, define the canonical linear equivalence (given by multiplication) constantBaseRingEquiv from ⨂ i : ι, R and R.

Estimated changes

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

added theorem PiTensorProduct.congr_symm_tprod

added theorem PiTensorProduct.congr_tprod

modified theorem PiTensorProduct.isEmptyEquiv_apply_tprod

added theorem PiTensorProduct.lift_comp_map

modified def PiTensorProduct.map

added def PiTensorProduct.mapIncl

added def PiTensorProduct.mapMonoidHom

added theorem PiTensorProduct.map_comp

added theorem PiTensorProduct.map_comp_reindex_eq

added theorem PiTensorProduct.map_comp_reindex_symm

added theorem PiTensorProduct.map_id

added theorem PiTensorProduct.map_mul

added theorem PiTensorProduct.map_one

added theorem PiTensorProduct.map_range_eq_span_tprod

added theorem PiTensorProduct.map_reindex

added theorem PiTensorProduct.map_reindex_symm

modified theorem PiTensorProduct.map_tprod

added theorem PiTensorProduct.span_tprod_eq_top