Zulip Chat Archive

Stream: new members

Topic: Getting involved with mathlib

Cameron Torrance (May 07 2022 at 17:43):

I would like to get to point where I can start contributing to mathlib but I don't really know where to get started.
For the last few months I have been working on lean 3 maths library from scratch (not depending on mathlib) where I've :

1) proved choice => zorn
2) obtained some simple results about commutative rings (existence of maximal ideals, nilradical is intersection of prime ideals, first iso thm and the prime spectrum is a top space)
3) did some category theory (path cat of graph, products, colimts, defn of adjoints, wrote a slight unwieldly defn of a sheaf on top space)
4) plus some other dumb side projects.

I think I could help with some C*-algebra or Hopf algebra stuff if they aren't too far developed and really like the idea of working on some manifoldy stuff (but I doubt my diff geo courses covered enough for me to be that helpful). Where do I find what what needs working on and who is working on it?
The code I write is pretty mesy (many proofs start me repeatedly barking cases) and there are number of things I don't really understand that well (how to get typeclass inference to play nice with pi types, appropriate precedences for user defined notation, defn tactics , layout of mathlib etc.) so I think I need a fair amount of onboarding.

Kevin Buzzard (May 07 2022 at 18:01):

The best way to learn is just to get going with a project. I was talking to someone yesterday who was interested in C* algebras and lean -- here I think that @Jireh Loreaux and @Scott Morrison might know the state of the art.

Julian Berman (May 07 2022 at 18:07):

@Vasily Ilin and @Leo Mayer are working on Hopf algebras and may also welcome an extra pair of hands.

Jireh Loreaux (May 07 2022 at 18:50):

Messy code is not a problem. That can always be fixed during PR review, although you're always welcome to ask for tips on Zulip before it gets that far.

Currently @Frédéric Dupuis and I are in the process of getting Gelfand duality and the continuous functional calculus off the ground, and there's a fair bit of C*-algebra development that has to wait for that.

I'm in the process of trying to generalize enough of mathlib to handle non-unital rings and algebras, which is proving to be rather a large chore.

One thing that needs doing: we need to put the c-star norm on docs#unitization, or maybe on a type synonym.

If you want to know where we're at, some good places to look are analysis/normed_space/star and analysis/normed_space/spectrum.

Unfortunately, I'll be rather too busy to have time for Lean for about 2-3 weeks, but I'll still be somewhat available on Zulip for questions.

Jireh Loreaux (May 07 2022 at 19:55):

@Yaël Dillies did I see you (or someone else) added Krein-Milman recently?

Yaël Dillies (May 07 2022 at 19:56):

#7288 for geometric Hahn-Banach and #8112 for Krein-Milman

Cameron Torrance (May 07 2022 at 21:36):

Have direct sums of banach algebras been implemented? If not where is the right place to put them?

Yaël Dillies (May 07 2022 at 21:42):

A Banach algebra is [normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [complete_space E], right?

Yaël Dillies (May 07 2022 at 21:43):

In that case, yes, it is already implemented and Lean will find all the relevant instances on α ⊕ β if you have the right imports.

Cameron Torrance (May 07 2022 at 22:03):

Not that I need it but has this also been done for a generic index set?

Eric Wieser (May 07 2022 at 22:09):

(Binary) direct sums are α × β not α ⊕ β, @Yaël Dillies

Eric Wieser (May 07 2022 at 22:09):

Cameron, docs#pi.normed_algebra is the version for a finite index set

Eric Wieser (May 07 2022 at 22:10):

I would guess we could do something similar for docs#dfinsupp for a finitely-supported index set, but that's currently missing

Eric Wieser (May 07 2022 at 22:11):

(note that docs#direct_sum is just docs#dfinsupp but with a convolutional multiplication structure)

Cameron Torrance (May 07 2022 at 22:12):

I was thinking of the subspace of the product that has finite sup given the sup norm.

Jireh Loreaux (May 07 2022 at 22:21):


Jireh Loreaux (May 07 2022 at 22:23):

This is what you would want I think for non-finite index sets, but I'm not sure if the relevant instances for the multiplicative structure on L- infty exist yet. Perhaps someone else knows.

Cameron Torrance (May 07 2022 at 22:35):

this seems to be for finite indexing sets as well.

Eric Wieser (May 07 2022 at 22:37):

Right, docs#pi.has_norm (the sup norm) is limited to finite index sets as otherwise it would introduce a different topology to docs#Pi.topological_space.

Eric Wieser (May 07 2022 at 22:38):

@Jireh Loreaux, that definition does not allow p = ∞ for the sup norm

Jireh Loreaux (May 07 2022 at 22:42):

Whoops, I thought this is what Heather added a few months ago, and I would have sworn she explicitly handled infinity, but maybe I'm wrong.

Jireh Loreaux (May 07 2022 at 22:43):


Jireh Loreaux (May 07 2022 at 22:44):

Sorry, I picked wrong.

Eric Wieser (May 07 2022 at 22:44):


Eric Wieser (May 07 2022 at 22:52):

It looks like we don't have the statement that lp over components that are normed algebras is a normed_algebra; Is that what you're asking about @Cameron Torrance? Under what generality is it true?

Jireh Loreaux (May 07 2022 at 22:58):

I think he just wants L infty, otherwise there is no multiplication. And it's true over arbitrary index types. If all components are complete, so is L infty.

Jireh Loreaux (May 07 2022 at 23:12):

Completeness we already have though. Basically, we just want a has_mul on lp infty

Cameron Torrance (May 07 2022 at 23:13):

at the moment I only really need it for the binary product but it will be important later on.

Jireh Loreaux (May 07 2022 at 23:13):

And then the rest (normed_ring and normed_algebra) will be easy.

Jireh Loreaux (May 07 2022 at 23:14):

Yes, if you're up for it, please have a go at this. Ping me here or on GitHub when it's ready for review.

Cameron Torrance (May 07 2022 at 23:16):

do you have a proof that C^* algebra norms are unique?

Cameron Torrance (May 07 2022 at 23:16):

I'll have a go tomorrow.

Jireh Loreaux (May 07 2022 at 23:23):

Not yet. That's a bit hard to state in mathlib, though not impossible. We have Gelfand's formula though.

Eric Wieser (May 07 2022 at 23:35):

@Cameron Torrance, have you already been invited to the mathlib github org? You won't be able to make a PR the right way if not.

Cameron Torrance (May 08 2022 at 00:14):

Not yet, I was going to ask about that when I had stuff to send over, I think my github username is Cameron Torrance (I think) . Can't we get away with showing that star isos between C^* algebras are isometric .

Eric Wieser (May 08 2022 at 00:23):


Jireh Loreaux (May 08 2022 at 00:26):

That would be my preferred way to say it, yes. What we'll want to say is that an injective star algebra hom is isometric. This is how we'll define the spectrum in a way that's meaningful in non-unital algebras (we will define the spectrum of an element in a non-unital algebra to be the spectrum in the unitization, then the isometric property above yields spectral invariance. So the spectrum so-defined is equal no matter how you embed in a unital algebra).

Cameron Torrance (May 08 2022 at 00:28):

Eric Wieser said:



Jireh Loreaux (May 08 2022 at 00:28):

What I meant about it being hard is that it's hard to state the way it is in a textbook (i.e., if a type has two c-star norms then they coincide)

Eric Wieser (May 08 2022 at 00:30):

I guess that would be stated something like [ring R] : subsingleton (\sigma [star_ring R], by exactI cstar_ring R)?

Eric Wieser (May 08 2022 at 00:31):

Oh yeah, that's super hard to state because docs#non_unital_normed_ring extends ring, and you want to say "given a fixed ring structure, there's only one norm"

Jireh Loreaux (May 08 2022 at 00:31):


Eric Wieser (May 08 2022 at 00:32):

(Are you saying "given a fixed star" too?)

Cameron Torrance (May 08 2022 at 00:32):


Eric Wieser (May 08 2022 at 00:36):

Jireh Loreaux said:


As an aside; I just updated doc-gen#163 to show the instances that currently exist for lp: https://leanprover-community.github.io/mathlib_docs_demo/analysis/normed_space/lp_space.html#lp

Last updated: Dec 20 2023 at 11:08 UTC