Playing with free groups

Stream: new members

[Laurent Bartholdi]

I tried to get back to my questions about free groups, and tried the following. Can some kind soul please help me out?

import group_theory.free_group

def f := free_group bool

def g1 := free_group.mk [(tt,tt)]
def g2 := free_group.mk [(ff,tt)]
def G1 := free_group.mk [(tt,ff)]
def G2 := free_group.mk [(ff,ff)]

theorem trivialthm1 : g1⁻¹ = G1 := begin -- this one is easy, it's by definition
  refl,
end

theorem trivialthm2 : g1 ≠ g2 := begin -- this is easy too, the map bool -> f is injective. Is there a way to golf it down to a single command?
  intro h,
  let k := free_group.of_injective h,
  tauto,
end

theorem trivialthm3 : g1 ≠ 1 := begin -- this is hard (for me)
  intro j,
  let k := free_group.reduce.sound j, -- now goal is "false", and hypothesis is "free_group.reduce [(tt, tt)] = free_group.reduce list.nil"
  -- I want to say that these reductions are [(tt,tt)] and list.nil respectively, using free_group.reduce.cons
  -- and then say that the reductions are different, contradiction.
  -- I could do none of these things :(
  sorry,
end

[Scott Morrison]

cases k

[Kevin Buzzard]

theorem trivialthm2 : g1 ≠ g2 :=
λ h, bool.no_confusion $ free_group.of_injective h

[David Wärn]

It's maybe nicer to directly define

g1 := free_group.of tt
g2 := free_group.of ff
G1 := g1⁻¹
G2 := g2⁻¹

For longer words you can just multiply the generators. The list stuff is sort of an implementation detail that you as an end-user shouldn't have to see. Of course free_group.reduce.sound will still give you an equality of lists (as it should), but you don't need to start with lists.

[Eric Wieser]

Hooray, my speculative adding of docs#free_group.of_injective turned out to be useful! edit: looks like I didn't add that one after all

[Laurent Bartholdi]

Great, thanks a lot! now, harder: a free group on 3 generators! Am I creating a type with 3 elements in the correct way? (I know I could put everything into a "free_group \nat", but I'd also like to be able to define free groups of finite rank \ne 2). How do I tell lean that three's elements are distinct, and that there are exactly these three?

import group_theory.free_group

inductive three : Type
| x : three
| y : three
| z : three

def f := free_group three

def g1 := free_group.of three.x
def g2 := free_group.of three.y
def g3 := free_group.of three.z

theorem trivialthm1 : g1*g2*g2⁻¹*g1⁻¹ = 1 := by simp

theorem trivialthm2 : g1 ≠ g2 := λ h, by cases free_group.of_injective h

theorem trivialthm3 : g1 ≠ 1 := λ h, by cases free_group.reduce.sound h
-- fails: needs to know "decidable_eq three"

[David Wärn]

You can use fin 3

[Laurent Bartholdi]

David Wärn said:

You can use fin 3

Very nice! So I'm happy with

def f := free_group (fin 3)

def g1 := free_group.of (0 : fin 3)
def g2 := free_group.of (1 : fin 3)
def g3 := free_group.of (2 : fin 3)

Now, something I don't understand (and could be unrelated): why is def g2 := free_group.of (4 : fin 3) legal? I guess types don't have cardinalities, but it seems I can coerce every natural into fin 3, meaning it has more than 3 elements!

[Anne Baanen]

fin n works modulo n, so (0 : fin 3) = (3 : fin 3) = (6 : fin 3) = ...

[David Wärn]

Actually Lean knows that free_group A has decidable equality whenever A does, so you can also write things like

open free_group
def x : free_group (fin 3) := of 0
def y : free_group (fin 3) := of 1
def z : free_group (fin 3) := of 2
example : x * y * x⁻¹ ≠ z := dec_trivial
example : x * x * x⁻¹ = x := dec_trivial

[Laurent Bartholdi]

Thanks @David Wärn ! That's two hole-in-one in a row!

[Kevin Buzzard]

The original inductive definition of three would also have been fine -- if you prefix it with @[derive decidable_eq] then probably the proofs would work just the same. You can't push dec_trivial too far though. However an MSc student of mine, Chris Hughes, has been working on group theory algorithms in Lean and he has some working tactics which can solve equalities and inequalities even in finitely presented groups (of course this is not decidable in general, but the algorithm just has a go and often succeeds).

[Kevin Buzzard]

@Laurent Bartholdi if you want a challenge, this recent work of Gardam disproving the unit conjecture for group rings got some press coverage recently and would probably be an interesting but feasible challenge to do in Lean. I talked to @Chris Hughes about it who pointed out that it would not be immediately straightforward but the arguments seem to me to be very amenable to formalisation.

[Laurent Bartholdi]

That's a great idea! Unfortunately I'm again stuck at basics:

import group_theory.free_group
import algebra.monoid_algebra

open free_group

def x : free_group (fin 2) := of 0
def y : free_group (fin 2) := of 1
example : x * y ≠ y * x := dec_trivial

def rx := (monoid_algebra.of ℤ (free_group (fin 2))) x -- noncomputable!
def ry := (monoid_algebra.of ℤ (free_group (fin 2))) y -- noncomputable!
-- and: how do I avoid re-typing this "(monoid_algebra.of ℤ (free_group (fin 2)))"?

example : rx ≠ ry := dec_trivial -- understandably, fails

If I can get this running, though, I think the Gardam paper will be easy to formalize. It's a matter of defining a group by 2x2 matrices, which we could do using (explicitly) invertible functions Z^2->Z^2, and have everything be evaluated by lean.

[Laurent Bartholdi]

@Kevin Buzzard I should add that I convinced a few students to learn lean with me, and hopefully they'll soon be more expert than me. A suggestion I made was to formalize the ping-pong lemma (https://en.wikipedia.org/wiki/Ping-pong_lemma), at least in its simplest form (proving that an action of a free group is faithful). Do you see any objections to this project?

[Alex J. Best]

Here is how to do what you want:

import group_theory.free_group
import algebra.monoid_algebra
noncomputable theory -- disables the noncomputable warning
open free_group

def x : free_group (fin 2) := of 0
def y : free_group (fin 2) := of 1
example : x * y ≠ y * x := dec_trivial

open monoid_algebra -- so we can jsut write `of` below, slightly less copy pasting
def rx := of ℤ _ x  -- because lean knows where x and y live the free_group (fin 2) is duplicate information and you can leave that out with an underscore
def ry := of ℤ _ y

example : rx ≠ ry :=
begin
  intro h,
  have := monoid_algebra.of_injective h, -- key lemma
  exact (dec_trivial : x ≠ y) this,  -- same idea as your first example, one we have a statement about the free group over fin 2 everything is checkable by lean
end

[Kevin Buzzard]

@Laurent Bartholdi this is what happened to me -- I introduced some students to Lean and after a while they started teaching it to me. @Chris Hughes is an example -- Chris, do you think the ping pong lemma would be formalisable in a relatively straightforward manner?

[Kevin Buzzard]

Re: the Gardam paper -- Chris already pointed out to me that if you're not careful then you might find it hard to prove that the unit he constructs is not of the form lambda*g, i.e. you'll need to prove that various elements of your group are distinct. There seemed to be two ways of thinking about the group in the paper -- one as an extension of Z/2 x Z/2 by Z^3 and another as some explicit finite presentation. I don't know a maths proof that these two groups are equal (but I didn't look at the paper carefully and I don't know this stuff at all -- Chris has been doing his MSc project with me on finitely generated groups in Lean so might well know more)

[David Wärn]

Another simple result about free groups, which I think would be nice to see in Lean, is the fact that the free group on two generators contains as a subgroup a free group on infinitely many generators

[Chris Hughes]

I think proving the ping pong lemma should be fairly easy. It actually looks easier than proving associativity of multiplication of the free product. I do think that working with free groups is generally extremely challenging, there are a lot of arguments about the normal form that are intuitive on paper but very challenging to formalize. There are a bunch of questions about the best approach to this stuff. I think it might even be sensible to work mostly with binary coproducts, and then transfer to larger coproducts. Binary coproducts can be implemented as a subtype of H × list (G × H) × G, with the stipulation that none of the pairs in the list is 1. The element (h₁, [(g₂, h₂)], g₃) would represent the element $h_1g_2h_2g_3$. You could also just do the list of pairs and stipulate that the first and last elements are allowed to be one. It would require a lot of work to really work out how to properly reason with free groups. An elegant proof of associativity of multiplication of reduced words would be a nice start.

[Chris Hughes]

I do think the current interface for free groups isn't anywhere near enough to reason about normal forms. I have some [code](https://github.com/ChrisHughes24/single_relation/tree/master/src/coprod about normal forms of coproducts of groups, but the associativity proof is messy and it's not mathlib ready. I don't have time right now to work on it, but I certainly wouldn't be offended if someone else PRed it or modified it.

[Chris Hughes]

David Wärn said:

Another simple result about free groups, which I think would be nice to see in Lean, is the fact that the free group on two generators contains as a subgroup a free group on infinitely many generators

The argument I know for this is that $F(2)$ is isomorphic to $F(\mathbb{Z}) \rtimes \mathbb{Z}$, where $\mathbb{Z}$ acts on $F(\mathbb{Z})$ by extending the left regular action of $\mathbb{Z}$ on itself. This is all really easy in Lean right now.

[David Wärn]

Huh, I wasn't aware of this argument. I suppose you just show that left (of 0) and right 1 freely generate this semidirect product? Anyway I agree it shouldn't be difficult. The argument I had in mind was to consider the kernel of $F(2) \to \mathbb Z$ sending $x$ to $0$ and $y$ to $1$, using docs#subgroup_is_free_of_is_free, and doing a bit of work to show that the set of generators is really $\{y^n x y^{-n} \mid n \in \mathbb Z\}$ (it's this picture where you have an infinite path and a loop at every vertex).

[Kevin Buzzard]

My favourite theorem about finitely generated free groups is that a subgroup of index n is also f.g. free and the Euler characteristic 2g-2 gets multiplied by n, e.g. an index 2 subgroup of F(2) must be free on 3 generators. The proof I know is topological.

[David Wärn]

You can deduce this from what's currently in mathlib without too much effort! I did so here (except you need to perform some subtractions to get the usual version with finite ranks)

[David Wärn]

I mean mathlib now has the "free" part, you just need to do a bit more work to get the formula relating rank and index

[Kevin Buzzard]

Oh nice -- a constructive version!

[Eric Rodriguez]

I had no clue that the formula for the group's size was because of Euler's characteristic - that's really cool

[David Wärn]

Chris Hughes said:

I do think the current interface for free groups isn't anywhere near enough to reason about normal forms. I have some code about normal forms of coproducts of groups, but the associativity proof is messy and it's not mathlib ready. I don't have time right now to work on it, but I certainly wouldn't be offended if someone else PRed it or modified it.

There's a reasonably nice way to do this, where you take the set of reduced words and act on it one letter at a time, but mabye this is as complicated as what you currently have? Suppose we want to construct $\coprod_i G_i$. For $w$ a reduced word and $g \in G_i$, define the reduced word given by prepending $g$ to $w$ (this is your rcons). Then show that this determines an action of $G_i$ on the set of reduced words. It's obviously faithful, by acting on the empty word. So for each $i$ we can view $G_i$ as a subgroup of the symmetric group on the reduced words. Then take the subgroup generated by all of these, and show it bijects with the set of reduced words

[David Wärn]

Kevin Buzzard said:

Oh nice -- a constructive version!

It's not completely constructive since taking spanning trees in the infinite-index case is verboten

[Chris Hughes]

I proved that $F(Z)$ embeds into $F(2)$ https://gist.github.com/ChrisHughes24/6829f57b86cb00b1067011f673c472b4 Nowhere near as pretty as I'd like. There's some missing simp lemmas in the library about how a bunch of stuff like mul_action.to_perm behave.

[Chris Hughes]

It's a special case of a more general argument saying $G \ast H \cong (\coprod_{h \in H} G) \rtimes H$

[Laurent Bartholdi]

Alex J. Best said:

Here is how to do what you want:

import group_theory.free_group
import algebra.monoid_algebra
noncomputable theory -- disables the noncomputable warning
open free_group

def x : free_group (fin 2) := of 0
def y : free_group (fin 2) := of 1
example : x * y ≠ y * x := dec_trivial

open monoid_algebra -- so we can jsut write `of` below, slightly less copy pasting
def rx := of ℤ _ x  -- because lean knows where x and y live the free_group (fin 2) is duplicate information and you can leave that out with an underscore
def ry := of ℤ _ y

example : rx ≠ ry :=
begin
  intro h,
  have := monoid_algebra.of_injective h, -- key lemma
  exact (dec_trivial : x ≠ y) this,  -- same idea as your first example, one we have a statement about the free group over fin 2 everything is checkable by lean
end

Great! however, I'm stuck now an inch further:

example : (0 : monoid_algebra ℤ (free_group (fin 2))).support = ∅ := begin
  simp at *,
end

example : rx.support = {x} := sorry

example : rx ≠ 0 :=
begin
  suffices : rx x ≠ (0 : monoid_algebra ℤ (free_group (fin 2))) x,
  sorry,
end

It seems to me that, generally speaking, it's good to argue about supports of elements in a group ring. However, I find it hard to dec_trivial away any of the examples, such as the next-to-last one.

As I understand it, elements of a group ring are functions, so it makes sense to evaluate them. This is what I try in the last example : show two functions differ because they have different values at x.

[Laurent Bartholdi]

David Wärn said:

There's a reasonably nice way to do this, where you take the set of reduced words and act on it one letter at a time, but mabye this is as complicated as what you currently have? Suppose we want to construct $\coprod_i G_i$. For $w$ a reduced word and $g \in G_i$, define the reduced word given by prepending $g$ to $w$ (this is your rcons). Then show that this determines an action of $G_i$ on the set of reduced words. It's obviously faithful, by acting on the empty word. So for each $i$ we can view $G_i$ as a subgroup of the symmetric group on the reduced words. Then take the subgroup generated by all of these, and show it bijects with the set of reduced words

I second this -- the reference is [van der Waerden, B. L. Free products of groups. Amer. J. Math. 70 (1948), 527–528. https://doi.org/10.2307/2372196]. The article really feels like van der Waerden had formalization in mind!

[David Wärn]

Thanks for this reference! I only knew it as a folklore idea, so it's nice to see the reference. I wrote up a definition of coproducts in PR #7395 using some of these ideas. It turned out quite nice.

[David Wärn]

For supports in the monoid algebra: there is a lemma called finsupp.support_single_ne_zero which should do what you want. Note the it relies on the non-obvious fact 1 ≠ 0. simp can help you with the second sorry if you let it know what rx is (e.g. simp [rx])

[Laurent Bartholdi]

David Wärn said:

For supports in the monoid algebra: there is a lemma called finsupp.support_single_ne_zero which should do what you want. Note the it relies on the non-obvious fact 1 ≠ 0. simp can help you with the second sorry if you let it know what rx is (e.g. simp [rx])

I just feel I managed to conquer Mt Everest:

lemma x_ne_y : x ≠ y := dec_trivial

example : rx + ry ≠ 0 := begin
  rw finsupp.nonzero_iff_exists,
  use x,
  simp [rx,ry],
  rw finsupp.single_apply,
  simp [x_ne_y.symm],
end

Is there a better way to do this? In particular, how do I avoid putting "simp" everywhere?

[Eric Wieser]

A shorter proof:

example : rx + ry ≠ 0 := begin
  rw [rx, ry, monoid_algebra.of_apply, monoid_algebra.of_apply, finsupp.nonzero_iff_exists],
  use x,
  rw [finsupp.add_apply, finsupp.single_eq_same,finsupp.single_eq_of_ne x_ne_y.symm, add_zero],
  exact one_ne_zero,
end

[Eric Wieser]

Or a different strategy:

example : rx + ry ≠ 0 := begin
  dunfold rx ry,
  rw [monoid_algebra.of_apply, monoid_algebra.of_apply, ne.def, ←eq_neg_iff_add_eq_zero,
    ←finsupp.single_neg, finsupp.single_eq_single_iff],
  simp [x_ne_y],
end

where docs#finsupp.single_eq_single_iff does most of the work

[Laurent Bartholdi]

OK, my next attempt: a new tactic! There are 2 things I could not find in the documentation: how to use a tactic variable (here "elt"), and how to construct on-the-fly a proof of equality / inequality of group elements:

meta def group_ring_ne_zero_at {g : Type} [group g] (elt : g) : tactic unit := `[repeat { rw monoid_algebra.of_apply },
          rw finsupp.nonzero_iff_exists,
          use x, -- here "use elt" does not work :(
          repeat { rw finsupp.add_apply },
          repeat { rw [finsupp.single_eq_same,finsupp.single_eq_of_ne x_ne_y.symm] }, -- I want the tactic to look up the variable of the present term, and try to prove (by dec_trivial) that they're equal or unequal
          simp
         ]

example : rx + rx + ry ≠ 0 := begin
  repeat { rw [rx, ry] },
  group_ring_ne_zero_at x
end

[Scott Morrison]

Yes, it's unfortunately the case that you can't use antiquotations to embed variables inside `[...] blocks.

[Scott Morrison]

Instead you need to lean the distinction between "interactive" tactics and non-interactive tactics, and use these "under the hood" tactics.

[Scott Morrison]

If you jump-to-definition on use, you'll see that it immediately calls tactic.use, which is the underlying non-interactive tactic.

[Scott Morrison]

However you'll see that use doesn't take a g, of course, it takes a list pexpr.

[Scott Morrison]

pexpr is a "pre-expression": a "meta" representation of some mathematical term.

[Scott Morrison]

When you actually use use inside a begin ... end block the parser takes care of converting what you thinking of as "the actual mathematical thing x" into this pexpr representation of it.

[Scott Morrison]

(Of course, Lean itself knows nothing about "the actual mathematical thing", and is just manipulating pexpr and expr objects in the C++ code.)

[Scott Morrison]

So if you want to do this too in your tactic you'll need to learn a bit about the parser, and take pexpr arguments as appropriate.

[Scott Morrison]

Explaining all that is perhaps beyond the scope of this thread, but you should watch Rob Lewis' excellent tutorial from LFTCM2020, and its associated exercises.

[Scott Morrison]

https://www.youtube.com/playlist?list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2

[Holly Liu]

David Wärn said:

Actually Lean knows that free_group A has decidable equality whenever A does, so you can also write things like

open free_group
def x : free_group (fin 3) := of 0
def y : free_group (fin 3) := of 1
def z : free_group (fin 3) := of 2
example : x * y * x⁻¹ ≠ z := dec_trivial
example : x * x * x⁻¹ = x := dec_trivial

i'm trying to do proofs with free groups and was wondering what the "of" notation means, and where else it could be used? or if you could link me somewhere? also, does free_group.of and of do the same things?
could you also explain how fin 3 is implemented?

[Alex J. Best]

If the namespace free_group is open (which will happen if we run open free_group) then yes of will very likely be shorthand for free_group.of

[Alex J. Best]

Does the docstring at docs#free_group.of help?

[Alex J. Best]

fin 3 is a simple to use type with only 3 terms/elements, a term of fin 3 is a natural number n and a proof that n is less than 3. As the proofs don't change which terms are equal you can just think of these terms as the number 0,1,2.

[Alex J. Best]

So of 0 is the generator corresponding to the number 0 of the free group generated by the terms 0, 1, 2

[Alex J. Best]

Where these terms have no relations between them in the free group

[Holly Liu]

that helps a lot, thanks. is def g1 := free_group.of tt creating a list (g1 x tt)? and is list (g1 x ff) its inverse?

[Holly Liu]

actually, is it the generator corresponding to the bool true of the free group?

[Alex J. Best]

Yeah the second thing, its just a single term of type free_group bool

[Holly Liu]

ok. is there a difference between usingtt or ff?

[Alex J. Best]

The terms tt (true) and ff (false) are the two distinct terms of bool so the corresponding of tt and of ff are terms of free_group boolthat are not equal.

[Holly Liu]

i was wondering where quot.mk is defined? i found the following snippet at https://github.com/leanprover-community/lean/blob/a5822ea47ebc52eec6323d8f1b60f6ec025daf99/library/init/data/quot.lean#L93 that uses mk in the definition of mk, which I am a bit confused about.

protected def mk {α : Sort u} [s : setoid α] (a : α) : quotient s :=
quot.mk setoid.r a

[Bryan Gin-ge Chen]

quot is a bit special, it's added by the command init_quotient here.

[Bryan Gin-ge Chen]

Section 11.4 of TPiL is about quotient types in Lean.

[Kevin Buzzard]

This is docs#quotient.mk being defined in terms of quot.mk, which is defined by magic at start-up in an unconventional way.