Zulip Chat Archive

Stream: new members

Topic: First problems in group theory


view this post on Zulip Laurent Bartholdi (Feb 11 2020 at 14:30):

Hello world!
I played enough of the "number game" that I thought I should try something a bit different -- more in my area, and more advanced.

I checked that Lean has the concepts of group, and in particular finite groups, built-in. I was thinking about proving the following theorems, in order of difficulty:
-- The group generated by x->x+1 acting on the reals is the free group <a|>
-- The group generated by x->x+1 and x->2x has as presentation <a,b|ab=ba^2>
-- The group generated by x->x+1 and x->x^3 is the free group <a,b|>

Any opinions on whether this is a sensible task for a newbie?

TIA, Laurent

view this post on Zulip Johan Commelin (Feb 11 2020 at 14:36):

@Laurent Bartholdi What exactly do you mean with "the group generated by x -> x+1 and x -> x^3"?

view this post on Zulip Johan Commelin (Feb 11 2020 at 14:37):

Are you fixing a real number, and then taking the closure under those functions?

view this post on Zulip Johan Commelin (Feb 11 2020 at 14:38):

Anyway, I think such statements can be done in Lean, although there might be some annoying technicalities.

view this post on Zulip Laurent Bartholdi (Feb 11 2020 at 14:45):

Are you fixing a real number, and then taking the closure under those functions?

There are two options. I could think about maps on the reals, and this is my preferred choice. I could also think of the orbit of \pi under these operations (assuming lean knows that \pi is transcendental, of course).

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:23):

It doesn't know that pi is transcendental

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:24):

Aha, so you want to look at subgroups of Aut(R), sorry, I was being dense.

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:25):

There is something called \R \equiv \R, which is all bijections from R to itself.

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:25):

Lean knows that it is a group.

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:25):

Lean also knows how to generate a subgroup from a set.

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:26):

So you could start by building the bijections that you stated in your post. That would be task 0.1 I guess

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:27):

def add_one : \R \equiv \R :=
{ to_fun := sorry,
  inv_fun := sorry,
  left_inv := sorry,
  right_inv := sorry }

def double : \R \equiv \R := sorry

def pow_three : \R \equiv \R := sorry

view this post on Zulip Johan Commelin (Feb 11 2020 at 15:27):

(Sorry, no unicode nearby...)

view this post on Zulip Kevin Buzzard (Feb 11 2020 at 16:48):

It will be no problem proving that the group generated by xx+1x\mapsto x+1 is isomorphic to the free group.

view this post on Zulip Kevin Buzzard (Feb 11 2020 at 16:58):

For the others, I don't know a formal maths proof but it wouldn't surprise me if it were straightforward for an expert to formalise, although it might be long for a beginner.

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:40):

Laurent, the honest answer is: everything is hard, but it's a lot of fun.

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:44):

What Johan wrote is probably not enough to get you started. The first point is that, for computer science related reasons, a lot of things in mathlib are setup in terms of this equiv structure which packages a map, its inverse and proofs that the inverse is indeed a left and right inverse. Of course from a mathematics perspective, it has no additional content compared to a map and a proof of bijectivity, but from a computational perspective it's different. This is slightly painful but it would be much worse if you wanted to use Coq whose community is full of people who care about computations.

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:45):

We also have an abbreviation for self-equiv called perm. So the map x+1 seen as a permutation of reals is defined as:

def T : perm  :=
{ to_fun := λ x, x+1,
  inv_fun := λ x, x-1,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp }

The last two lines are the proofs, they are crushed by the simplifier.

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:48):

Then the subgroup spanned by T is: group.closure ({T} : set (perm ℝ)). Note that it should be enough to write group.closure {T} but Lean3's elaborator is failing badly here (this is a known bug) so we need to tell it explicitly that this singleton {T} is a set of permutations of ℝ.

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:49):

Question @Mario Carneiro and @Rob Lewis who seem to be around. Do you have any idea why Lean doesn't immediately get a subgroup instance on that group closure?

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:50):

Minimal example here:

import data.real.basic
import group_theory.free_group
open equiv function
open_locale classical
noncomputable theory

def T : perm  :=
{ to_fun := λ x, x+1,
  inv_fun := λ x, x-1,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp }

namespace LB1
-- The subgroup generated by T
def LB1 := group.closure ({T} : set (perm ))

instance : is_subgroup LB1 := group.closure.is_subgroup _  -- by apply_instance fails

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:52):

Next trap for Laurent. You may think that T belongs to LB1. But elements of LB1 are packages containing a permutation and a proof that it belongs to the subgroup spanned by T. So you need something like def t : LB1 := ⟨T, group.in_closure.basic (by simp) to define t which is T seen as an element of LB1 (we could probably write a nice helper function here).

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:54):

Then you need to start reading https://leanprover-community.github.io/mathlib_docs/group_theory/free_group.html or the corresponding Lean file. Unfortunately this was written before we enforced nice documentation requirements. I you like documenting what you understand, you could take this as a challenge to contribute documentation to mathlib.

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:55):

Same applies to https://leanprover-community.github.io/mathlib_docs/group_theory/presented_group.html

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:56):

One possible way to state your first two challenges would then be:

import data.real.basic
import group_theory.free_group
open equiv function
open_locale classical
noncomputable theory

def T : perm  :=
{ to_fun := λ x, x+1,
  inv_fun := λ x, x-1,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp }

namespace LB1
-- The subgroup generated by T
@[derive is_subgroup]
def LB1 := group.closure ({T} : set (perm ))

-- The transformation T seen as an element of the subgroup it generates.
def t : LB1 := T, group.in_closure.basic (by simp)


-- Free group on one generator denoted by ()
@[derive group]
def F₁ := free_group unit

-- Laurent's first map
def LB1_map : F₁  LB1 := free_group.to_group (λ u : unit, t)

lemma LB1_iso : bijective LB1_map :=
sorry

end LB1

def S : perm  :=
{ to_fun := λ x, 2*x,
  inv_fun := λ x, x/2,
  left_inv := λ x, by simp ; ring,
  right_inv := λ x, by simp ; ring }

namespace LB2
@[derive is_subgroup]
def LB2 := group.closure ({T, S} : set (perm ))

def t : LB2 := T, group.in_closure.basic (by simp)
def s : LB2 := S, group.in_closure.basic (by simp)

-- The free group generated by booleans tt and ff
@[derive group]
def F₂ := free_group bool

-- First generator of F
def a : F₂ := free_group.mk [(tt, tt)]
def b : F₂ := free_group.mk [(ff, tt)]

-- Laurent's second map
def LB2_map : F₂  LB2 := free_group.to_group (λ b, if b then t else s)

instance : is_group_hom LB2_map := free_group.to_group.is_group_hom

lemma surj : surjective LB2_map :=
sorry

lemma ker : is_group_hom.ker LB2_map = group.normal_closure {a*b*(b*a^2)⁻¹} :=
sorry
end LB2

view this post on Zulip Patrick Massot (Feb 11 2020 at 17:57):

Understanding that piece should already give you plenty of questions to ask here. For everybody else: note there is another mysterious instance that type class instance resolution is not finding.

view this post on Zulip Rob Lewis (Feb 11 2020 at 17:58):

Question Mario Carneiro and Rob Lewis who seem to be around. Do you have any idea why Lean doesn't immediately get a subgroup instance on that group closure?

import group_theory.perm.all data.real.basic
open tactic equiv

def T : perm  :=
{ to_fun := λ x, x+1,
  inv_fun := λ x, x-1,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp }

example : is_subgroup (group.closure ({T} : set (perm ))) :=
by apply_instance

seems fine?

view this post on Zulip Patrick Massot (Feb 11 2020 at 18:00):

Oh sorry. It's unfolding again.

view this post on Zulip Patrick Massot (Feb 11 2020 at 18:01):

So I could have written

@[derive is_subgroup]
def LB1 := group.closure ({T} : set (perm ))

view this post on Zulip Patrick Massot (Feb 11 2020 at 18:01):

This doesn't work for the second failing instance. derive complains it want a group real instance.

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 18:04):

For +1 we have equiv.add_right.

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 18:04):

I'd define all these subgroups as images of the free group under a lift homomorphism, then study the kernels of these homomorphisms.

view this post on Zulip Rob Lewis (Feb 11 2020 at 18:04):

This doesn't work for the second failing instance. derive complains it want a group real instance.

What's the second failing instance?

view this post on Zulip Patrick Massot (Feb 11 2020 at 18:04):

is_group_hom LB2_map

view this post on Zulip Patrick Massot (Feb 11 2020 at 18:05):

It needs the big message with 67 lines of code.

view this post on Zulip Patrick Massot (Feb 11 2020 at 18:06):

And maybe it's not the right starting point. I only tried to get one, but maybe Yury has a better way. I don't know group theory in mathlib.

view this post on Zulip Patrick Massot (Feb 11 2020 at 18:07):

There should be a nice documented way of formalizing those kind of questions, but I don't think anyone did this yet (at least it doesn't seem documented).

view this post on Zulip Rob Lewis (Feb 11 2020 at 18:09):

Oh, I think the derive handler is struggling with the function type there like in #1951. I'll look into it eventually.

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 18:10):

BTW, it would be nice to turn equiv.mul_left (or _right?) into a group homomorphism G →* (mul_equiv G G)

view this post on Zulip Laurent Bartholdi (Feb 11 2020 at 20:21):

Thanks to all, esp. @Patrick Massot for getting me on the horse.

Indeed I do have some questions, that I can't answer myself.
1) why the "instance : is_group_hom LB2_map := free_group.to_group.is_group_hom"? I understand "instance" as forcing is_group_hom(LB2_map) to be non-empty by supplying an instance; but why isn't it automatic? Maybe I'm missing the point of the discussion in the following messages

2) what are the angles in "⟨T, group.in_closure.basic (by simp)⟩"? Is it that we would like to write "def t : LB2 := T" but need to help lean perform the type conversion? Are the angles equivalent to "begin... end"?

3) I tried, of course, LB3 :). However,
def R : perm ℝ :=
{ to_fun := λ x, x^3,
inv_fun := λ x, x^(1/3),
left_inv := λ x, by simp ; ring,
right_inv := λ x, by simp ; ring }

and lean complains that (x^3)^(1/3) cannot be simplified. I grep'ed through deps/mathlib/src hoping to find something on real numbers, but failed.

view this post on Zulip Floris van Doorn (Feb 11 2020 at 20:41):

You can put code between triple backticks (```) to format it nicely.

view this post on Zulip Floris van Doorn (Feb 11 2020 at 20:43):

(1) Lean doesn't unfold definitions when checking whether is_group_hom(LB2_map) is non-empty, so we have to tell it explicitly. Alternatively you can mark LB2_map as reducible (with @[reducible] def LB2_map ...) and then it will be unfolded.

view this post on Zulip Floris van Doorn (Feb 11 2020 at 20:44):

(2) These are "anonymous constructors". When providing any kind of tuple (for example an inhabitant of a structure) you can use it to provide the fields.

view this post on Zulip Patrick Massot (Feb 11 2020 at 20:52):

I don't think Lean reads that x^(1/3) the way you would expect it.

view this post on Zulip Patrick Massot (Feb 11 2020 at 20:52):

I guess it uses division on natural number and makes it x^0. @Chris Hughes can you help here?

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 20:58):

I guess you need to tell lean that this one is a real number

view this post on Zulip Patrick Massot (Feb 11 2020 at 20:58):

Laurent, you need to read a bit more if you only played the natural number game and want to do more. Did you get https://github.com/leanprover-community/tutorials/ and played a bit with the unique lean file it contains? You should also read Theorem Proving in Lean. If you use VScode you can type Ctrl-Shift-p and then type doc (you should see in the menu Lean: Open documentation view) and then Enter. This will open the book webpage and allow you to try the examples right in VScode.

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:58):

It doesn't. You probably want

to_fun := λ x, x^(3 : ),
inv_fun := λ x, x^(1/3 : ),

but then the proofs of left_inv and right_inv are harder.

view this post on Zulip Chris Hughes (Feb 11 2020 at 20:58):

I just checked, and there isn't actually a nice way to take cube roots in the reals right now. rpow is the function for reals to the power of reals, but it returns junk when the first real is negative (I think it will return the real part of one of the complex cube roots, but not the real cube root). There should probably be a theorem saying there are real nth roots of negative numbers when n is odd

view this post on Zulip Patrick Massot (Feb 11 2020 at 21:00):

This is what I feared. Cube roots of real numbers are not used to solve the cap set problem or define perfectoid spaces.

view this post on Zulip Patrick Massot (Feb 11 2020 at 21:00):

mathlib is still very young and such embarrassing holes are not uncommon.

view this post on Zulip Daniel Keys (Feb 11 2020 at 21:22):

Is there a way to take derivatives, even only point-wise, for simple functions like polynomials? I just tried to, but couldn't get more than a Prop so far.

view this post on Zulip Sebastien Gouezel (Feb 11 2020 at 22:24):

If f is a real function, deriv f x is the derivative of f at the point x.

view this post on Zulip Daniel Keys (Feb 11 2020 at 22:32):

@Sebastien Gouezel Right, that is what I did. What I mean is that I don't seem to be able to get a value, evaluation/reduction fails:

import data.real.basic
import analysis.calculus.deriv

def twoX (x : ) :  := x + x
#check twoX
#check has_deriv_at
#check has_deriv_at twoX (2:) (5:) -- type Prop
#check deriv twoX (2:)  -- type real
#eval deriv twoX (2:) -- this fails

Is there something I'm doing wrong?

view this post on Zulip Floris van Doorn (Feb 11 2020 at 22:46):

You cannot use Lean to #eval or #reduce anything on the real numbers: they are not computable. You have to prove that it equals a value:

example : deriv twoX (2:ℝ) = 2 :=
[...]

view this post on Zulip Floris van Doorn (Feb 11 2020 at 22:49):

In proofs, you can use norm_num to compute with specific real numbers, like example : (2:ℝ) + 3 = 5 := by norm_num.
It is imaginable that at some point we will have a similar tactic for computing derivatives, but that time is not now.

view this post on Zulip Daniel Keys (Feb 11 2020 at 22:50):

OK, now it all makes sense!

view this post on Zulip Floris van Doorn (Feb 11 2020 at 22:51):

In your manual proof, try using deriv_add and deriv_id.

view this post on Zulip Daniel Keys (Feb 11 2020 at 22:51):

So do I need to prove for every point I am interested in?

view this post on Zulip Floris van Doorn (Feb 11 2020 at 22:57):

You can do it for all real numbers at the same time:

import data.real.basic
import analysis.calculus.deriv

def twoX (x : ) :  := x + x
example (x : ) : deriv twoX x = 2 :=
begin
  apply has_deriv_at.deriv, apply has_deriv_at.add; apply has_deriv_at_id
end

view this post on Zulip Daniel Keys (Feb 11 2020 at 22:58):

This is very helpful, very glad I asked! Thanks @Floris van Doorn

view this post on Zulip Rob Lewis (Feb 11 2020 at 23:01):

I haven't really worked at all with deriv yet, but should we have (or is there?) a deriv rule simp set? Something like

import analysis.calculus.deriv

#check deriv

mk_simp_attribute deriv_simp "simp rules for deriv"

attribute [deriv_simp] differentiable_at_pow differentiable_at_const
  deriv_add deriv_const deriv_pow

example (x : ) : deriv (λ x : , x^2 + 2) x = 2 * x :=
by simp with deriv_simp

view this post on Zulip Rob Lewis (Feb 11 2020 at 23:02):

@Sebastien Gouezel were we talking about something like this in Pittsburgh?

view this post on Zulip Sebastien Gouezel (Feb 12 2020 at 07:14):

Yes, we talked about this in relationship with the continuity tactic. I was afraid that, on more complicated examples with composition, the apply bug would show up and make a simpset not powerful enough and that one would need a dedicated tactic, but on this example the naive simpset idea works pretty well.

view this post on Zulip Johan Commelin (Feb 12 2020 at 07:37):

The apply bug can now be fixed in lean 3.5.1, right?


Last updated: May 11 2021 at 00:31 UTC