## Stream: maths

### Topic: teaching use of quotients in Lean

#### Kevin Buzzard (Aug 09 2018 at 17:03):

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 (Aug 09 2018 at 17:20):

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

#### Mario Carneiro (Aug 09 2018 at 17:24):

I'm not seeing why 37 is better than n

#### Kevin Buzzard (Aug 09 2018 at 17:24):

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

#### Mario Carneiro (Aug 09 2018 at 17:24):

make a notation for that

#### Kevin Buzzard (Aug 09 2018 at 17:24):

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

#### Kevin Buzzard (Aug 09 2018 at 17:25):

I want him to use type class inference

#### Mario Carneiro (Aug 09 2018 at 17:26):

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

#### Chris Hughes (Aug 09 2018 at 17:27):

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

no idea

#### Mario Carneiro (Aug 09 2018 at 17:28):

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 (Aug 09 2018 at 17:29):

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

#### Mario Carneiro (Aug 09 2018 at 17:29):

that's a bit vague

#### Chris Hughes (Aug 09 2018 at 17:30):

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

#### Mario Carneiro (Aug 09 2018 at 17:30):

we won't have either

#### Kevin Buzzard (Aug 09 2018 at 17:30):

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 (Aug 09 2018 at 17:30):

presumably that's moving to mathlib

#### Kevin Buzzard (Aug 09 2018 at 17:31):

we could have heartsuit_group

#### Kevin Buzzard (Aug 09 2018 at 17:31):

the possibilities are endless

#### Mario Carneiro (Aug 09 2018 at 17:31):

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

#### Kevin Buzzard (Aug 09 2018 at 17:34):

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 (Aug 09 2018 at 17:35):

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 (Aug 09 2018 at 17:35):

maybe it should be

#### Mario Carneiro (Aug 09 2018 at 17:35):

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

#### Mario Carneiro (Aug 09 2018 at 17:36):

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

#### Mario Carneiro (Aug 09 2018 at 17:39):

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

#### Kevin Buzzard (Aug 09 2018 at 17:40):

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

You mean do an _example_???

#### Kevin Buzzard (Aug 09 2018 at 17:40):

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

#### Kevin Buzzard (Aug 09 2018 at 17:41):

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 (Aug 09 2018 at 17:41):

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

#### Mario Carneiro (Aug 09 2018 at 17:42):

that is not what I expected

#### Mario Carneiro (Aug 09 2018 at 17:42):

the proof I know uses covering maps and winding numbers

#### Johan Commelin (Aug 09 2018 at 17:43):

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

#### Johan Commelin (Aug 09 2018 at 17:43):

Now, how do we explain that to Lean?

wait what

#### Mario Carneiro (Aug 09 2018 at 17:44):

how does that last step work?

#### Johan Commelin (Aug 09 2018 at 17:45):

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

#### Mario Carneiro (Aug 09 2018 at 17:45):

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

#### Johan Commelin (Aug 09 2018 at 17:45):

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

#### Mario Carneiro (Aug 09 2018 at 17:45):

and you should get niceness that way

#### Johan Commelin (Aug 09 2018 at 17:46):

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 (Aug 09 2018 at 17:47):

are you still elucidating your one line proof?

#### Johan Commelin (Aug 09 2018 at 17:47):

Yes... I'm sorry.

#### Mario Carneiro (Aug 09 2018 at 17:47):

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

#### Johan Commelin (Aug 09 2018 at 17:48):

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

#### Johan Commelin (Aug 09 2018 at 17:49):

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

#### Mario Carneiro (Aug 09 2018 at 17:49):

oh so that's true in generality?

#### Johan Commelin (Aug 09 2018 at 17:49):

If X is nice.

#### Johan Commelin (Aug 09 2018 at 17:49):

Maybe even in general.

G is discrete?

#### Mario Carneiro (Aug 09 2018 at 17:50):

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

True.

#### Mario Carneiro (Aug 09 2018 at 17:51):

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

#### Johan Commelin (Aug 09 2018 at 17:51):

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

#### Johan Commelin (Aug 09 2018 at 17:51):

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

#### Mario Carneiro (Aug 09 2018 at 17:52):

which kind of quotient are we talking about here?

#### Johan Commelin (Aug 09 2018 at 17:52):

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

#### Johan Commelin (Aug 09 2018 at 17:53):

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

#### Mario Carneiro (Aug 09 2018 at 17:53):

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

#### Mario Carneiro (Aug 09 2018 at 17:54):

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

#### Johan Commelin (Aug 09 2018 at 17:54):

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

#### Kevin Buzzard (Aug 09 2018 at 17:55):

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

#### Kevin Buzzard (Aug 09 2018 at 17:55):

so the quotient space is the set of orbits

#### Kevin Buzzard (Aug 09 2018 at 17:55):

An example is the quotient of a group by a subgroup

#### Kevin Buzzard (Aug 09 2018 at 17:57):

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 (Aug 09 2018 at 17:58):

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

#### Kevin Buzzard (Aug 09 2018 at 17:58):

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

#### Johan Commelin (Aug 09 2018 at 17:59):

Right, that is maybe a more reasonable definition.

#### Mario Carneiro (Aug 09 2018 at 17:59):

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

#### Kevin Buzzard (Aug 09 2018 at 17:59):

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

#### Johan Commelin (Aug 09 2018 at 17:59):

And then identify it with the unit circle in C

Right.

#### Johan Commelin (Aug 09 2018 at 18:00):

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

#### Mario Carneiro (Aug 09 2018 at 18:00):

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

:-)

#### Kevin Buzzard (Aug 09 2018 at 18:00):

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

#### Mario Carneiro (Aug 09 2018 at 18:01):

that's actually a good idea Johan

#### Kevin Buzzard (Aug 09 2018 at 18:02):

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

#### Kevin Buzzard (Aug 09 2018 at 18:02):

warning: not all code compiles

#### Mario Carneiro (Aug 09 2018 at 18:02):

which is why it is a good community fork project

#### Mario Carneiro (Aug 09 2018 at 18:03):

you are already using it but the PR needs more work

#### Mario Carneiro (Aug 09 2018 at 18:03):

or at least I need to spend more time on it

#### Kevin Buzzard (Aug 09 2018 at 18:04):

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

#### Kevin Buzzard (Aug 09 2018 at 18:04):

I can't find it in either

#### Mario Carneiro (Aug 09 2018 at 18:04):

surely it's not in the binomial theorem

#### Johan Commelin (Aug 09 2018 at 18:04):

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

yes

#### Kevin Buzzard (Aug 09 2018 at 18:05):

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

I suppose you do

#### Kevin Buzzard (Aug 09 2018 at 18:06):

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 (Aug 09 2018 at 18:07):

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

#### Kevin Buzzard (Aug 09 2018 at 18:07):

No wonder it didn't get accepted :-)

#### Johan Commelin (Aug 09 2018 at 18:07):

@Chris Hughes We need you (-;

#### Kevin Buzzard (Aug 09 2018 at 18:07):

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

#### Mario Carneiro (Aug 09 2018 at 18:08):

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

#### Johan Commelin (Aug 09 2018 at 18:09):

branch is no longer there.

#### Johan Commelin (Aug 09 2018 at 18:09):

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

#### Kevin Buzzard (Aug 09 2018 at 18:09):

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

#### Mario Carneiro (Aug 09 2018 at 18:09):

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

#### Mario Carneiro (Aug 09 2018 at 18:09):

it says it is a PR from unknown repository

#### Kevin Buzzard (Aug 09 2018 at 18:10):

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 (Aug 09 2018 at 18:10):

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

#### Chris Hughes (Aug 09 2018 at 18:10):

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

#### Kevin Buzzard (Aug 09 2018 at 18:10):

They don't teach mathematicians git :-(

#### Mario Carneiro (Aug 09 2018 at 18:11):

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

#### Kevin Buzzard (Aug 09 2018 at 18:11):

I'm not competent to write it

#### Johan Commelin (Aug 09 2018 at 18:11):

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

#### Mario Carneiro (Aug 09 2018 at 18:12):

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

#### Andrew Ashworth (Aug 09 2018 at 18:56):

Install sourcetree while you're at it

#### Andrew Ashworth (Aug 09 2018 at 18:57):

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

#### Patrick Massot (Aug 09 2018 at 21:04):

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.

Last updated: May 09 2021 at 11:09 UTC