teaching use of quotients in Lean

Stream: maths

[Kevin Buzzard]

I once found it hard to use quotients in Lean. I typically wanted to use quotients to define mathematical objects (like quotient rings) and the example (unordered pairs) in TPIL was a bit CSish for me. The first time I needed them was for localisation of rings and Kenny wrote everything for me. But I needed them more and more, and eventually I had to learn how they worked. I wrote code for the integers mod n, but at the time I didn't understand the type class inference system very well either, and the code was not great. @Luca Gerolla needs to work with quotients for his work on the fundamental group and it occurred to me that I should revisit the work and tidy it up. One problem with integers mod n which I think could confuse beginners was a problem discussed here once, namely that it's hard to use type classes to put the equivalence relation of being congruent mod n onto Z, because that's one equivalence relation per n, and type class inference would rather there just be one equivalence relation on a type. The fix suggested to me at the time was to use a new version of Z for each integer, but having mulled this over for a while I decided that it added another layer of complexity which was unsuitable for the beginner. So I decided to choose everyone (except Johan)'s favourite integer 37, and just construct the integers mod 37 instead.

I jump from tactic mode proofs to half-tactic half-term to full term mode proofs, depending on whether I'm trying to demonstrate something for the first time or just get things done. This code is supposed to be readable by learners who know a bit about Lean and are interested in decyphering all the quotient.induction_on\2 stuff and want to see a relatively simple example. The code is here:

https://github.com/kbuzzard/xena/blob/master/xenalib/m1f/zmod37.lean

[Patrick Massot]

Why do you define a setoid instance instead of having a def?

[Mario Carneiro]

I'm not seeing why 37 is better than n

[Kevin Buzzard]

I want to give the same answer to both questions -- so I can use type class inference

[Kevin Buzzard]

I wanted access to the \[[ notation etc

[Mario Carneiro]

make a notation for that

[Kevin Buzzard]

I didn't want to make it harder. I wanted to show Luca how to do it

[Kevin Buzzard]

That's the actual answer.

[Kevin Buzzard]

I want him to use type class inference

[Mario Carneiro]

I think setoid is one of the more poorly thought out typeclasses

[Chris Hughes]

Are we still going to be stuck with those things in lean4?

[Mario Carneiro]

no idea

[Mario Carneiro]

I think it should be called has_equiv and be tied to the \approx notation, but the \[[ notation should be inferred by unification

[Kenny Lau]

in lean4 we wouldn't have to worry about + and * being different things right

[Mario Carneiro]

that's a bit vague

[Chris Hughes]

I think the idea is that we won't have both add_group and group

[Mario Carneiro]

we won't have either

[Kevin Buzzard]

I think setoid is one of the more poorly thought out typeclasses

Sure, but I am teaching Lean 3.4.1 so I went with it.

[Mario Carneiro]

presumably that's moving to mathlib

[Kevin Buzzard]

we could have heartsuit_group

[Kevin Buzzard]

the possibilities are endless

[Mario Carneiro]

my point is that it's not a great example if you are teaching typeclasses

[Kevin Buzzard]

I'm not teaching typeclasses, I'm teaching Luca how to work with the quotient of the paths from x to x by the is_homotopic relation which he's shown is an equivalence relation. He now has to define a group structure on the quotient, and I looked at his code, and he defined the group law by using quotient.out to choose two random lifts, composed the paths, and went back down again. He was not using type class inference either, so it was @quotient.out [insert proof of equiv reln here] I needed to show him how to do it properly. I agree that the file doesn't do everything, but hopefully it does what it needs to do.

[Kevin Buzzard]

It is also the file I wished I had when I was trying to figure out how to use quotients for the first time.

[Mario Carneiro]

maybe it should be

[Mario Carneiro]

rather than showing people Z/37Z, show them the fundamental group

[Mario Carneiro]

it's surely more interesting for students with more mathematical sophistication

[Mario Carneiro]

then prove the fundamental group of the circle is Z and PR it :D

[Kevin Buzzard]

then prove the fundamental group of the circle is Z and PR it :D

You mean do an _example_???

[Kevin Buzzard]

Oh, is this just a way of proving that the definition is correct?

[Kevin Buzzard]

The proof of pi_1(S^1)=Z I know involves constructing going via a triangulation and using some simplicial approximation theorem stuff

[Kevin Buzzard]

it would not surprise me if there were a cute proof though

[Mario Carneiro]

that is not what I expected

[Mario Carneiro]

the proof I know uses covering maps and winding numbers

[Johan Commelin]

S^1 = real/int, and real is contractible. So int is the fundamental group.

[Johan Commelin]

Now, how do we explain that to Lean?

[Mario Carneiro]

wait what

[Mario Carneiro]

how does that last step work?

[Johan Commelin]

I guess you need to know that S^1 is a nice space...

[Mario Carneiro]

I believe the first line, that's not hard to prove

[Johan Commelin]

Where nice means locally compact and t2, or something similar.

[Mario Carneiro]

and you should get niceness that way

[Johan Commelin]

And then you know that S^1 has a universal covering space, and you get a group structure on the fibre, which is exactly pi_1

[Mario Carneiro]

are you still elucidating your one line proof?

[Johan Commelin]

Yes... I'm sorry.

[Mario Carneiro]

I'm trying to figure out how R is contractible plays into this

[Johan Commelin]

Well, that is supposed to convince you that R is the universal covering space...

[Johan Commelin]

We could prove a general lemma of the form simply_connected X implies pi_1(X/G) = G

[Mario Carneiro]

oh so that's true in generality?

[Johan Commelin]

If X is nice.

[Johan Commelin]

Maybe even in general.

[Mario Carneiro]

G is discrete?

[Mario Carneiro]

i.e. pi_1(X/X) is not X

[Johan Commelin]

True.

[Mario Carneiro]

to make X a covering map you need it to be locally like a quotient by a discrete space

[Johan Commelin]

So there are some conditions. G needs to be discrete (topologically) and act freely on X, and the action must be continuous.

[Johan Commelin]

So G is a discrete subgroup of Aut_Top(X).

[Mario Carneiro]

which kind of quotient are we talking about here?

[Johan Commelin]

But I haven't formalised this... so I don't know what I'm talking about.

[Johan Commelin]

X/G as a set, with quotient topology, I think.

[Mario Carneiro]

If X is a topological group and G a discrete subgroup you get the other conditions

[Mario Carneiro]

R/Z as a set is garbage, that just identifies the points of Z in R making it a bouquet of circles

[Johan Commelin]

Aah, sorry. I meant as group action of sets.

[Kevin Buzzard]

this is the quotient of a group acting on a nice top space

[Kevin Buzzard]

so the quotient space is the set of orbits

[Kevin Buzzard]

An example is the quotient of a group by a subgroup

[Kevin Buzzard]

but if $\Gamma$ is a subgroup of $SL(2,\mathbb{Z})$ with no torsion (e.g. the elements congruent to the identity modulo $N$ for any $N>=3$) then $\Gamma$ acts on the upper half plane (which is nice and contractible) discretely, and the quotient is a non-compact Riemann surface with fundamental group $\Gamma$.

[Johan Commelin]

What would the definition of S^1 be in Lean?

[Kevin Buzzard]

You could certainly define it to be the closed subspace of R^2

[Johan Commelin]

Right, that is maybe a more reasonable definition.

[Mario Carneiro]

that's my thought as well, it's true to the literature and also generalizes to using circles as... circles

[Kevin Buzzard]

and IF WE EVER MANAGED TO GET THE EXPONENTIAL FUNCTION INTO MATHLIB then you could even prove it was R mod Z :-)

[Johan Commelin]

And then identify it with the unit circle in C

[Johan Commelin]

Right.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Trivial.20things.20about.20convergent.20power.20series

[Johan Commelin]

Maybe exp should move to the community fork. Who knows if that would move it forward...

[Mario Carneiro]

pff, use rational trig and you don't need exp

[Kevin Buzzard]

:-)

[Kevin Buzzard]

Who needs to be complex when you can just be rational.

[Mario Carneiro]

that's actually a good idea Johan

[Kevin Buzzard]

Or you could just come to the xena project, we use it freely over there :-)

[Kevin Buzzard]

warning: not all code compiles

[Mario Carneiro]

which is why it is a good community fork project

[Mario Carneiro]

you are already using it but the PR needs more work

[Mario Carneiro]

or at least I need to spend more time on it

[Kevin Buzzard]

I don't even know which PR it is any more. Is it in the binomial theorem one or the limits one?

[Kevin Buzzard]

I can't find it in either

[Mario Carneiro]

surely it's not in the binomial theorem

[Johan Commelin]

I think anyone can pull that branch into the community fork, right? (After we found it)

[Mario Carneiro]

yes

[Kevin Buzzard]

I think he needed the binomial theorem to prove exp(x+y)=exp(x)exp(y)

[Mario Carneiro]

I suppose you do

[Kevin Buzzard]

By the way, another random PR we use a lot at Imperial is Chris' zmod work. But I hear you didn't like pos_nat and I believe Chris is now re-doing everything with pnat and prime

[Kevin Buzzard]

I can't find exp. Did he close it?

[Kevin Buzzard]

No wonder it didn't get accepted :-)

[Johan Commelin]

@Chris Hughes We need you (-;

[Kevin Buzzard]

he's too busy helping all the other Imperial UGs while I'm on holiday :-)

[Mario Carneiro]

https://github.com/leanprover/mathlib/pull/43

[Johan Commelin]

branch is no longer there.

[Johan Commelin]

So we will need to get the stuff out of Xena.

[Kevin Buzzard]

so it looks like the ball's in Chris' court.

[Mario Carneiro]

no wait it's https://github.com/leanprover/mathlib/pull/41

[Mario Carneiro]

it says it is a PR from unknown repository

[Kevin Buzzard]

I'd be quite happy if he were to concentrate on zmod at the minute, we've all found this very helpful. There's a bunch of people doing number theory and group theory, some of whom use it.

[Johan Commelin]

Which means that the repo was deleted from github, I think

[Chris Hughes]

I think I deleted my fork of mathlib at some point when I was frustratedly trying to learn how to use git.

[Kevin Buzzard]

They don't teach mathematicians git :-(

[Johan Commelin]

Chapter 0 in your book is about git, right?

[Mario Carneiro]

I think those files should all be dumped in the community fork, and we can come back to it at some point

[Kevin Buzzard]

I'm not competent to write it

[Johan Commelin]

You could have a foreword by someone else... Mario for example

[Mario Carneiro]

Step 1: git-scm.com, step 2: profit

[Andrew Ashworth]

Install sourcetree while you're at it

[Andrew Ashworth]

Nobody has time to remember all the magic git invocations, so a gui wrapper really helps

[Patrick Massot]

I used to believe that. So I advised computer afraid colleagues to use source tree and, after many rescuing operations, I realized command line is much simpler. Because you don't have to know about all commands and options that are not written in your git cheat sheet.