intro Jan de Wit

Stream: new members

[Jan de Wit]

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. ..

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

There you have a type with 4 elements

[Johan Commelin]

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

[Eric Wieser]

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

[Thomas Browning]

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

[Jan de Wit]

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.

[Thomas Browning]

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.

[Eric Wieser]

multiplicative (zmod n) is the multiplicative version

[Eric Wieser]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Jan de Wit]

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.

[Alex J. Best]

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!

[Jan de Wit]

@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 :-)

[Johan Commelin]

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

[Thomas Browning]

And the plain search feature in VS Code

[Jan de Wit]

@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 :-)

[Scott Morrison]

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.)

[Scott Morrison]

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. :-)

[Anne Baanen]

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? :)