Proving a statement about Hopf Algebras

Stream: new members

[Sam Ezeh]

import Aesop
import Mathlib.Algebra.Algebra.Basic
import Mathlib.RingTheory.Bialgebra
import Mathlib.RingTheory.HopfAlgebra

example [CommSemiring R] [CommSemiring A] [H : HopfAlgebra R A] :
  (LinearMap.mul' R A)
  ∘ₗ (LinearMap.mul' R A).lTensor A
  ∘ₗ (TensorProduct.assoc R A A A)
  ∘ₗ H.comul.rTensor A
  ∘ₗ TensorProduct.map (LinearMap.mul' R A) H.antipode
  ∘ₗ (TensorProduct.assoc R A A A).symm
  ∘ₗ H.comul.lTensor A
  =
  (LinearMap.mul' R A)
  ∘ₗ (TensorProduct.comm R A A)
  ∘ₗ (LinearMap.mul' R A).lTensor A
  ∘ₗ (TensorProduct.assoc R A A A)
  ∘ₗ H.comul.rTensor A
:= by
  sorry

I think the statement's correct and the first thing I want to do is rewrite H.comul.rTensor A ∘ₗ TensorProduct.map (LinearMap.mul' R A) H.antipode as TensorProduct.map (H.comul ∘ₗ LinearMap.mul' R A) H.antipode. Once I've done this, I'd like touse mul_compr₂_comul to get TensorProduct.map ((LinearMap.mul' R _) ∘ₗ (TensorProduct.map H.comul H.comul)) H.antipode. However, all the bialgebra laws use LinearMap.mul instead of LinearMap.mul' and they use the compr₂ variants instead of TensorProduct.map which might suggest that I'm writing this weirdly, is there a better way to state this?

Another thing is the hopf algebra laws use LinearMap.mul' and LinearMap.lTensor/LinearMap.rTensor instead of LinearMap.mul and compr₂, am I missing a way to make the two definitions work nicely together?

[Kevin Buzzard]

@Edison Xie @Jujian Zhang you have both been thinking about this stuff recently

[Eric Wieser]

Sam Ezeh said:

However, all the bialgebra laws use LinearMap.mul instead of LinearMap.mul' and they use the compr₂ variants instead of TensorProduct.map which might suggest that I'm writing this weirdly, is there a better way to state this?

Another thing is the hopf algebra laws use LinearMap.mul' and LinearMap.lTensor/LinearMap.rTensor instead of LinearMap.mul and compr₂, am I missing a way to make the two definitions work nicely together?

I think it would be very reasonable to add some more Bialgebra lemmas that convert the existing statements to these statements

[Kevin Buzzard]

Your first step is

  rw [← LinearMap.comp_assoc _ _ (LinearMap.rTensor A Coalgebra.comul)] -- brackets in right place
  unfold LinearMap.rTensor -- is there no API for this?
  rw [← map_comp] -- :tada
  rw [LinearMap.id_comp] -- simplify

but I have no idea about all this compr/compl stuff. I do know that @Eric Wieser was adamant that the statement of the bialgebra axiom needed to be changed from comul (a * b) = comul a * comul b (the original choice) to (LinearMap.mul R A).compr₂ comul = (LinearMap.mul R (A ⊗[R] A)).compl₁₂ comul comul but I have no understanding of why this is better, all I know is that Eric understands this stuff much better than me so I trusted him.

I will also say that this question took me several minutes to even parse: the lack of a commutative diagram widget (even though it's been advertised on FRO slides for months if not years) is really painful here.

[Sam Ezeh]

Kevin Buzzard said:

I will also say that this question took me several minutes to even parse: the lack of a commutative diagram widget (even though it's been advertised on FRO slides for months if not years) is really painful here.

What is the state of this? Are there people working on it? My motivation for working with Hopf Algebras is precisely for my graphical rewriting project where I want to build a proof of concept for string diagrams: https://github.com/dignissimus/Untangle

[Eric Wieser]

Even when it existed, it was only for statements written categorically. There is an open PR for string diagrams in monoidal categories, but this has the same shortcoming.

[Edison Xie]

Kevin Buzzard said:

Edison Xie Jujian Zhang you have both been thinking about this stuff recently

open BigOperators
set_option tactic.skipAssignedInstances false
set_option synthInstance.maxHeartbeats 50000
example (R1 : Type) (A1 : Type) [CommRing R1] [CommRing A1] [H : HopfAlgebra R1 A1] :
  (LinearMap.mul' R1 A1)
  ∘ₗ (LinearMap.mul' R1 A1).lTensor A1
  ∘ₗ (TensorProduct.assoc R1 A1 A1 A1)
  ∘ₗ H.comul.rTensor A1
  ∘ₗ TensorProduct.map (LinearMap.mul' R1 A1) H.antipode
  ∘ₗ (TensorProduct.assoc R1 A1 A1 A1).symm
  ∘ₗ H.comul.lTensor A1
  =
  (LinearMap.mul' R1 A1)
  ∘ₗ (TensorProduct.comm R1 A1 A1)
  ∘ₗ (LinearMap.mul' R1 A1).lTensor A1
  ∘ₗ (TensorProduct.assoc R1 A1 A1 A1)
  ∘ₗ H.comul.rTensor A1
:= by
  rw [← LinearMap.comp_assoc _ _ (LinearMap.rTensor A1 Coalgebra.comul)] -- brackets in right place
  unfold LinearMap.rTensor -- is there no API for this?
  rw [← TensorProduct.map_comp] -- :tada
  rw [LinearMap.id_comp] -- simplify

  ext a b
  simp only [TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
    LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply,
    LinearMap.lTensor_tmul, LinearMap.rTensor_tmul]
  obtain ⟨I1, x1, x2, hx⟩ := HopfPoints.comul_repr R1 A1 a
  obtain ⟨I2, y1, y2, hy⟩ := HopfPoints.comul_repr R1 A1 b
  simp (config := { zetaDelta := true, zeta := false }) only [hy, TensorProduct.tmul_sum, map_sum,
    TensorProduct.assoc_symm_tmul, TensorProduct.map_tmul, LinearMap.mul'_apply,
    LinearMap.rTensor_tmul, Bialgebra.comul_mul, hx, TensorProduct.sum_tmul,
    TensorProduct.assoc_tmul, LinearMap.lTensor_tmul, TensorProduct.comm_tmul,
    LinearMap.id_coe,id_eq]
  simp only [LinearMap.coe_comp, comp_apply, LinearMap.mul'_apply, Bialgebra.comul_mul]
  obtain ⟨I11, y11, y12, hy1⟩ := HopfPoints.comul_repr R1 A1 (y1 x)
  sorry

I attempted this but failed, but i think the general idea is using sweedler to open everything up then it should be clear using some properties of antipode :(

[Eric Wieser]

What's the statement of HopfPoints.comul_repr?

[Jujian Zhang]

I think it is saying that $comul(a) = \sum_{i \in I}, a_1 i \otimes a_2 i$ for some inex set $I$ and coordinate function $a_1, a_2$

[Sam Ezeh]

Eric Wieser said:

I think it would be very reasonable to add some more Bialgebra lemmas that convert the existing statements to these statements

Would these be welcome?

lemma mul'_comp_comul [CommSemiring R] [Semiring A] [B : Bialgebra R A] : LinearMap.mul' R _ ∘ₗ  TensorProduct.map B.comul B.comul = B.comul ∘ₗ LinearMap.mul' R A := by
  ext
  simp

lemma mul'_comp_counit [CommSemiring R] [Semiring A] [B : Bialgebra R A] : LinearMap.mul' R _ ∘ₗ  TensorProduct.map B.counit B.counit = B.counit ∘ₗ LinearMap.mul' R _:= by
  ext
  simp

lemma lift_map_eq_lift_compl₁₂
  [CommSemiring R]
  [Semiring A] [Semiring B] [Semiring C]
  [Semiring D] [Semiring E] [Semiring F]
  [Semiring G] [Semiring H]
  [Module R A] [Module R B] [Module R C]
  [Module R D] [Module R E] [Module R F]
  [Module R G] [Module R H]
  {f : B ⊗[R] C →ₗ[R] E ⊗[R] F →ₗ[R] G ⊗[R] H}
  {g : A →ₗ[R] B ⊗[R] C}
  {h : D →ₗ[R] E ⊗[R] F}
: TensorProduct.lift f ∘ₗ TensorProduct.map g h = TensorProduct.lift (f.compl₁₂ g h) := by
  ext
  simp

lemma comp_lift_eq_lift_compr₂
  [CommSemiring R]
  [Semiring A] [Semiring B] [Semiring C] [Semiring D]
  [Module R A] [Module R B] [Module R C] [Module R D]
  {f : A →ₗ[R] B →ₗ[R] C}
  {g : C →ₗ[R] D}
: g ∘ₗ TensorProduct.lift f = TensorProduct.lift (f.compr₂ g) := by
  ext
  simp

[Eric Wieser]

I think some of those assumptions are too strong; I doubt you need your modules to be semirings?

[Eric Wieser]

Otherwise they look fine