Getting involved with mathlib

Stream: new members

[Cameron Torrance]

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]

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]

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

[Jireh Loreaux]

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]

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

[Yaël Dillies]

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

[Cameron Torrance]

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

[Yaël Dillies]

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

[Yaël Dillies]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Cameron Torrance]

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

[Jireh Loreaux]

docs#pi_Lp

[Jireh Loreaux]

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]

this seems to be for finite indexing sets as well.

[Eric Wieser]

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]

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

[Jireh Loreaux]

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]

docs#lp

[Jireh Loreaux]

Sorry, I picked wrong.

[Eric Wieser]

(deleted)

[Eric Wieser]

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]

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]

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

[Cameron Torrance]

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

[Jireh Loreaux]

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

[Jireh Loreaux]

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]

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

[Cameron Torrance]

I'll have a go tomorrow.

[Jireh Loreaux]

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

[Eric Wieser]

@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]

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]

https://github.com/CameronTorrance?

[Jireh Loreaux]

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]

Eric Wieser said:

https://github.com/CameronTorrance?

yeah

[Jireh Loreaux]

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]

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

[Eric Wieser]

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]

Exactly

[Eric Wieser]

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

[Cameron Torrance]

yes

[Eric Wieser]

Jireh Loreaux said:

docs#lp

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