Zulip Chat Archive

Stream: new members

Topic: intro Jan de Wit


view this post on Zulip Jan de Wit (Mar 13 2021 at 21:02):

Hello everybody!

I'm Jan de Wit, from Utrecht in the Netherlands. I have a fairly strong mathematical but mostly CS (Haskell) background (@Andres Löh might remember me from way back when in the Generic Haskell days...). Nowadays I work in IT, but that's not going to stop me from tickling my brain from time to time; and Lean seems just the ticket.

So to kick things off, I've got two questions; one CS-y and one mathematical.

1: Is there a formal definition of the Lean language, something like to the Haskell reports? The sheer amount of syntax overwhelms me at times, but that's probably due to me not knowing the "prelude" by heart....

2: How would I go about proving that a group with 4 elements is either isomorphic to Z_4 or Z_2 x Z_2? I've followed the 'Formalising Mathematics' series of blog posts by @Kevin Buzzard up to week 6, but I don't even know how to state the hypothesis that the carrier is finite and has 4 elements. I also don't know how to construct cyclic groups or direct products. And finally I don't want to do a case analysis on the 4^16 possible multiplication tables :-) I don't need (or want!) a slick proof, I just want to know where to start. ..

view this post on Zulip Johan Commelin (Mar 13 2021 at 21:04):

Welcome! Always good to have more Dutchies on board :grinning:

view this post on Zulip Johan Commelin (Mar 13 2021 at 21:05):

example (G : Type*) [fintype G] (h : fintype.card G = 4) : ...

view this post on Zulip Johan Commelin (Mar 13 2021 at 21:05):

There you have a type with 4 elements

view this post on Zulip Johan Commelin (Mar 13 2021 at 21:09):

docs#prod.group gives you product groups and docs#is_cyclic cyclic groups

view this post on Zulip Eric Wieser (Mar 13 2021 at 21:21):

I think this might be one way to state your theorem for 2:

import data.zmod.basic
import data.fintype.basic

example (G : Type*) [fintype G] [add_group G] (h : fintype.card G = 4) :
  nonempty (G ≃+ zmod 4)  nonempty (G ≃+ zmod 2 × zmod 2) := sorry

where docs#add_equiv ≃+ is your "isomorphic", and docs#zmod is your Z_n

view this post on Zulip Thomas Browning (Mar 13 2021 at 21:22):

And if you want to classify groups of order 4 (or p^2) for that matter, you might find docs#order_of helpful

view this post on Zulip Jan de Wit (Mar 13 2021 at 21:23):

Hi Johan, thanks for the welcome! I'll go and poke around in mathlib some more tomorrow, you've given me the first steps :-) I guess I'm still stumbling around due to a lack of discoverability - I know it's probably there, but I just don't know where to look.

view this post on Zulip Thomas Browning (Mar 13 2021 at 21:24):

Is there a cyclic multiplicative group in mathlib? As soon as you go to groups of order 6, you're going to want to work with multiplicative groups rather than additive groups.

view this post on Zulip Eric Wieser (Mar 13 2021 at 21:24):

multiplicative (zmod n) is the multiplicative version

view this post on Zulip Eric Wieser (Mar 13 2021 at 21:25):

But does it matter? All it changes is whether you use the symbols +/- or *//.

view this post on Zulip Thomas Browning (Mar 13 2021 at 21:26):

if you're working with nonabelian groups, then * seems like a better option. For example, the symmetric groups are multplicative, I think.

view this post on Zulip Thomas Browning (Mar 13 2021 at 21:26):

(e.g. equiv.perm (fin n))

view this post on Zulip Thomas Browning (Mar 13 2021 at 21:27):

Technically there's no difference, but morally I feel like you should be using *

view this post on Zulip Jan de Wit (Mar 13 2021 at 21:30):

Eric Wieser said:

nonempty (G ≃+ zmod 2) ∨ nonempty (G ≃+ zmod 2 × zmod 2) := sorry

````

(Your first 2 should be a 4, right?)
Ahh, I get it, I think.  G  ≃+ H is the *type* of additive isos between G and H, not the proposition that there exists such an iso.

view this post on Zulip Alex J. Best (Mar 13 2021 at 21:31):

Jan de Wit said:

Hi Johan, thanks for the welcome! I'll go and poke around in mathlib some more tomorrow, you've given me the first steps :-) I guess I'm still stumbling around due to a lack of discoverability - I know it's probably there, but I just don't know where to look.

https://leanprover-community.github.io/learn.html is the place to start if you haven't seen it, but there is a lot on there! The tactic cheat sheet https://leanprover-community.github.io//img/lean-tactics.pdf might be the sort of thing you are looking for, with some of the most common tactics.
For example I imagine your proof will start with something like by_cases h : \exists g : G, g.order_of = 4,.
The issue with having a completely definitive reference is that tactics can take almost arbitrary syntax, so to know the language completely you'd have to read all of https://leanprover-community.github.io/mathlib_docs/tactics.html which is way too long!

view this post on Zulip Jan de Wit (Mar 13 2021 at 21:36):

@Alex J. Best : I studied under Swierstra so I know monadic parsers when I see 'em :-) The flexibility of Lean's syntax makes me go down rabbit holes which leave me wanting for clearer docstrings :-)

view this post on Zulip Johan Commelin (Mar 13 2021 at 21:36):

@Jan de Wit I think the search bar on the docs page is quite useful, and good ol' grep (-;

view this post on Zulip Thomas Browning (Mar 13 2021 at 21:43):

And the plain search feature in VS Code

view this post on Zulip Jan de Wit (Mar 13 2021 at 21:59):

@Johan Commelin and all the rest: Thank you all for the help, I know what I'll be doing tomorrow!

PS: can you parametrize over x/+/foo? It seems a waste of namespace to have to use ≃, ≃+ and ≃foo etcetera, when the operation is a parameter. I know there's a (rather brute-force) tactic that lifts multiplicative proofs to additive ones for groups somewhere, but it seems to me that once you want to express statements like the (x,inv,1/+,neg,0/foo,bar,baz) group on the left is isomorphic to the (x/+/foo) group on the right you get a quadratic explosion of statements, all rather devoid of content :-)

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:31):

Jan de Wit said:

... go down rabbit holes which leave me wanting for clearer docstrings :-)

This is perhaps an unhelpful thing to say to a newcomer, but we love PRs adding docstrings, and, sometimes the person most able to add good ones is the person who has just now deciphered what the function is doing. (But also, our collective apologies: we know docstrings need to be better.)

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:42):

Jan de Wit said:

Johan Commelin and all the rest: Thank you all for the help, I know what I'll be doing tomorrow!

PS: can you parametrize over x/+/foo?

Three answers:

  • no, this is an embarrassing aspect of mathlib; at least everyone with good taste asks this, and we have to keep explaining. :-)
  • as it turns out, there's less foo than you might expect, and mathematicians have pretty robust opinions about what is + and what is * (but of course we have order equivalences, and perhaps soon lattice equivalences, etc etc)
  • yes, the category theory library has a polymorphic notion of equality, and you can write G ≅ H (with the same iso behind that notation), whether G H : AddCommGroup or G H : cochain_complex (Mon_ (sheaf X Ring)). But:
    • this is not actually as polymorphic as the existing ≃+, because it requires G and H to be in the same universe. (My universe is Type 0...)
    • the category theory library is not used much in the pre-1950s parts of mathlib. :-)

view this post on Zulip Anne Baanen (Mar 15 2021 at 10:27):

Hi Jan, nice to see a fellow ex-Utrechter here :grinning: I did my Master's thesis under Swierstra, but I don't think we met each other. Perhaps your Swierstra was Doaitse, not Wouter? :)


Last updated: May 14 2021 at 13:24 UTC