First problems in group theory

Stream: new members

[Laurent Bartholdi]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Laurent Bartholdi]

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

[Johan Commelin]

It doesn't know that pi is transcendental

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Lean knows that it is a group.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

(Sorry, no unicode nearby...)

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Rob Lewis]

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?

[Patrick Massot]

Oh sorry. It's unfolding again.

[Patrick Massot]

So I could have written

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

[Patrick Massot]

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

[Yury G. Kudryashov]

For +1 we have equiv.add_right.

[Yury G. Kudryashov]

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

[Rob Lewis]

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

What's the second failing instance?

[Patrick Massot]

is_group_hom LB2_map

[Patrick Massot]

It needs the big message with 67 lines of code.

[Patrick Massot]

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.

[Patrick Massot]

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

[Rob Lewis]

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

[Yury G. Kudryashov]

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

[Laurent Bartholdi]

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.

[Floris van Doorn]

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

[Floris van Doorn]

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

[Floris van Doorn]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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.

[Rob Lewis]

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.

[Chris Hughes]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Daniel Keys]

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.

[Sebastien Gouezel]

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

[Daniel Keys]

@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?

[Floris van Doorn]

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 :=
[...]

[Floris van Doorn]

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.

[Daniel Keys]

OK, now it all makes sense!

[Floris van Doorn]

In your manual proof, try using deriv_add and deriv_id.

[Daniel Keys]

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

[Floris van Doorn]

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

[Daniel Keys]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Sebastien Gouezel]

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.

[Johan Commelin]

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