Coalgebras/bialgebras/Hopf algebras

Stream: maths

[Amelia Livingston]

Does anyone have any thoughts on how these objects should be set up? I've tried several configurations for coalgebras and bialgebras and there's always something a little ugly. I've settled on making them classes and I'm keen to get bialgebra to extend coalgebra, for no reason other than personal taste. I'm just messing around with this stuff; I want to mention them in a talk on Thursday.

[Johan Commelin]

I can imagine it quickly gets ugly. On paper we very quickly suggest to a very suggestive notation.

[Johan Commelin]

https://en.wikipedia.org/wiki/Coalgebra#Sweedler_notation

[Johan Commelin]

But this seems very hard to mimic in Lean.

[Kalle Kytölä]

Sweedler's notation is indeed very useful, and looks scary for formalization.

But is that absolutely horrible to mimick in Lean? Sweedler's notation of course amounts to choosing non-canonical expressions for the coproducts of all elements (indexed collections of $a_{(1)}$'s and $a_{(2)}$'s for every $a$), but maybe even choice can do that. Lemmas are true for the appropriate sums of such non-canonical choices, so that doesn't look too bad as such. And one certainly wants separate non-canonical representations for iterated coproducts, but still one can set up lemmas to translate between these. (In the worst case one will then have to juggle such coassociativity lemmas just like one would do with associativity lemmas without ring, which would indeed be bad. Do we need a coring tactic?)

I of course haven't tried, but I'm optimistically hoping that it looks even scarier than it ends up being. :big_smile:

[Johan Commelin]

Maybe you can get quite far with appropriate induction lemmas? But it would need some engineering to get a usable system, I guess.

[Kalle Kytölä]

I also expect that a lot of engineering would be needed.

Probably one anyway wants to avoid working with elements as much as possible (and therefore avoid Sweedler notation as much as possible). (Sure, at times Sweedler's notation might really be the easiest way, but other times it is just used out of habit.) So in parallel to engineering Sweedler's notation, maybe this area would also benefit from engineering for good ways to compose multilinear maps in flexibly specified (diagrammatic?) ways?

[Junyan Xu]

@Vasily Ilin tried to construct the Hopf algebra structure on K[X] last April-May, but seemed to give up (due to timeouts/slowness?) and apparently then switched to defining affine group schemes using representable functors. Not sure what lessons came out of it ... here are some relevant threads:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20structure.20vs.20class/near/282163086
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/refactoring.20proofs
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/get.20the.20two.20maps.20from.20an.20isomorphism

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20algebra.20maps.20takes.201.20to.201
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20.60calc.60.20block
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/deterministic.20timeout.20on.20definition.20of.20structure

[Vasily Ilin]

https://github.com/leomayer1/Hopf/tree/master/src
Here is the repo with our attempt!

[Junyan Xu]

Oh nice! You did finish checking K[X]'s Hopf algebra structure without sorries.

[Kevin Buzzard]

@Amelia Livingston what did you not like about that approach? Like sheaves of modules I can quite believe that each approach has advantages and disadvantages.

[Amelia Livingston]

I had just seen Scott Morrison's comment that coalgebras and bialgebras should be defined first so was having a go at that. But I hadn't read all of these threads so thank you! And I've been using the functor definition too - wanted to compare them and show they're equivalent

I've had a little go at using Sweedler notation because I think it might improve organisation in my coalgebra/bialgebra stuff, but I haven't finished setting it up.

[Amelia Livingston]

FWIW Vasily if you do want to PR your work, I'm not looking to PR mine - just wanted to roll my own (for a talk I'm now too ill to give) and so I know what's going on, and then use it for more specific things, which I maybe would PR.

[Kevin Buzzard]

I would like to see group schemes in mathlib because they're a huge source of very nice results and you don't need any of the theory of varieties to set them up

[Amelia Livingston]

I think Joël Riou has some cool work on internal objects in categories here I was hoping might get PR'ed someday, as explained here

[Pedro Sánchez Terraf]

Amelia Livingston said:

I had just seen Scott Morrison's comment that coalgebras and bialgebras should be defined first so was having a go at that.

One (most probably superfluous) remark: There's a bunch of "general coalgebra" stuff (as in "general/universal algebra") in CS, so I understand the classical coalgebra will be under some appropriate namespace.

[Eric Wieser]

I doubt that will be the case; coalgebra would probably end up in the root namespace like algebra is.

[Eric Wieser]

Thanks to @Ali Ramsey, we now have docs#Coalgebra !

[Kevin Buzzard]

So bialgebras next and then Hopf algebras?

[Yaël Dillies]

Is it really called "conunitality" in the literature?

[Johan Commelin]

That must be a typo

[Kyle Miller]

fixed the typo: #8874

[Eric Wieser]

It looks like you based it on the version that the docs were built from and not master, and picked up a merge conflict as a result.

[Kyle Miller]

Oops. I tried doing this quickly by using the github interface rather than pulling mathlib locally...

[Patrick Massot]

Was there any progress on the Sweedler notation in Lean question?

[Kevin Buzzard]

@Edison Xie ?

[Kevin Buzzard]

(who is doing exams right now)

[Edison Xie]

Hi! Yes I’ve got sweeter notation in my project (on a branch in FLT) but it’s super old and recently someone pointed out that my work is not yet in mathlib so I might spend some time clean it up and PR it after Big Proof 2025

[Edison Xie]

(Sorry was revising didn’t check Zulip messages)

[Yaël Dillies]

Edison's Sweedler notation will be used in Toric soon

[Patrick Massot]

@Edison Xie could you share a link to your code? It doesn’t matter that it’s not ready, I only want to see how it looks like.

[Edison Xie]

you mean something like this?

import Mathlib
suppress_compilation

section Coalgebra

variable {R A : Type*} [CommSemiring R]
variable [AddCommMonoid A] [Module R A] [Coalgebra R A]
open TensorProduct Coalgebra

lemma exists_repr (x : A) :
    ∃ (I : Finset (A ⊗[R] A)) (x1 : A ⊗[R] A → A) (x2 : A ⊗[R] A → A),
    Coalgebra.comul x = ∑ i ∈ I, x1 i ⊗ₜ[R] x2 i := by
  classical
  have mem1 : comul x ∈ (⊤ : Submodule R (A ⊗[R] A)) := ⟨⟩
  rw [← TensorProduct.span_tmul_eq_top, Submodule.mem_span_set] at mem1
  obtain ⟨r, hr, (eq1 : ∑ i ∈ r.support, (_ • _) = _)⟩ := mem1
  choose a a' haa' using hr
  replace eq1 := calc _
    comul x = ∑ i ∈ r.support, r i • i := eq1.symm
    _ = ∑ i ∈ r.support.attach, (r i : R) • i.1 := Finset.sum_attach _ _ |>.symm
    _ = ∑ i ∈ r.support.attach, (r i • a i.2 ⊗ₜ[R] a' i.2) :=
        Finset.sum_congr rfl fun i _ ↦ congr(r i.1 • $(haa' i.2)).symm
    _ = ∑ i ∈ r.support.attach, ((r i • a i.2) ⊗ₜ[R] a' i.2) :=
        Finset.sum_congr rfl fun i _ ↦ TensorProduct.smul_tmul' _ _ _
  refine ⟨r.support, fun i ↦ if h : i ∈ r.support then r i • a h else 0,
    fun i ↦ if h : i ∈ r.support then a' h else 0, eq1 ▸ ?_⟩
  conv_rhs => rw [← Finset.sum_attach]
  exact Finset.sum_congr rfl fun _ _ ↦ (by aesop)

/-- an arbitrarily chosen indexing set for comul(a) = ∑ a₁ ⊗ a₂. -/
def ℐ (a : A) : Finset (A ⊗[R] A) := exists_repr a |>.choose

/-- an arbitrarily chosen first coordinate for comul(a) = ∑ a₁ ⊗ a₂. -/
def Δ₁ (a : A) : A ⊗[R] A → A := exists_repr a |>.choose_spec.choose

/-- an arbitrarily chosen second coordinate for comul(a) = ∑ a₁ ⊗ a₂. -/
def Δ₂ (a : A) : A ⊗[R] A → A :=
  exists_repr a |>.choose_spec.choose_spec.choose

lemma comul_repr (a : A) :
    Coalgebra.comul a = ∑ i ∈ ℐ a, Δ₁ a i ⊗ₜ[R] Δ₂ (R := R) a i :=
  exists_repr a |>.choose_spec.choose_spec.choose_spec

end Coalgebra

[Eric Wieser]

Could this just be an induction principle for tensor products?

[Eric Wieser]

induction h : comul a using TensorProduct.sum_induction or similar?

[Patrick Massot]

I thought you meant the Sweedler notation without sums. But I’ll check with the people who are actually interested in this (I was asked this question by people in Hamburg).

[Michał Mrugała]

I thought we already have some Sweedler’s notation in mathlib, but yes it uses sums. See docs#Coalgebra.Repr

[Patrick Massot]

Now I’m rather confused, but it’s probably coming from the fact I don’t know anything about Hopf algebras. What is the relation between @Edison Xie ’s code and docs#Coalgebra.Repr.arbitrary ?

[Michał Mrugała]

Unless I'm misuderstanding something, they seem like essentially the same thing. My impresssion was that Repr was introduced in Edison and Amelia's work to function as Sweedler's notation. I think there is some confusion about what did and didn't make it to mathlib from their work (for example anticommutativity of the antipode didn't make it).

[Patrick Massot]

That would explain why I’m confused.

[Patrick Massot]

Maybe I’ll get more information if I ask more specific questions and write some code. @Ingo Runkel in Hamburg was telling me he really needed something called Sweedler’s notation and that I’ve never heard of. I search zulip and found this thread. Then I asked Ingo to give one example of an easy computation using this notation. He said that in a Hopf algebra you have, $∀ h, ε(S(h)) = ε(h)$, and provided a very short proof. I didn’t find this lemma in Mathlib, but I was able to write:

import Mathlib.RingTheory.HopfAlgebra.Basic

variable {R A : Type*} [CommRing R]
variable [Ring A] [HopfAlgebra R A]
open TensorProduct Coalgebra HopfAlgebra Bialgebra

lemma sum_counit_mul_eq (h : A) :
    ∑ x ∈ (ℛ R h).index, counit (R := R) ((ℛ R h).left x) • (ℛ R h).right x = h := by
  have := sum_counit_tmul_eq  (R := R) (ℛ R h)
  apply_fun lift (LinearMap.lsmul R A) at this
  simp_rw [map_sum] at this
  convert this
  simp

lemma antipode_counit (h : A) : counit (R := R) (antipode (R := R) h) = counit (R := R) h := by
  have := sum_mul_antipode_eq_smul (R := R) (ℛ R h)
  apply_fun counit (R := R) at this
  simp_rw [map_smul, counit_one, smul_eq_mul, mul_one, map_sum, counit_mul,
           ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_mul_eq] at this
  exact this

[Patrick Massot]

This is really close to the proof Ingo sent me. So maybe the conclusion is that some workable version of Sweedler is indeed already in Mathlib, although it would be nice to have something lighter than (ℛ R h).left.

[Patrick Massot]

Now here is my question: how are we meant to use Hopf algebra without all those (R := R)? If this isn’t possible, why is R an implicit argument to counit and antipode?

[Patrick Massot]

Other question: is my first lemma really missing? Is lift (LinearMap.lsmul R A) really missing?

[Patrick Massot]

The later is the scalar multiplication as a linear map from $R \otimes A$ to $A$.

[Michał Mrugała]

On a side note, it’s worth mentioning that we’re developing some API for Hopf algebras as part of Toric, which the people from Hamburg might be interested in (it’s hard to say more without knowing what they’re trying to do).

[Patrick Massot]

I don’t know what Ingo wants to do. I think he simply tried this as a Lean exercise.

[Patrick Massot]

He may tell us more later.

[Michał Mrugała]

Patrick Massot said:

Other question: is my first lemma really missing? Is lift (LinearMap.lsmul R A) really missing?

I think the latter map is expressed as (TensorProduct.mk R A R).flip 1 in docs#Coalgebra My bad this is the map in the other direction. Best I could find is docs#Algebra.TensorProduct.lid

[Michał Mrugała]

As far as I can tell the first lemma is not in mathlib. The second lemma is proved in Toric using a different method (convolution products). In general there are still a lot of fundamental results missing from mathlib.

[Eric Wieser]

Patrick Massot said:

If this isn’t possible, why is R an implicit argument to counit and antipode?

My guess is that this predates the lean 4 feature that lets us make the argument explicit

[Eric Wieser]

And I think in review I might have said it would be simpler just to wait rather than duplicating the API with implicit and explicit arguments

[Eric Wieser]

Should antipode take an R argument at all? (edit: I guess TensorProduct.antipode_def is troublesome otherwise)

[Andrew Yang]

There must be a way to write a command set_base_ring R and then some tactic magic can fill in all R with the same R. But I'm guessing we don't want this on the same basis that we didn't like parameter in lean3?

[Eric Wieser]

#25060 makes the R argument to antipode explicit

[Eric Wieser]

For comul and counit it's not so clear cut, since the type can usually be inferred

[Eric Wieser]

Then again, we seem to have survived with two unecessarily explicit type arguments to algebraMap for a long time

[Notification Bot]

A message was moved from this topic to #mathlib4 > Universe polymorphic Coalgebra instance for tensor products by Eric Wieser.

[Kevin Buzzard]

Oh I definitely want two explicit arguments to algebraMap, I use them all the time

[Eric Wieser]

Sure, but what fraction of your uses could be algebraMap _ A or algebraMap _ _?

[Andrew Yang]

Most of my algebraMaps appear unapplied (in algebraic geometry). It would be quite bad if the type of it is not shown in the infoview and I need to hover on each of them to check.
Even if Lean can figure it out, my feeble human brain cannot.

[Patrick Massot]

Andrew Yang said:

There must be a way to write a command set_base_ring R and then some tactic magic can fill in all R with the same R. But I'm guessing we don't want this on the same basis that we didn't like parameter in lean3?

That would be really really nice.

[Patrick Massot]

Note you can already do

set_option quotPrecheck false
notation "ε" => counit (R := R)

but then you don’t get a delaborator for free.

[Kevin Buzzard]

I've been using this quotPrecheck trick in FLT:

set_option quotPrecheck false in
/-- `D_𝔸` is notation for `D ⊗[K] 𝔸_K`. -/
notation "D_𝔸" => (D ⊗[K] AdeleRing (𝓞 K) K)

i.e. "I can't be bothered to write D_𝔸 D K everywhere, it just looks silly, in the LaTeX I just write let $D_{\mathbb{A}}:=D\otimes_K\mathbb{A}_K$ and I want to do this here too and write D_𝔸" and I've not run into problems with this yet.

[Yaël Dillies]

@Patrick Massot, Ingo might be interested in the last few commits to Toric:

• https://github.com/YaelDillies/Toric/commit/395b7897af77f9f45191c259731572201dfc9663: Sweedler notation lemmas
• https://github.com/YaelDillies/Toric/commit/ef54079fb1c93a04a427d217163b253ac8c90d0b: The antipode antidistributes over multiplication

[Yaël Dillies]

I've also added your proof of antipode_counit to Toric in https://github.com/YaelDillies/Toric/commit/4c9712ba94ed08ce407900e3b6d2f295cde61396

[Patrick Massot]

Thanks, but you can directly ping @Ingo Runkel, especially since my visit to Hamburg ended.