[Merged by Bors] - feat: heterogenize TensorProduct.congr and friends

[eric-wieser]

The summary is that this PR:

• generalizes a handful of results to non-commutative algebras (simply by moving them to an earlier section)
• adds heterogenous versions of map, congr, mapBilinear, homTensorHom, leftComm, tensorTensorTensorComm
• generalizes lcurry, uncurry, and assoc to take an extra algebra, such that the As in the two different places can separately be replaced with R

The punchline here is really:

def tensorTensorTensorComm :
  (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) :=

which is valuable for a base change / tensor product of bilinear forms when instantiated as

(M ⊗[R] N) ⊗[A] (Dual A M ⊗[R] Dual R N)
  ≃ₗ[A]
(M ⊗[A] Dual A M) ⊗[R] (N ⊗[R] Dual R N)

It would not surprise me if it's possible to introduce a third ring into tensorTensorTensorComm, but for now I'd prefer to assume that for that particular definition, two rings is enough for anybody!

Unfortunately, this was not the case for lcurry, uncurry, and assoc, which really do need to work over three rings so that the As in the two different places can separately be replaced with R; both permutations are needed in the construction of tensorTensorTensorComm, and it seemed preferable to not have a plethora of primed variants.

I make no claim that the pile of IsScalarTower and SMulCommClass arguments here are in any sense optimal, besides the fact they specifically enable the use-case I have for the base change of bilinear forms.

---

• depends on: [Merged by Bors] - feat(ring_theory/tensor_product): add missing scalar tower instances mathlib3#19143
• depends on: [Merged by Bors] - chore(linear_algebra/tensor_product): forward-port leanprover-community/mathlib#19143 #6094
• depends on: [Merged by Bors] - chore: split RingTheory/TensorProduct #6187

Extracted from pygae/lean-ga#31. There is more I want to extract from that patch (most notably the heterobasic BilinForm.tensorDistrib, but the rest will come in a future PR.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(ring_theory/tensor_product): add missing scalar tower instances mathlib3#19143
• [Merged by Bors] - chore(linear_algebra/tensor_product): forward-port leanprover-community/mathlib#19143 #6094
• [Merged by Bors] - chore: split RingTheory/TensorProduct #6187
  By Dependent Issues (🤖). Happy coding!

[kbuzzard]

I get the impression that this work is a lot more impressive than it lets on: I tried mildly generalising some of the results and immediately got into all sorts of problems. All the proofs are very succinct and to be quite frank I think I might struggle with some of them on paper; if everything is R-linear and tensor products are all over R then everything is easy, but once you start throwing around more rings then things seem to become a lot more delicate. Well done! I left a host of comments, some of which don't need acting on and can just be resolved after you've read them if you agree that nothing needs doing. Thanks a lot!

[kbuzzard]

Is this a candidate for @[simps]? I'm only just getting the hang of @[simps]. Or is the idea that you're safer writing your own simp lemmas for declarations as complicated as this?

[eric-wieser]

simps generates something with implicit type arguments, which aren't really needed here; though I'll admit I don't remember if that was my reason.

In generaly my rule is "use simps if I'm feeling lazy, write the lemma manually if I'm feeling picky or simps screws up". The important thing is to have some simp lemma, the API doesn't really care whether it's generated with simps.

[kbuzzard]

Do you think there's a version of this where [IsScalarTower A B M] is replaced by [IsScalarTower A B P]? Note that I'm not suggesting that you add it, but if you think that there's some merit to this suggestion then you could leave a comment. This seems to be the only def where you need to assume B is an A-algebra.

[eric-wieser]

I don't know. This was one where the "obvious" implementation required more typeclasses than the statement. I think I recall places in mathlib where the "clever" bundling approach requires more typeclasses than the dumb but annoying induction approach, but I was pretty maximally annoyed by this point and didn't want to think much more about generalization!

[eric-wieser]

I get the impression that this work is a lot more impressive than it lets on: I tried mildly generalising some of the results and immediately got into all sorts of problems.

I'll try to reflect this in an update to the PR description :)

All the proofs are very succinct and to be quite frank I think I might struggle with some of them on paper; if everything is R-linear and tensor products are all over R then everything is easy, but once you start throwing around more rings then things seem to become a lot more delicate.

Frankly tensorTensorTensorComm was awful; keeping track of 4 modules tensored over 3 rings was too much for my working memory, and I think I would have had a much easier time if I could have color-coded the goal view somehow to keep track of them.

[jcommelin]

Thanks, this looks very clean.
I did not think at all about whether/how this could possibly be generalized. As you indicate, it is probably possible. But we can do that when we need it.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style