TensorProduct vs TensorProduct.AlgebraTensorModule vs ...

Stream: mathlib4

[Yaël Dillies]

We currently have two ways to talk about the tensor product of modules:

• Things in the TensorProduct namespace are about the tensor product of two R-modules M and N as an R-module
• Things in the TensorProduct.AlgebraTensorModule namespace are about the tensor product of anR-module M with an A-module N as an A-module, where A is an R-algebra

[Yaël Dillies]

On top of this, there's the tensor product of algebras and of coalgebras whose respective APIs lie in the Algebra.TensorProduct and Coalgebra.TensorProduct namespaces (making the Algebra and Coalgebra namespaces basically unopenable btw, since almost everything in Algebra.TensorProduct/Coalgebra.TensorProduct would conflict with almost everything in the TensorProduct namespace).

[Yaël Dillies]

Declarations in the TensorProduct namespace are not defeq to their analogues in the TensorProduct.AlgebraTensorModule namespace. For most of these declarations, mathlib doesn't even know that they are equal (in fact, docs#TensorProduct.AlgebraTensorModule.rid_eq_rid is the only one I could find)

[Yaël Dillies]

Recently, @Andrew Yang changed the defeq of the declarations in the Coalgebra.TensorProduct namespace from the ones in TensorProduct to the ones in TensorProduct.AlgebraTensorModule. Toric quite literally exploded.

[Eric Wieser]

Have you considered removing the || catch_fire step from your CI, if the explosion was literal?

[Yaël Dillies]

Okay, it didn't explode that literally :laughing:

[Eric Wieser]

I would guess that we want to drop everything in TensorProduct and replace it with the stuff in AlgebraTensorModule, but that we didn't do so in the past because of performance

[Eric Wieser]

Or maybe the generalities were not comparable until more recently

[Eric Wieser]

I also agree that the Foo.TensorProduct namespacing is terrible, but I think it's difficult to clean this up without first doing the merge I just described.

[Andrew Yang]

Here's the PR making them defeq so we can switch more easily later: #25298

[Yaël Dillies]

(deleted)