Zulip Chat Archive

Stream: maths

Topic: teaching use of quotients in Lean


view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 09 2018 at 17:20):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:24):

I'm not seeing why 37 is better than n

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:24):

I wanted access to the \[[ notation etc

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:24):

make a notation for that

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:25):

That's the actual answer.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:25):

I want him to use type class inference

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:26):

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

view this post on Zulip Chris Hughes (Aug 09 2018 at 17:27):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:27):

no idea

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 09 2018 at 17:29):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:29):

that's a bit vague

view this post on Zulip Chris Hughes (Aug 09 2018 at 17:30):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:30):

we won't have either

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:30):

presumably that's moving to mathlib

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:31):

we could have heartsuit_group

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:31):

the possibilities are endless

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:31):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:35):

maybe it should be

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:35):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:36):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:39):

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

view this post on Zulip 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_???

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:40):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:41):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:42):

that is not what I expected

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:42):

the proof I know uses covering maps and winding numbers

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:43):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:43):

Now, how do we explain that to Lean?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:43):

wait what

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:44):

how does that last step work?

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:45):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:45):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:45):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:45):

and you should get niceness that way

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:47):

are you still elucidating your one line proof?

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:47):

Yes... I'm sorry.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:47):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:48):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:49):

oh so that's true in generality?

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:49):

If X is nice.

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:49):

Maybe even in general.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:49):

G is discrete?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:50):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:50):

True.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:51):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:52):

which kind of quotient are we talking about here?

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:52):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:53):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 17:53):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:54):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:55):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:55):

so the quotient space is the set of orbits

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:55):

An example is the quotient of a group by a subgroup

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:57):

but if Γ\Gamma is a subgroup of SL(2,Z)SL(2,\mathbb{Z}) with no torsion (e.g. the elements congruent to the identity modulo NN for any N>=3N>=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.

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:58):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 17:58):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:59):

Right, that is maybe a more reasonable definition.

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:59):

And then identify it with the unit circle in C

view this post on Zulip Johan Commelin (Aug 09 2018 at 17:59):

Right.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:00):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:00):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:00):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:00):

:-)

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:00):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:01):

that's actually a good idea Johan

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:02):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:02):

warning: not all code compiles

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:02):

which is why it is a good community fork project

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:03):

you are already using it but the PR needs more work

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:03):

or at least I need to spend more time on it

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:04):

I can't find it in either

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:04):

surely it's not in the binomial theorem

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:04):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:04):

yes

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:05):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:05):

I suppose you do

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:07):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:07):

No wonder it didn't get accepted :-)

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:07):

@Chris Hughes We need you (-;

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:07):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:08):

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

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:09):

branch is no longer there.

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:09):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:09):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:09):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:09):

it says it is a PR from unknown repository

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:10):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:10):

They don't teach mathematicians git :-(

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:11):

Chapter 0 in your book is about git, right?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:11):

I'm not competent to write it

view this post on Zulip Johan Commelin (Aug 09 2018 at 18:11):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:12):

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

view this post on Zulip Andrew Ashworth (Aug 09 2018 at 18:56):

Install sourcetree while you're at it

view this post on Zulip Andrew Ashworth (Aug 09 2018 at 18:57):

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

view this post on Zulip 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