tensor product of bialgebras

Stream: maths

[Kevin Buzzard]

Some of my undergrads have been tricked by me into doing projects for my course which are useful for FLT. Some of them worked on bialgebras and Hopf algebras, and one of them produced the following spectacular piece of code to prove the completely obvious fact "there's an obvious isomorphism $(A\otimes B)\otimes (A\otimes B)\otimes (A\otimes B)=(A\otimes A\otimes A)\otimes(B\otimes B\otimes B)$":

-- Define the linear equivalence of  (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2
-- and (A1 ⊗[R] A1 ⊗[R] A1) ⊗[R] A2 ⊗[R] A2 ⊗[R] A2
private noncomputable def reorder6 :
  (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2 ≃ₗ[R]
  (A1 ⊗[R] A1 ⊗[R] A1) ⊗[R] A2 ⊗[R] A2 ⊗[R] A2 :=
  LinearEquiv.ofLinear
    ((TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
      (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
      (((TensorProduct.assoc _ _ _ _).toLinearMap.rTensor A2).rTensor A2 ∘ₗ
        (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ
        (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ
        (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ
        (((TensorProduct.comm R (A2 ⊗[R] A2) A1).lTensor A1).lTensor A1) ∘ₗ
        (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
        (TensorProduct.assoc _ _ _ _).toLinearMap).rTensor A2 ∘ₗ
     (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ
     ((reorder4 R A1 A2).symm.rTensor (A1 ⊗[R] A2)) ∘ₗ
     (TensorProduct.assoc _ _ _ _).symm.toLinearMap)
    ((TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
      ((reorder4 R A1 A2).rTensor (A1 ⊗[R] A2)) ∘ₗ
      (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
      LinearMap.rTensor A2
      ((TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ
        (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ
        ((TensorProduct.comm R A1 (A2 ⊗[R] A2)).lTensor A1).lTensor A1 ∘ₗ
        (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
        (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
        (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
        ((TensorProduct.assoc _ _ _ _).symm.toLinearMap.rTensor A2).rTensor A2) ∘ₗ
      (TensorProduct.assoc _ _ _ _).symm.toLinearMap ∘ₗ
      (TensorProduct.assoc _ _ _ _).symm.toLinearMap)
 (by aesop) (by aesop)

-- How reorder acts elementwise
lemma reorder6_tmul (a1 a2 a3 : A1) (b1 b2 b3 : A2) :
  reorder6 R A1 A2 ((a1 ⊗ₜ[R] b1) ⊗ₜ[R] (a2 ⊗ₜ[R] b2) ⊗ₜ[R] (a3 ⊗ₜ[R] b3)) =
  (a1 ⊗ₜ[R] a2 ⊗ₜ[R] a3) ⊗ₜ[R] (b1 ⊗ₜ[R] b2 ⊗ₜ[R] b3) := rfl

Mathematically this is needed to prove associativity of comultiplication on the tensor product of two bialgebras (probably even coalgebras). There is now a threat that something like this will end up PRed. Are there tricks here to make this slightly less convoluted?

[Kevin Buzzard]

Oh, I've just noticed that they use reorder4 in that code, so I should post that too (it says $(A\otimes A)\otimes(B\otimes B)=(A\otimes B)\otimes(A\otimes B)$)

-- Define the linear equivalence of (A1 ⊗[R] A1) ⊗[R] (A2 ⊗[R] A2) and
-- (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2)
private noncomputable def reorder4 : (A1 ⊗[R] A1) ⊗[R] A2 ⊗[R] A2 ≃ₗ[R]
  (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2 :=
  LinearEquiv.ofLinear
    ((TensorProduct.assoc R A1 A2 (A1 ⊗[R] A2)).symm.toLinearMap ∘ₗ
      (TensorProduct.assoc R A2 A1 A2).toLinearMap.lTensor A1 ∘ₗ
      ((TensorProduct.comm R A1 A2).rTensor A2).lTensor A1 ∘ₗ
      (TensorProduct.assoc R A1 A2 A2).symm.toLinearMap.lTensor A1 ∘ₗ
      (TensorProduct.assoc R A1 A1 (A2 ⊗[R] A2)).toLinearMap)
    ((TensorProduct.assoc R A1 A1 (A2 ⊗[R] A2)).symm.toLinearMap ∘ₗ
      (TensorProduct.assoc R A1 A2 A2).toLinearMap.lTensor A1 ∘ₗ
      ((TensorProduct.comm R A2 A1).rTensor A2).lTensor A1 ∘ₗ
      (TensorProduct.assoc R A2 A1 A2).symm.toLinearMap.lTensor A1 ∘ₗ
      (TensorProduct.assoc R A1 A2 (A1 ⊗[R] A2)).toLinearMap)
    (by aesop) (by aesop)

[Kevin Buzzard]

This is the algebra underlying the statement that the product of two group schemes is a group scheme. Is it OK to be completely out of control like this? The first def probably hits the Gouezel bound for number of lines needed in order to start asking the author of the PR to put comments in the code. Here the comments are all "I'm moving a bracket"

[Antoine Chambert-Loir]

It's funny how that statement is clear if you speak functorially.

[Kevin Buzzard]

Yes!

[Kevin Buzzard]

But in fact the main point of their project was to prove that a commutative Hopf algebra gave a group scheme, and to prove this you need to prove that inverse (defined as a linear map in the Hopf algebra file) is an algebra morphism, and to prove this you need tensor product of coalgebras (apparently)

[Ruben Van de Velde]

I would recommend open TensorProduct

[Antoine Chambert-Loir]

I believe people in monoidal category theory know how to do that: for any parenthesed word using bitensor products, you associate some type, and there are associativity and commutativity isomorphisms which relate them, compatibly.

[Ruben Van de Velde]

It seems they construct the equiv from maps left-to-right and right-to-left. Could it be a composition of equivs instead? (I can't tell, my eyes glaze over)

[Antoine Chambert-Loir]

Yes and no. There is no LinearEquiv.rTensor in mathlib. (I needed it last week…)

[Antoine Chambert-Loir]

Of course, it's no more than

variable {R M N P : Type*} [CommSemiring R]
  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P]

noncomputable def LinearEquiv.rTensor (e : M ≃ₗ[R] N)   :
    M ⊗[R] P ≃ₗ[R] N ⊗[R] P := TensorProduct.congr e (refl R P)

[Geoffrey Irving]

Is this just by ring if you build up some surrounding theory? I.e., do tensor products form the multiplication part of a commutative semiring? Or I suppose one could use just abel if tensor products form an abelian group?

[Geoffrey Irving]

(This would of course require descending to the quotient type of isomorphism classes.)

[Geoffrey Irving]

Ah, but it's supposed to be a def, of course. :/

[Antoine Chambert-Loir]

If mathlib had HoTT, it would by by abel.

[Antoine Chambert-Loir]

But mathlib has docs#CategoryTheory.FreeMonoidalCategory so it should be possible to use that.

[Eric Wieser]

Are you aware of docs#TensorProduct.tensorTensorTensorComm ? I think that's precisely your reorder4.

[Eric Wieser]

tensorTensorTensorTensorTensorTensorComm is indeed missing

[Eric Wieser]

But I don't think we need it, it's trivial by combining the 4-ary one with itself

[Eric Wieser]

I think I remember a tactic that would produce arbitrary Equivs for permuting products; LinearEquivs for TensorProduct would be a natural extension

[Anatole Dedecker]

I think this kind of thing is precisely why we want IsTensorProduct ?

[Eric Wieser]

I don't see how that would help here?

[Eric Wieser]

Note also that spelling everything out explicitly makes it easier to generalize to the heterogeneous base change case

[Eric Wieser]

Eric Wieser said:

But I don't think we need it, it's trivial by combining the 4-ary one with itself

Like so:

import Mathlib

variable (R A1 A2) [CommSemiring R] [Semiring A1] [Semiring A2] [Algebra R A1] [Algebra R A2]

open scoped TensorProduct

private noncomputable def reorder6 :
    (A1 ⊗[R] A2) ⊗[R] (A1 ⊗[R] A2) ⊗[R] A1 ⊗[R] A2 ≃ₗ[R]
      (A1 ⊗[R] A1 ⊗[R] A1) ⊗[R] A2 ⊗[R] A2 ⊗[R] A2 :=
  TensorProduct.congr (.refl _ _) (TensorProduct.tensorTensorTensorComm _ _ _ _ _)
    ≪≫ₗ TensorProduct.tensorTensorTensorComm _ _ _ _ _

-- How reorder acts elementwise
lemma reorder6_tmul (a1 a2 a3 : A1) (b1 b2 b3 : A2) :
    reorder6 R A1 A2 ((a1 ⊗ₜ[R] b1) ⊗ₜ[R] (a2 ⊗ₜ[R] b2) ⊗ₜ[R] (a3 ⊗ₜ[R] b3)) =
      (a1 ⊗ₜ[R] a2 ⊗ₜ[R] a3) ⊗ₜ[R] (b1 ⊗ₜ[R] b2 ⊗ₜ[R] b3) :=
  rfl

[Kim Morrison]

It does seem like one should define tensorList : List C \to C in any monoidal category (indeed, making it a monoidal functor), and tensorMultiset : Multiset C \to C in braided category, along with the isomorphism between tensorList L and tensorMultiset L.toMultiset (or however you spell that).

[Kim Morrison]

Then whenever you have two lists which are permutations, you would get an isomorphism between their tensor products.

[Kim Morrison]

(And in a symmetric category you would get "the" isomorphism.)

[Kevin Buzzard]

Antoine Chambert-Loir said:

If mathlib had HoTT, it would by by abel.

There's more than one isomorphism; here we really do need to say what we want rather than asking a machine to find it with a tactic (because it might find the wrong thing)

[Michael Stoll]

You could define the more general isomorphism $(A_1 \otimes A_2) \otimes (A_3 \otimes A_4) \otimes (A_5 \otimes A_6) \cong (A_1 \otimes A_3 \otimes A_5) \otimes (A_2 \otimes A_4 \otimes A_6)$ first and automatically (there is only one choice that always works, I'd think) and then specialize.

[Yuma Mizuno]

I think the following is a preliminary question: Given a permutation of a list, is it possible by some theorem or tactic of mathlib to rewrite it as a composition of adjacent transpositions?

[Antoine Chambert-Loir]

docs#Equiv.Perm.mem_closure_isSwap is close to that.

[Eric Wieser]

Michael Stoll said:

You could define the more general isomorphism $(A_1 \otimes A_2) \otimes (A_3 \otimes A_4) \otimes (A_5 \otimes A_6) \cong (A_1 \otimes A_3 \otimes A_5) \otimes (A_2 \otimes A_4 \otimes A_6)$ first and automatically (there is only one choice that always works, I'd think) and then specialize.

my construction above works for this case too with no change after the :=

[Eric Wieser]

Yuma Mizuno said:

I think the following is a preliminary question: Given a permutation of a list, is it possible by some theorem or tactic of mathlib to rewrite it as a composition of adjacent transpositions?

I guess this would be a data-carrying version of List.sorted?

[Kevin Buzzard]

@Eric Wieser can you do the R-algebra version too? Should this stuff be PRed?

[Kevin Buzzard]

import Mathlib

open TensorProduct

def foo (R : Type) [CommRing R] {A B C D E F : Type*} [Ring A] [Ring B] [Ring C]
    [Ring D] [Ring E] [Ring F] [Algebra R A] [Algebra R B] [Algebra R C]
    [Algebra R D] [Algebra R E] [Algebra R F] :
    (A ⊗[R] B) ⊗[R] (C ⊗[R] D) ⊗[R] (E ⊗[R] F) ≃ₐ[R] (A ⊗[R] C ⊗[R] E) ⊗[R] (B ⊗[R] D ⊗[R] F) := by
  sorry

[Eric Wieser]

We should have docs#Algebra.TensorProduct.tensorTensorTensorComm if we don't already, but I don't think mathlib wants the 6-way one

[Eric Wieser]

Unfortunately defining that isomorphism is very typeclass-cursed:

import Mathlib

open TensorProduct

def Algebra.TensorProduct.tensorTensorTensorComm.{uR, uA, uM, uN, uP, uQ}
    (R : Type uR) (A : Type uA) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ)
    [CommSemiring R] [CommSemiring A] [Algebra R A] [Semiring M] [Algebra R M] [Algebra A M] [IsScalarTower R A M] [Semiring N] [Algebra R N] [Semiring P] [Algebra R P] [Algebra A P] [IsScalarTower R A P] [Semiring Q] [Algebra R Q] :
    letI i : Semiring ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
    letI i : Algebra A ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
    letI i : Semiring ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
    letI i : Algebra A ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
    (M ⊗[R] N) ⊗[A] P ⊗[R] Q ≃ₐ[A] (M ⊗[A] P) ⊗[R] N ⊗[R] Q :=
  letI i : Semiring ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
  letI i : Algebra A ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
  letI i : Semiring ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
  letI i : Algebra A ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
  AlgEquiv.trans
    (AlgEquiv.trans (AlgEquiv.symm (Algebra.TensorProduct.assoc R A A (M ⊗[R] N) P Q))
      (Algebra.TensorProduct.congr (AlgEquiv.symm (sorry /- Algebra.TensorProduct.rightComm R A M P N -/)) 1))
    (AlgebraTensorModule.assoc R R A (M ⊗[A] P) N Q)

[Eric Wieser]

The proof is just copied from the module version, but the letIs are all needed

[Damiano Testa]

... and you are calling the variables i for improved presentation, right? :smile:

[Ruben Van de Velde]

There is no "I" in... Wait

[Richard Copley]

@Eric Wieser, is that illustrative/aspirational, or do you have an environment where it typechecks? (In Mathlib4, Algebra.TensorProduct.assoc only has four parameters (a ring R and three R-modules))

[Richard Copley]

a commutative semiring R, two R-algebras (on semirings), and a semiring, rather

[Eric Wieser]

I thought that type checked for me, but maybe it crashed

[Eric Wieser]

Either way, the point is the fact that I had to fight TC search to even state it

[Eric Wieser]

Here's the non-aspirational version:

import Mathlib

set_option autoImplicit false

suppress_compilation

open TensorProduct

universe uR uA uM uN uP uQ
variable (R : Type uR) (A : Type uR) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ)

def Algebra.TensorProduct.tensorTensorTensorComm
    [CommSemiring R] [CommSemiring A] [Algebra R A] [Semiring M] [Algebra R M] [Algebra A M] [IsScalarTower R A M] [Semiring N] [Algebra R N] [Semiring P] [Algebra R P] [Algebra A P] [IsScalarTower R A P] [Semiring Q] [Algebra R Q] :
    letI : Semiring ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
    letI : Algebra A ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
    letI : Semiring ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
    letI : Algebra A ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
    (M ⊗[R] N) ⊗[A] P ⊗[R] Q ≃ₐ[A] (M ⊗[A] P) ⊗[R] N ⊗[R] Q :=
  letI : Semiring ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
  letI : Algebra A ((M ⊗[R] N) ⊗[A] P ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := A) (A := M ⊗[R] N) (B := P ⊗[R] Q)
  letI : Semiring ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.instSemiring (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
  letI : Algebra A ((M ⊗[A] P) ⊗[R] N ⊗[R] Q) := Algebra.TensorProduct.leftAlgebra (S := A) (R := R) (A := M ⊗[A] P) (B := N ⊗[R] Q)
  AlgEquiv.ofLinearEquiv
    (AlgebraTensorModule.tensorTensorTensorComm R A M N P Q)
    rfl
    (by rw [←LinearEquiv.coe_toLinearMap, LinearMap.map_mul_iff]; ext; rfl)

[Richard Copley]

Nice, thanks.

[Eric Wieser]

Of course, if you are looking for more aspiration you could try and put a third ring into docs#AlgebraTensorModule.tensorTensorTensorComm, so that the linear equiv is B-linear

[Kevin Buzzard]

Yesterday I was thinking "let's PR some of this stuff" but now I'm thinking I should just see what's needed for the application; I've learnt several tips in this thread. Thanks!

[Yuma Mizuno]

BTW, I was able to make a good illustration expnaining of what is going on in the Eric's definition using the string diagram widget.
tensortensor0.png
tensortensor1.png

import Mathlib.Tactic.Widget.StringDiagram
import ProofWidgets.Component.Panel.SelectionPanel
import ProofWidgets.Component.Panel.GoalTypePanel
import Mathlib.Algebra.Category.AlgebraCat.Symmetric

-- In ymizuno-string branch

noncomputable
section

open ProofWidgets
open CategoryTheory
open MonoidalCategory

universe u

variable {R : Type u} [CommRing R]

def tensorTensorTensorComm (A B C D : AlgebraCat R) : (A ⊗ B) ⊗ (C ⊗ D) ⟶ (A ⊗ C) ⊗ (B ⊗ D) :=
  𝟙 _ ⊗≫ A ◁ (β_ B C).hom ▷ D ⊗≫ 𝟙 _

def foo (A B C D E F : AlgebraCat R) : (A ⊗ B) ⊗ (C ⊗ D) ⊗ (E ⊗ F) ⟶ (A ⊗ C ⊗ E) ⊗ (B ⊗ D ⊗ F) :=
  𝟙 _ ⊗≫ (A ⊗ B) ◁ tensorTensorTensorComm C D E F ⊗≫ tensorTensorTensorComm _ _ _ _
  -- Alternatively, we can use the following as suggested by the string diagram:
  -- 𝟙 _ ⊗≫
  -- A ◁ B ◁ C ◁ (β_ D E).hom ▷ F ⊗≫
  -- A ◁ (β_ B C).hom ▷ E ▷ D ▷ F ⊗≫
  -- A ◁ C ◁ (β_ B E).hom ▷ D ▷ F ⊗≫ 𝟙 _

example  (A B C D E F : AlgebraCat R) : foo A B C D E F = sorry := by
  dsimp only [foo, tensorTensorTensorComm]
  with_panel_widgets [GoalTypePanel]
  with_panel_widgets [SelectionPanel]
    rw [BraidedCategory.braiding_tensor_right]
    sorry

[Eric Wieser]

I'm not sure that is actually showing my definition (which uses a 4-ary permutation twice)

[Eric Wieser]

But it is cool!

[Eric Wieser]

I'm curious if that node with three inputs and outputs is how this would be drawn on paper

[Ruben Van de Velde]

I think that needs origami

[Yuma Mizuno]

Eric Wieser said:

I'm not sure that is actually showing my definition (which uses a 4-ary permutation twice)

Ah, yes, dsimp was expanding the definition. The original definition is like:
tensortensor2.png

Unfortunately, some lines are overlapping.

[Gareth Ma]

Just want to say this is very very very very cool <3