Self-Introduction

Stream: new members

[Ingo Runkel]

Hi, my Name is Ingo Runkel and I work at the Math Department in Hamburg. We did run a beginners seminar on Lean to get to know the basics, and to practice it more I am trying to put some simple things about Hopf algebras into Lean (https://github.com/irunkel/HopfAlgebras). As expected, there are many small and (to me) big issues, and I would be happy to get some hints.
Here is a small one: The convolution algebra on a Hopf algebra H over R is build from linear endomorphism on H. I wanted to hide R and H, but it seems to be necessary to provide them anyway in many places, e.g.:

import Mathlib.LinearAlgebra.Basic
import Mathlib.LinearAlgebra.TensorProduct.Basic

open TensorProduct

variable {R:Type} [CommSemiring R]
variable {H:Type} [AddCommMonoid H] [Module R H]

def convAlg : Type := LinearMap (RingHom.id R) H H
-- fails (typeclass instance problem is stuck):
-- instance : AddCommMonoid convAlg := inferInstanceAs (AddCommMonoid (LinearMap (RingHom.id R) H H))
-- works:
instance : AddCommMonoid (@convAlg R _ H _ _) := inferInstanceAs (AddCommMonoid (LinearMap (RingHom.id R) H H))
instance : Module R (@convAlg R _ H _ _) := inferInstanceAs (Module R (LinearMap (RingHom.id R) H H))
-- fails (typeclass instance problem is stuck):
-- noncomputable def convAlg_mul : convAlg ⊗[R] convAlg →ₗ[R] convAlg := sorry
-- works:
noncomputable def convAlg_mul : (@convAlg R _ H _ _) ⊗[R] (@convAlg R _ H _ _) →ₗ[R] (@convAlg R _ H _ _) := sorry

[Johan Commelin]

cc @Kevin Buzzard

[Kevin Buzzard]

Re your code: you should probably make R and H explicit in your variables, and make convAlg an abbrev not a def, because then typeclass inference can see through the definition and then you probably won't need all the instances.

I have students at Imperial working on Hopf algebras so it might be best to coordinate.

[Ingo Runkel]

Kevin Buzzard said:

Re your code: you should probably make R and H explicit in your variables, and make convAlg an abbrev not a def, because then typeclass inference can see ...

Thank you. Yes, in the code above one no longer needs the instances if one uses abbrev, but one still needs to write @convAlg R _ H _ _ rather than just convAlg, at least in the snippet above.
One reason I went with def was that I actually did not want Lean to find all the pre-set instances. E.g. End(H) is already an algebra with respect to composition, but that is not the algebra structure I want and I was not sure if the two would interfere.

import Mathlib.Algebra.Algebra.Basic

variable {R:Type} [CommSemiring R]
variable {H:Type} [AddCommMonoid H] [Module R H]

abbrev convAlg : Type := LinearMap (RingHom.id R) H H

#check inferInstanceAs (Algebra R convAlg)

The Hopf algebra project is more of a hobby for me and I am not really planning to get to a specific point, but I would indeed by interested to see what your student is doing and how, if your student does not mind.

[Kevin Buzzard]

There are ten open mathlib4 PRs by user 101damnations, most of them blocked by earlier PRs, but there you can see what's happening

[Ingo Runkel]

Thank you, I will have a look.