Algebra.TensorProduct.assoc

Stream: Is there code for X?

[Edison Xie]

import Mathlib
def Algebra.TensorProduct.assoc' (R S R' A B C : Type*) [CommSemiring R] [CommSemiring S]
    [CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A]
    [Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C]
    [IsScalarTower R R' A] [IsScalarTower R R' B] [Algebra S A] [Algebra R S] [Algebra R' S]
    [IsScalarTower R' S A] [IsScalarTower R S A] :
    (A ⊗[R'] B) ⊗[R] C ≃ₐ[S] A ⊗[R'] (B ⊗[R] C) :=
  AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.assoc _ _ _ _ _ _)
    rfl (LinearMap.map_mul_iff _|>.2 <| by ext; simp)

Do we have this in mathlib? If not should I PR this?

[Antoine Chambert-Loir]

What about docs#TensorProduct.AlgebraTensorModule.assoc ?

[Edison Xie]

That’s the linear version right :-)

[Antoine Chambert-Loir]

Right, sorry… You want an heteromachinchose version of docs#Algebra.TensorProduct.assoc.
(This afternoon, I spent two much time defining an analogous trivial map S' ⊗[R'] R' ⊗[R] M ≃ₗ[S'] S' ⊗[R] M…)

[Yaël Dillies]

Since the advent of heterobasic tensor product, the whole situation is a mess :sad: We need to

1. Remove the homobasic version in favour of the heterobasic one
2. Find naming schemes for the different kinds of tensor products and the different kinds of maps they have

[Eric Wieser]

I think for the algebra ones we just tried to make all the results heterobasic?

[Edison Xie]

Yaël Dillies said:

Since the advent of heterobasic tensor product, the whole situation is a mess :sad: We need to

1. Remove the homobasic version in favour of the heterobasic one
2. Find naming schemes for the different kinds of tensor products and the different kinds of maps they have

So… the answer is yes and no? It’s just this lemma has been sitting inside my repo for four months and I think it’s useful to have it in mathlib :joy:

[Yaël Dillies]

I have no idea whether this is in mathlib or not, but at this point I would rather see a big refactor that gets what's there right before committing to new stuff

[Kevin Buzzard]

This is not really a helpful comment unless it's followed by "...and I'm going to start that refactor right now" and in particular a clarification of what it means to get things "right" in your view. You're saying "I don't like how things are" but are not offering a path to make it more like how you want it, whilst simultaneously blocking progress. I would rather see this lemma merged than a nebulous complaint.

[Yaël Dillies]

Yaël Dillies said:

Since the advent of heterobasic tensor product, the whole situation is a mess :sad: We need to

1. Remove the homobasic version in favour of the heterobasic one
2. Find naming schemes for the different kinds of tensor products and the different kinds of maps they have

Is this not exactly the path forward I suggested?

[Yaël Dillies]

Eric Wieser said:

I think for the algebra ones we just tried to make all the results heterobasic?

Indeed, it looks like what's left as homobasic duplication is the TensorProduct vs AlgebraTensorModule stuff.

[Yaël Dillies]

In total I can find:

• TensorProduct: Homobasic tensor product of modules
• TensorProduct.AlgebraTensorModule: Heterobasic tensor product of modules
• Algebra.TensorProduct: Heterobasic tensor product of algebras
• Coalgebra.TensorProduct: Heterobasic tensor product of coalgebras
• Bialgebra.TensorProduct: Heterobasic tensor product of bialgebras/Hopf algebras

[Yaël Dillies]

Therefore I would suggest that:

1. We deprecate all the TensorProduct material in favour of the TensorProduct.AlgebraTensorModule one.
2. We find a naming scheme for the material that's left.

[Yaël Dillies]

My experience working with these is that one often needs eg the module and algebra versions simultaneously. meaning that it should be possible to open namespaces and still have the different version easily distinguishable

[Yaël Dillies]

I see a few options for that. Taking the representative series docs#TensorProduct.AlgebraTensorModule.map, docs#Algebra.TensorProduct.map, docs#Coalgebra.TensorProduct.map, docs#Bialgebra.TensorProduct.map, we could have

1. Statu quo: Module.TensorProduct.map, Algebra.TensorProduct.map, Coalgebra.TensorProduct.map, Bialgebra.TensorProduct.map. Is a more conventional use of namespaces, but then no two of Module, Algebra, Coalgebra, Bialgebra can be opened simultaneously.
2. Statu quo with namespaces inverted: TensorProduct.Module.map, TensorProduct.Algebra.map, TensorProduct.Coalgebra.map, TensorProduct.Bialgebra.map. This way one can open TensorProduct and work with Module.map and Algebra.map simultaneously, which an improvement over the statu quo but not great still.
3. Single namespace with types of maps appended: TensorProduct.mapLinearMap (or maybe just TensorProduct.map), TensorProduct.mapAlgHom, TensorProduct.mapCoalgHom, TensorProduct.mapBialgHom. This is the actual convention that we use elsewhere. Makes it a bit lengthy when talking about a single kind of tensor products/maps, but overall pretty good.
4. Single namespace with types of maps appended as a single letter: TensorProduct.mapL,TensorProduct.mapA, TensorProduct.mapC, TensorProduct.mapB. Pushes the abbreviations to their limit, but is still discoverable, learnable, and is definitely the most concise when talking about several kinds of tensor products simultaneously.

[Yaël Dillies]

/poll Which of the above options strikes the best balance of readability/conciseness when using both a single and several tensor products?
Statu quo
Statu quo with namespaces inverted
Single namespace with types of maps appended
Single namespace with types of maps appended as a single letter

[Eric Wieser]

I don't think this is relevant to Edison's problem, where the answer is just "generalize the existing definition in-place"?

[Eric Wieser]

(and so I'd suggest splitting the thread)

[Eric Wieser]

I think there's also a danger here of the module ones becoming semilinearized, which might not be compatible with heterogeneity

[Antoine Chambert-Loir]

Just a remark about the mess for heterobasic situations that I observed yesterday. Imagine you havet wo commutative semirings $R$ and $S$ and three modules $M$, $N$, $P$ that allow to build the tensor product $M \otimes_R \otimes N \otimes_S P$. There are two (symmetric) sets of hypotheses that allow mathlib to recognize this expression as legit.

theorem exists_multiset_eq_sum_tmul_tmul {R S M N P: Type*}
    [CommSemiring R]  [CommSemiring S] [Algebra R S]
    [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N]
    [AddCommMonoid P] [Module S P]
    (x : M ⊗[R] N ⊗[S] P) :
    ∃ (ξ : Multiset (M × N × P)), x = (ξ.map (fun x ↦ x.1 ⊗ₜ[R] x.2.1 ⊗ₜ[S] x.2.2)).sum := by
sorry

and its symmetric variant

theorem exists_multiset_eq_sum_tmul_tmul' {R S M N P: Type*}
    [CommSemiring R] [CommSemiring S] [Algebra S R]
    [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower S R N]
    [AddCommMonoid P] [Module S P]
    (x : M ⊗[R] N ⊗[S] P) :
    ∃ (ξ : Multiset (M × N × P)),  x = (ξ.map (fun x ↦ x.1 ⊗ₜ[R] x.2.1 ⊗ₜ[S] x.2.2)).sum := by
  sorry

[Antoine Chambert-Loir]

(I put as a challenge to establish the analogues with docs#Finset, I'm not sure they hold.)

[Yaël Dillies]

Surely in practice you only have one of Algebra R S and Algebra S R, and never both?

[Antoine Chambert-Loir]

Except when R = S, you mean?

[Antoine Chambert-Loir]

All of this would be clearer with bimodules, $M$ would be a right $R$-module, $N$ an $(R,S)$-bimodule and $P$ a left $S$-module.

[Antoine Chambert-Loir]

By the way, the code above suggests the interest of a notation for summation over a docs#Multiset.

[Yaël Dillies]

Such notation hasn't been added to encourage you to use docs#Finset.sum instead

[Yaël Dillies]

ie something like ∃ (ι : Type) (_ : Fintype ι) (m : ι → M) (n : ι → N) (p : ι → P), x = ∑ i, m i ⊗ₜ[R] n i ⊗ₜ[S] p i. This is more composable than your statement

[Yaël Dillies]

Antoine Chambert-Loir said:

Except when R = S, you mean?

When R = S, the assumptions are equivalent, so I am not sure what your point is

[Antoine Chambert-Loir]

Assuming that Kevin is not around, I have to confess that I tried such a thing but couldn't guess the adequate universe in which the type ι would live. And the obvious definition does not furnish Type 0.

[Antoine Chambert-Loir]

Anyway, I'll adjust as you suggest.

[Aaron Liu]

Antoine Chambert-Loir said:

Assuming that Kevin is not around, I have to confess that I tried such a thing but couldn't guess the adequate universe in which the type ι would live. And the obvious definition does not furnish Type 0.

I know of docs#Module.equiv_free_prod_directSum which uses the universe the ring is in and docs#CommGroup.equiv_prod_multiplicative_zmod_of_finite which uses Type 0 (the universe that ℤ is in). They should all still be (noncomputably) equivalent since finite types can be shrunk down to any universe.

[Eric Wieser]

Yaël Dillies said:

Surely in practice you only have one of Algebra R S and Algebra S R, and never both?

I think you need neither?

[Yaël Dillies]

I suspect so too, but I would need to play with the proof to convince myself

[Eric Wieser]

I thought the claim was about the statement only

[Yaël Dillies]

Ah maybe!

[Antoine Chambert-Loir]

Well, the present proof uses the hypothesis, just because the mathlib statement needs it, but the bimodule version indicates that it shouldn't be needed.

[Yaël Dillies]

Eric Wieser said:

I think there's also a danger here of the module ones becoming semilinearized, which might not be compatible with heterogeneity

Can you expand on exactly how it would be incompatible?

[Eric Wieser]

We have a number of bundled linear maps for linear map composition which exist in both variants without a common generalization

[Eric Wieser]

If you can generalize those I will be less concerned

[Yaël Dillies]

Do you have an example pair? Is one of the maps merely semi-linear, or are they both linear?