feat(LinearAlgebra/TensorAlgebra): implement HopfAlgebra for TensorAlgebra

[ntapiam]

implementation of the natural Hopf algebra structure on the TensorAlgebra

[ntapiam]

-awaiting-author

[github-actions]

PR summary 0a01e3ed11

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Bialgebra.FreeAlgebra (new file)	875
Mathlib.RingTheory.Bialgebra.TensorAlgebra (new file)	886
Mathlib.RingTheory.HopfAlgebra.TensorAlgebra (new file)	888

---

Declarations diff

+ algebraMapInv_ι
+ algebraMapInv_ι_apply
+ algebraMapInv_ι_eq_zero
+ antipode
+ antipode_algebraMap_apply
+ antipode_antihom
+ antipode_antihom_apply
+ antipode_ι_apply
+ comul
+ comul_ι
+ instHopfAlgebra
++ instBialgebra

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kckennylau]

The review is not finished (there's still a very long proof that I haven't gone over), but I think I've pointed out enough things to fix for the moment. Please ping me (@kenny Lau) on Zulip when you're done.

[kckennylau]

(MulOpposite.opLinearEquiv R): but R is commutative?

[ntapiam]

MulOpposite.opLinearEquiv R has implicit parameter {N} [AddCommMonoid N] [Module R N] so it is actually of type T[M] →ₗ[R] T[M]

[kckennylau]

I don't think you understood my point. What I meant is that R is commutative so MulOpposite.opLinearEquiv R is just the identity map.

[kckennylau]

I think I'm wrong here, it seems like you wanted to do MulOpposite for T[M].

[kckennylau]

If this is true, doesn't it mean that the antipode is just negation? In this case, it would just be LinearEquiv.neg.

[ntapiam]

This holds only on the image of ι R. For example

antipode R (ι R x * ι R y) = ι R y * ι R x

In general, for x in T[M]

antipode R ((tprod R M n) x) = (-1)^n • (tprod R M n) (fun i => x (n - i))

so there's an alternating minus sings and a reversal. I'm not sure if this is the best way to write it.

[kckennylau]

Also, welcome to Mathlib! I hope that this PR will teach you a lot about how to write better Lean/Mathlib code.

[YaelDillies]

I'm confused: Aren't you duplicating the content of Mathlib.RingTheory.HopfAlgebra.TensorProduct? Also, just so you know, there's more Hopf algebra material in Toric that's currently being upstreamed.

[ntapiam]

Thanks you both for your comments!

I'm confused: Aren't you duplicating the content of Mathlib.RingTheory.HopfAlgebra.TensorProduct? Also, just so you know, there's more Hopf algebra material in Toric that's currently being upstreamed.

@YaelDillies I think this is different as, as far as I understand, the file you mention proves that the tensor product of two Hopf algebras is again a Hopf algebra, while here I'm showing that the tensor algebra itself is a Hopf algebra where the coproduct is naturally induced by its freeness as an algebra (lift of (x : M) → ι R x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ι R x).

I'm not sure that this can be deduced from HopfAlgebra.ofAlgHom since antipode in this case is not an algebra homomorphism, but an antihomomorphism, which it always is.

It may be interesting to add those results to Mathlib.RingTheory.HopfAlgebra.Basic, maybe?

The reason I'm interested in this particular structure is that it–and its dual, the shuffle algebra–appears very frequently in my field (rough paths).

[YaelDillies]

Ah yes, thank you for the clarification. I would put this in RingTheory.HopfAlgebra.TensorAlgebra.

[ntapiam]

I could move it to a new file after the review is done.
Also, shouldn't HopfAlgebra.ofAlgHom be changed to something like HopfAlgebra.ofLinearMap since AFAIK it's very rare that antipode is actually an AlgHom.

In this file, at some point I tried defining it as antipode : T[M] →ₐ[R] T[M]ᵐᵒᵖ but that really only caused me problems because of the MulOpposites, which I didn't know how to handle, so I ended up with just T[M] →ₗ[R] T[M]. What's the preferred Mathlib way of dealing with antihoms?

[ntapiam]

-awaiting-author

[YaelDillies]

Why is the proof of this so long? Can you explain why this proof is difficult?

[ntapiam]

This may be due in part to my own incompetence with Lean/Mathlib, apologies.

The more straightforward proof uses that if A is generated as an algebra by its primitive elements, then then antipode is the unique anti alg hom such that antipode R x = -x for all primitive elements.
This is exactly the case here, but I don't know if such a result is available in Mathlib or how to use them.

Short of that, the pen-and-paper proof I know, which I tried to reproduce here (see image below), makes heavy use of Sweedler's notation, and the inductive nature of the Tensor Algebra. It then involves some juggling around with products such as the little assoc4 lemma in the proof.

Maybe this could be simplified, I tried my best.

[YaelDillies]

Could you try doing the proof involving primitive elements, to compare?

[ntapiam]

The argument is more abstract. If you know there is an antipode (in this case there is by graded connectedness), it must satisfy antipode R x = -x for all primitives. The tensor algebra is generated as an algebra by the image of ι R which is a submodule of the module of primitive elements. Therefore, any linear map f : M →ₗ[R] T[M] satisfying f ∘ₗ ι R = -ι R must be the antipode.

This argument bypasses showing the required identity altogether, so I'm not sure how difficult it would be to implement it in Mathlib.

[YaelDillies]

Try it, and come back to us if/when you get stuck 😉

[ntapiam]

-awaiting-author

[kckennylau]

Again I have not touched your long proof yet, because we haven't cleared up the definitions before.

[kckennylau]

I don't think you understood my point. What I meant is that R is commutative so MulOpposite.opLinearEquiv R is just the identity map.

[kckennylau]

Suggested change

	instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
	(by ext; simpa [comul, Algebra.TensorProduct.one_def, add_tmul, tmul_add] using by abel)
	(by ext; simp [comul, algebraMapInv])
	(by ext; simp [comul, algebraMapInv])
	instance instBialgebra : Bialgebra R T[M] := Bialgebra.ofAlgHom (comul R) algebraMapInv
	(by ext; simpa [Algebra.TensorProduct.one_def, add_tmul, tmul_add] using by abel)
	(by ext; simp)
	(by ext; simp)

Since you have the simp lemmas above, you don't need to unfold them here anymore.

[ntapiam]

for some reason I can't get it to accept just simp but I have to do simp [comul] for it to unfold the definition.

[YaelDillies]

Can you add lemmas stating these?

[ntapiam]

I added a lemma for comul. The ones for algebraMapInv should be Bialgebra.counit_*

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[hawkrobe]

It would be nice to have something like HopfAlgebra.ofAlgHom for the general case.

Feel free to write it 🙂

@ntapiam @YaelDillies @kckennylau: I opened #39785 and #39841 which lift this Sweedler proof to a general HopfAlgebra.ofPrimitives constructor so the proof could become something like:

  namespace TensorAlgebra

  open MulOpposite LinearMap

  variable (R : Type*) [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]

  instance instHopfAlgebra : HopfAlgebra R (TensorAlgebra R M) :=
    HopfAlgebra.ofPrimitives
      (lift R <| (opLinearEquiv R).toLinearMap ∘ₗ (-ι R : M →ₗ[R] _))
      (s := Set.range (ι R))
      adjoin_range_ι
      (fun p ⟨m, rfl⟩ =>
        { counit_eq_zero := by simpa using algebraMapInv_ι_apply m
          comul_eq_tmul_one_add_one_tmul := comul_ι m })
      (fun p ⟨m, rfl⟩ => by simp)

  end TensorAlgebra