Commit 2023-08-07 16:43 759a1d08

View on Github →

feat(RingTheory/TensorProduct): heterogenize (#6417) This:

  • Improves the module docstring, which was both out of date and not very informative
  • Addresses a TODO to generalize includeLeft to commuting actions. As a result a few downstream results are changed to be about includeLeftRingHom or a ⊗ₜ 1, as carrying around the extra useless ring just makes the lemmas harder to use. Nothing seems to suffer from this change.
  • Introduces TensorProduct.AlgebraTensorModule.rid
  • Generalizes the following to work for towers of rings:
    • Algebra.TensorProduct.algHomOfLinearMapTensorProduct
    • Algebra.TensorProduct.map
    • Algebra.TensorProduct.congr
    • Algebra.TensorProduct.endTensorEndAlgHom
    • Algebra.TensorProduct.ext (and renames it to Algebra.TensorProduct.ext')
    • Algebra.TensorProduct.rid
  • Introduces a new Algebra.TensorProduct.ext which follows "partially-applied ext lemmas", and uses it to golf a proof in RingTheory/Etale.lean

I need many of these results for building AlgEquivs relating to the base change of clifford algebras.

Estimated changes

modified theorem Algebra.TensorProduct.ext