Proving Cayley's Theorem

Stream: new members

[Greg Conneen]

Okay, so as was suggested to me the other day, I think it would be a good idea to prove Cayley's theorem in Lean. I think it would give me a good understanding of how certain mathematical structures are implemented in Lean, and would give me a chance to get some feedback on my code. Below is essentially my outline of a TODO.

Preliminaries: the first thing I need to do is talk about an arbitrary group G, with an operation x. Then I want the set of elements of G, S, defined. Third, I want to define the set F of bijective functions f: S -> S, that is, the set of permutations of S. I assume it would be easiest to first construct this just at injective mappings, and then it should be easy to prove that they are also surjective. Then, I want a construction of function composition within F. The final thing I want to show in my preliminaries is that (F, *) is a group with respect to composition. I assume this might take some bit of doing, since I'll have to show there is an inverse map, and it is in F. This seems like the hardest bit out of the preliminaries, unless there is already something in function.lean that shows a bijective map has an inverse. I will research this.

Now, the proof of the theorem: This much should be the easy part. all I have to do is define the map in F called f_g(x) = g*x, and show that the set of f_g for all g in G is a subgroup of F. That should be simple once I've gotten through the preliminaries.

Please let me know if this looks about right for what I'll end up implementing in Lean. Any tips on how to get started with the preliminaries, or any hints/tips about subtleties in Lean I might be missing would be much appreciated.

[Greg Conneen]

I have just discovered that the way permutations are defined includes an inverse

[Patrick Massot]

I'm a bit confused by your list. You saw perm S, right? There is also https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/group_action.lean

[Greg Conneen]

yes, I saw perm S. This sort of trivialises some of my workload

[Greg Conneen]

I did not see group_action.lean. I will study this file more and come back to this problem.

[Patrick Massot]

I'm very much aware of how bad is our documentation, but we still have lists of files visible on GitHub and on your hard drive. That file is not so well hidden in a folder named group_theory...

[Greg Conneen]

I understand. I've gotten used to hunting around mathlib for interesting and useful files, I just simply didn't think to look for such a file

[Kevin Buzzard]

Mathlib is a maze and it's extremely difficult to navigate it alone. I attempted to document some of what was there when I was just starting out, and I wrote some kind-of useless files, which perhaps helped nobody, but the attempt to write them at least made me look at every single Lean file in mathlib at least once. Of course back then mathlib was 1/3rd the size!

[Johan Commelin]

I'm wondering, is the proof of Cayley's theorem just funext and mul_assoc?

[Johan Commelin]

Ooh, we might need one more ext at the start.

[Mario Carneiro]

It's pretty crazy that since I gave my talk on the status of mathlib last year, mathlib has roughly doubled in size, and the number of contributors has gone up tenfold

[Johan Commelin]

Hmm... maybe you should give another talk. Let's see what happens?

[Kevin Buzzard]

@Greg Conneen There are two kinds of bijections in Lean; there are functions f : X -> Y equipped with an inverse function g : Y -> X and proofs that fg and gf are identity; those pieces of data are terms of type equiv X Y. There are also functions f : X -> Y plus a proof that these functions are injective and surjective. In constructive mathematics or computable mathematics or whatever weird kind of mathematics some computer scientists do, these two concepts are not the same. The problem is that the statement that f is bijective only gives you a theorem that for all y in Y there exists a unique x in X such that f(x)=y. To define the inverse function g you need an algorithm which spits this x out, i.e. "gets data from a proposition", and this is problematic. Even if f is computable, its inverse might not be -- given the algorithm which computes f, how do you get an algorithm which computes its inverse (especially if X is uncountable?). equiv is the "stronger" notion -- one can prove that equivs are bijective. To get a bijective map from an equiv you will have to struggle a bit more and switch on some stuff which I always have switched on anyway so I can't remember what it is exactly. noncomputability? The axiom of choice? Something like that.

[Kevin Buzzard]

For a general S, an injective function of course isn't bijective. Defining bijective functions in Lean is easy. You should prove that a composite of two injective functions is injective and the composite of two surjective functions is surjective, in tactic mode, as warm-up for this.

[Koundinya Vajjha]

Mathlib is a maze and it's extremely difficult to navigate it alone. I attempted to document some of what was there when I was just starting out, and I wrote some kind-of useless files, which perhaps helped nobody, but the attempt to write them at least made me look at every single Lean file in mathlib at least once. Of course back then mathlib was 1/3rd the size!

I myself was wondering about this. An ideal solution would be something like the archive of formal proofs for Lean, but all tied together with informal docstrings.

[Kevin Buzzard]

PS proving that an injective function from a finite set to itself is also surjective is not easy at all -- you are deluding yourself because you have an extremely accurate but unfortunately very geometric model of a finite set. Lean's definition of a finite set is equivalence classes of lists with no duplicate elements, so any proofs in the API will involve lifting to lists and then proving that things are constant on equivalence classes -- put it another way -- you have to order the set, prove or construct something with the ordered set (typically by induction on the size) and then prove that what you did was independent of the order. This can involve a very delicate induction, because the permutations of a finite set are generated by certain explicit permutations built into Lean. Everything about finite sets is much harder than you think. Fortunately the nice computer scientists wrote a gigantic API for finite sets so that mathematicians can use them the way they like to use them -- but don't be blinded by this -- finite sets are hard, and proving that an injective map is also surjective from first principles is hard.

[Greg Conneen]

Wow, okay. I was away all day and came back to a lot of really useful information. Thank you all so much, but now I have several questions

[Greg Conneen]

@Johan Commelin how can the proof be that simple? Is our library on groups and functions so extensive that it's practically trivial? I'd like to see your take on the proof. I still plan on doing it in a more roundabout way to help me understand Lean a little better in the process, but it'd be astoundingly beautiful to see a 5-line proof of Cayley's theorem.
@Mario Carneiro I would love a link to the talk you gave on mathlib, if you'd be so kind.
@Kevin Buzzard I saw how function.lean and data.equiv.basic handled bijections. That makes sense, given how they're defined. I still don't like the notation for equiv, but I suppose it's doable. Secondly, I'd be interested in proving that an injective map f: G -> G is bijective, and similarly when assuming surjectivity. I suppose that's a project for another day.
Lastly, is there anyone in particular to ask about more detailed comments in mathlib files? Not that the comments aren't sufficient, but I would like more mathematicians such as myself to be able to jump headfirst into Lean, and that seems difficult as-is. I know I'm not bringing up any new conversations, and this is a tangential question, but I was wondering who I should ask.

[Mario Carneiro]

https://www.youtube.com/watch?v=5tS4j_A1ZvU

[Greg Conneen]

Thank you so much!

[Mario Carneiro]

The statement that injective functions A -> A are bijective is fintype.injective_iff_bijective in data.fintype

[Greg Conneen]

Lovely. Is there a similar proof for surjective to bijective in that file?

[Mario Carneiro]

it's right after that

[Greg Conneen]

thanks, I'll check it out

[Kevin Buzzard]

Cayley's theorem can completely be simple. If G is a group then the multiplication map on G can be thought of as a map G -> (G -> G) (indeed in functional programming this is usually how it is stored) and this is exactly the function which embeds G into the permutations. I am confused by all this talk about injective and bijective. I thought G was an arbitrary group. So an injective function G -> G is not bijective. As for comments in mathlib files -- I guess what happened to me was that after a while I realised I didn't need comments, I could just read the code and see what was going on...

[Greg Conneen]

G is an arbitrary group, you're right. I was just talking about proving bijectivity since I came across it while studying Lean files that I'm not at all accustomed to.
As for comments... yeah, I guess I'm just not at the point where I'm able to read what's going on all the time. I suppose I just feel sort of stuck in low level Lean proofs since there's just a huge gap between basic proofs on propositions, integers, and the like and actually useful theoretical mathematics, such as algebra and analysis. I'm excited that the proof of Cayley's theorem is so simple, since that says very good things about the people who wrote the files on group theory and functions. But I feel that at the same time, it means I'm learning less about the way mathematics in Lean is formalised with every proof that comes my way. Do you think the best approach is to just read Lean files and use print/check/reduce/eval statements until I understand what's going on? I feel like in order to get comfortable with how mathematical structures are defined in Lean, that's an inevitability. I guess I'm just really excited to get to the high level stuff, but I'm slowly realising how much time that's going to take on my end. Is that the same for all of you, where Lean takes a lot of doing to get from where I am to a clear understanding of much of mathlib?

[Greg Conneen]

I also don't really know where to start. Should I be reading data.___.basic for things I'm interested in? Where's a good starting point?

[Kevin Buzzard]

Do you know the syntax for how to make a function and how to make a term of a structure? If so, then try and define a function G -> perm G

[Kevin Buzzard]

import data.equiv.basic

open equiv

def cayley (G : Type*) [group G] : G → perm G := ...

[Kevin Buzzard]

TPIL is the place to start

[Greg Conneen]

I know TPIL is like, the introductory level. But I've read through a majority of it, and skimmed through the bits I didn't. I don't know how much more there is to learn from it

[Mario Carneiro]

There is a long process from where you are to being able to write mathlib ready mathematics. The best thing you can do in that direction is pick an area that hasn't been formalized, write some stuff, and post about it here, or PR it. It will probably be torn apart but it's a good learning experience

To read mathlib isn't quite as hard as this; you can do pretty well by going to a file about a theory that interests you, and then browse through it, and figure out what the statements say and what part of the theory is being covered. Ctrl-click on stuff to trace back to prerequisite theorems, and you will start to get a sense of the layout

[Greg Conneen]

Gotcha. Yeah, I'm still sort of intimidated by a lot of mathlib files I guess, despite their triviality on paper

[Kevin Buzzard]

The thing about mathlib is that one of its philosophies is: if the observation is trivial on paper, then try and make the lean proof an incomprehensible one-liner. Of course a lot of these one-liners are now no longer incomprehensible to me, but I well remember when they were.

[Kevin Buzzard]

Here is a cool project. Prove that there is a bijection between equivalence relations on a set X and partitions of X into disjoint non-empty subsets. Mathematically this is straightforward but needs some basic stuff. You don't have to use typeclasses, which are tricky for beginners because the square bracket system needs to be internalised before you can see what it can do for you. Your job is to construct bijections between two sets and prove that they're bijections by evaluating the compositions and checking you get the identity. You'll learn a lot.

[Kevin Buzzard]

NB proving this might take you longer than you think. Not because it's hard, but because you'll have to learn how to manipulate structures and functions quite extensively, in a mathematically very simple situation. Even formalising the statement is a challenge for a beginner; I can do it for you if you want. You will need to make a structure partitions X such that a term of that type is a partition of X.

[Bryan Gin-ge Chen]

There's a related PR on partitions here, with links to some zulip threads on that topic. It's been languishing for a while since Johannes wanted a different approach and I've been distracted by other things.

[Kevin Buzzard]

This is like the "exercise 6.1" of Lean (forgive the obscure reference to the TeXbook). Proving something which is mathematically very simple and just involves a whole bunch of trivial-to-mathematician observations, in a formal system like Lean, forces you to think very carefully about what a term is, what a type, is, and what the type of everything is. It forces you to learn about how to define functions in Lean whose definitions you completely understand in maths, it forces you to learn about structures and ultimately the amount of code you'll probably end up writing as a beginner is surprisingly large. Then some whizz-kid will show you how it can all be done in a few lines using tricks and you'll begin to see why mathlib chooses 1 line proofs rather than 20 line proofs which are more "readable" -- who wants to read trivialities anyway?

[Kevin Buzzard]

Greg -- here's some homework.

import data.equiv.basic

/-

data.equiv.basic  is the import which gives you the type `equiv X Y`, the type of
bijections from X to Y.

Here's the definition of equiv from that file.

structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)
(inv_fun   : β → α)
(left_inv  : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)

To make a term of type `equiv α β` you have to supply a function α → β,
a function β → α, and proofs that both composites are the identity function.

Let's see how to create the bijection ℤ → ℤ sending x to -x.
-/
-- let's prove that x ↦ -x can be extended to
example : equiv ℤ ℤ :=
{ to_fun := λ x, -x, -- this is data
  inv_fun := λ x, -x,  -- this is data
  left_inv := begin -- this is a proof
    change ∀ (x : ℤ), - -x = x, -- that's the question
    exact neg_neg, -- note: I guessed what this function was called.
                   -- If it had been called "lemma 12" I would not have been able to guess
  end,
  right_inv := neg_neg -- another proof, this time in term mode
}

/-
Q1 Define the type of partitions of a type.
A partition of X is a set of subsets of X with the property that each subset
is non-empty and each element of X is in precisely one of the subsets.
NB : this is one of the harder questions here.
-/

structure partition (X : Type*). -- remove `.`  and fill in -- look at def of equiv above

/-
Equivalence relations are in core Lean -- we don't need any imports.
Here's an example: I'll prove that the "always true" relation on a set is
an equivalence relation.

-/

def always_true (X : Type*) : X → X → Prop := λ a b, true

-- and now here's the proof that it's an equivalence relation.

theorem always_true_refl (X) : reflexive (always_true X) :=
begin
  intro x,
  trivial
end

theorem always_true_symm (X) : symmetric (always_true X) :=
begin
  intros a b H,
  trivial
end

theorem always_true_trans (X) : transitive (always_true X) :=
begin
  intros a b c Hab Hbc,
  trivial
end

-- note pointy brackets to make a term of type "A ∧ B ∧ C"
theorem always_true_equiv (X): equivalence (always_true X) :=
⟨always_true_refl X, always_true_symm X, always_true_trans X⟩
-- autocomplete made that proof really easy to type. It's really
-- lucky that I didn't call these lemmas lemma 12, lemma 13 and lemma 14.

-- if X is a type, then `setoid X` is is the type of equivalence relations on X.
-- I'll now make a term of type `setoid X` corresponding to that equivalence
-- relation above.

-- note squiggly brackets and commas at the end of each definition to make a structure
def always_true_setoid (X : Type*) : setoid X :=
{ r := always_true X,
  iseqv := always_true_equiv X }

-- right click on `setoid` and peek the definition if you want to see another example of a structure.
/-
Q2 : If X is a type then `setoid X` is the type of equivalence relations on X,
and `partition X` is the type of partitions of X. These two concepts are in
some sort of "canonical" bijection with each other (interesting exercise: make
this statement mathematically meaningful -- I know we all say it, but what
does it *mean*?).

Let's prove that these sets biject with each other by defining
a term of type equiv (setoid X) (partitions X)
-/

variable {X : Type*}

def F (S : setoid X) : partition X := sorry

/-
Q3 : now define a map the other way
-/

def G (P : partition X) : setoid X := sorry

/-
Q4 : now finally prove that the composite of maps in both directions
is the identity
-/

theorem FG_eq_id (P : partition X) : F (G P) = P := sorry
theorem GF_eq_id (S : setoid X) : G (F S) = S := sorry

/-
Q5 : now finally construct the term we seek.
-/

def partitions_biject_with_equivalence_relations :
  equiv (setoid X) (partition X) := sorry

[Kevin Buzzard]

@Greg Conneen

[Greg Conneen]

Okay, I see. Thank you for the homework, I'll get to work on it as soon as I can. Sorry about the late response, that was 4am local time

[Kevin Buzzard]

Feel free to ask when you get stuck. There's a lot to do there, I know the maths sounds trivial, but I was surprised when I formalised it just how much was in there.

[Kevin Buzzard]

If you want to go even further at the end, you could prove that an equiv from X to Y induces equivs from partition X to partition Y and from setoid X to setoid Y`, and then you could prove that your construction made the square commute. That would be my answer to the question about why the construction we all know is "canonical"

[Kevin Buzzard]

Maybe you can even prove that your construction is an equivalence of categories from the groupoid of setoids to the groupoid of partitions. @Reid Barton is there enough category theory in core to be able to formalise this statement? What do you think of it as a working definition for "canonical" in what people might call "the canonical construction sending an equivalence relation to its equivalence classes"?

[Greg Conneen]

Ah, that sounds like fun. I've done enough category theory to feel comfortable with that on paper, but seems a bit more daunting in Lean

[Kevin Buzzard]

@Mario Carneiro @Scott Morrison can you write me a function which takes as input a simple structure (such as setoid) as input and returns some sort of groupoid? Am I asking for some sort of groupoid typeclass here on structures like partition or am I just talking nonsense?

[Kevin Buzzard]

Recently I've got interested in making loads of equivs, because they've been coming up in the way I think about mathematics. An equiv of setoids is just an equiv of the underlying types such that some diagrams involving the binary relations, all commute.

[Kevin Buzzard]

And I can define two setoids to be isomorphic if there existed an equiv and that's some groupoid I guess.

[Kevin Buzzard]

and then one could suggest that a functor was canonical if it commuted with the groupoid structures.

[Greg Conneen]

This is what I've got so far for my definition of a partition:

structure partition (X : Type*) :=
(subs : set (set X))
(part_nonempty : ∀ k : subs, nonempty k)
(ex_incl : ∀ a : X, ∃ k : subs, a ∈ k)
(unique_incl (k j : subs) (a : X) : k ≠ j → a ∈ k → a ∉ j)

but it throws an error on ex_incl since Lean doesn't know that objects of type subs can have elements, I think. Is something of type subs a (set X)? I assumed that's how Lean would handle it, but now I don't know if I've got the right type for k.

[Greg Conneen]

Or does it specifically have to do with the fact that I'm using the element of symbol?

[Johan Commelin]

@Greg Conneen Here is my rough attempt at Cayley:

import data.equiv.basic
import algebra.group

open equiv function
variables (G : Type*) [group G]

def cayley_fun : G → (perm G) :=
λ g,
{ to_fun := λ h, g * h,
  inv_fun := λ h, g⁻¹ * h,
  left_inv := λ h, show g⁻¹ * (g * h) = h, by { rw ← mul_assoc, simp },
  right_inv := λ h, show g * (g⁻¹ * h) = h, by { rw ← mul_assoc, simp } }

lemma cayley_inj : injective (cayley_fun G) :=
begin
  intros g₁ g₂ H,
  replace H := congr_arg equiv.to_fun H,
  replace H := congr H (rfl : (1 : G) = 1),
  simpa [cayley_fun] using H,
end

theorem cayley_hom : is_group_hom (cayley_fun G) :=
{ map_mul :=
begin
  intros g₁ g₂,
  ext h,
  exact mul_assoc g₁ g₂ h,
end }

[Greg Conneen]

I'm getting an error at cayley_hom saying mul was not provided and map_mul is not a field or structure

[Greg Conneen]

(deleted)

[Greg Conneen]

Oh, it was fixed by replacing the name map_mul with mul. nvm

[Johan Commelin]

Are you on up to date mathlib?

[Greg Conneen]

...probably not

[Greg Conneen]

And I'm not quite sure how to go about updating it. It's been quite a while since I did

[Kevin Buzzard]

The advantage of staying up to date is that code posted here is more likely to run. Mathlib moves fast and breaks things, and actually seeing your old code break when mathlib breaks is quite interesting, because it's either a change to mathlib which you should know about, or it's because your proof doesn't work any more because it was poorly written. Patrick, Johan and I work hard to keep up with mathlib in our project.

[Kevin Buzzard]

Our project has its own .toml file which says exactly which version of mathlib we are using. And then once every few weeks we try and update

[Greg Conneen]

How would I go about updating mathlib? I'm probably using a fall 2018 release

[Kevin Buzzard]

how are you using it currently?

[Keeley Hoek]

#ElanEverytime

[Greg Conneen]

It's sitting in _target. I installed using elan, but am not at all familiar with the use of elan. I just followed directions on a github ReadMe somewhere.

[Bryan Gin-ge Chen]

I believe the recommended way is to use the update-mathlib script. See this section of the mathlib readme. Since I've installed that script, I just type leanpkg upgrade and then update-mathlib in the root folder of my lean projects. Make sure that your leanpkg.toml has a line that says lean_version = "3.4.2" at the top.

[Kevin Buzzard]

so you are working in a project? Does the project have a toml file? If so, it might be as simple as running "leanpkg upgrade"

[Greg Conneen]

Yes, my project has a toml file. It does in fact have 3.4.2 as the version number

[Greg Conneen]

Says I should run source /c/Users/Greg/.profile after updating, but threw an error

[Bryan Gin-ge Chen]

Do you mean that the curl command to install update-mathlib threw an error? What was the error?

[Greg Conneen]

No. That didn't throw an error. Once I was done updating, it told me to run another command

[Kevin Buzzard]

Computer people like it if you just cut and paste everything and upload it all so they can see what the actual errors were?

[Kevin Buzzard]

Turns out it means something to them :-)

[Greg Conneen]

Yeah. I'm going to send a picture in just a moment.

[Greg Conneen]

Fixed the issue.

[Greg Conneen]

I still don't know what's wrong with this, though:

structure partition (X : Type*) :=
(subs : set (set X))
(part_nonempty : ∀ k : subs, nonempty k)
(ex_incl : ∀ a : X, ∃ k : subs, a ∈ k)
(unique_incl (k j : subs) (a : X) : k ≠ j → a ∈ k → a ∉ j)

[Kevin Buzzard]

(ex_incl : ∀ a : X, ∃ k ∈ subs, a ∈ k)

[Kevin Buzzard]

subs is a set not a type

[Greg Conneen]

ohhhh

[Greg Conneen]

I see, thank you

[Greg Conneen]

Also, top kek @ your comments on lines 28 and 82