Zulip Chat Archive

Stream: maths

Topic: free groups


Joachim Breitner (Feb 18 2022 at 08:16):

When formalizing free groups, one has the choice of taking all words and then form a quotient (this is done in mathlib), or define the type of normalized words and build the group on top of that (likely with a normalizion function, and multiplication being concatenation followed by normalization).

In a previous life I once formalized them in Isabelle and later in Agda, and made these notes

At first I wanted to follow the same path again and tried to define the free group on the set of fully reduced words. This is the natural way in Isabelle, where the existing setup for groups expects you to define the carrier as a subset of an existing type (the type here being lists of generators and their inverses). But I did not get far, and also I had to start using stuff like DecidableEquivalence, an indication that this might not go well with the intuitionalistic logic. So I changed my approach and defined the free group on all words as elements of the group, with a suitable equivalence relation. This allowed me define the free group construction and show its group properties without any smell of classical logic.

But mathlib isn't shy of classical logic, isn't it? So out of curiosity I wonder why mathlib's definition for free groups is using quotients. Because the support for quotient types is so good, it's worth using it? Or because it is simply simpler?

(One reason I'm asking is because we don't have the free product of groups yet, do we, and they'd probably be constructed similarly.)

Kyle Miller (Feb 18 2022 at 08:31):

The impression I'd gotten with free_group is that it's set up to be able to prove some formal properties about word reduction (for example, docs#free_group.red.church_rosser). If it had been defined using an explicit reduction procedure, then that would entail making arbitrary choices about the order of reduction. Later on, such a procedure ends up being defined (docs#free_group.reduce and docs#free_group.to_word), and there are proofs that it gives the reduction using the previous setup.

Kyle Miller (Feb 18 2022 at 08:41):

It's possible that part of it is that free_group is from 2018, and mathlib has gotten more classical over time. (I found the thread where it was developed. It's rather long.) Though, mathlib still tends to try to keep definitions computable where practical.

Joachim Breitner (Feb 18 2022 at 08:44):

The definition via normalization would still be computable (at least if the elements have decidable equality), wouldn't it?

Kyle Miller (Feb 18 2022 at 08:45):

Yeah, docs#free_group.reduce is computable given decidable equality

David Wärn (Feb 18 2022 at 09:33):

We do have free products of groups, docs#free_product. There's also a discussion about the definition in the doc-string.

Joachim Breitner (Feb 18 2022 at 10:32):

Oh, why did I think we didn’t. Must have been confused.
What about the ping-pong-lemma? Seems all necessary prerequisites are there then?

Joachim Breitner (Feb 18 2022 at 10:35):

And would it be a useful lemma to show that free product of free groups is a free group?

David Wärn (Feb 18 2022 at 11:13):

I don't know about the ping-pong lemma, but "free product of free groups is a free group" is immediate from universal properties right? In general there's also a lot of API missing about free products, e.g. we don't have binary products yet

Joachim Breitner (Feb 18 2022 at 12:58):

Yes, it should follow quickly from universal properties.
Is adding such not-super-hard lemmas useful, even they are not actually needed for something more serious, and not part of a systematic API development?

Kevin Buzzard (Feb 18 2022 at 14:39):

Definitely, I would say! Someone may well need them later on for something.

Joachim Breitner (Feb 18 2022 at 15:14):

(hmm, wait)

Joachim Breitner (Feb 18 2022 at 15:18):

Huh, turning something from a lemma to a def can make its proof fail. That’s unexpected.

Joachim Breitner (Feb 18 2022 at 15:21):

So, this works:

/-- The free product of free groups is itself a free group -/
lemma is_free_group_free_product_of_is_free_group {ι : Type*} (G : ι  Type*)
  [ i, group (G i)] [hG :  i, is_free_group (G i)] : is_free_group (free_product G) :=
{ generators := Σ i, is_free_group.generators (G i),
  of := λ i, x⟩, free_product.of (is_free_group.of x),
  unique_lift' :=
  begin
    introsI X _ f,
    refine free_product.lift (λ i, is_free_group.lift (λ x, f i, x⟩)), _ ⟩,
    split,
    { simp, },
    { intros g hfg, ext i x, simpa using hfg i, x⟩, }
  end, }

But surely this needs to be a def. But then the simp doesn't work, and I need to do something like

/-- The free product of free groups is itself a free group -/
@[simps]
def is_free_group_free_product_of_is_free_group {ι : Type*} (G : ι  Type*)
  [ i, group (G i)] [hG :  i, is_free_group (G i)] : is_free_group (free_product G) :=
{ generators := Σ i, is_free_group.generators (G i),
  of := λ i, x⟩, free_product.of (is_free_group.of x),
  unique_lift' :=
  begin
    introsI X _ f,
    refine free_product.lift (λ i, is_free_group.lift (λ x, f i, x⟩)), _ ⟩,
    split,
    { rintros i, x⟩,
      unfold is_free_group_free_product_of_is_free_group._match_1,
      simp, },
    { intros g hfg, ext i x, simpa using hfg i, x⟩, }
  end, }

to make it unfold my definition of generators. Am I doing something wrong?

Eric Rodriguez (Feb 18 2022 at 15:26):

a lemma's type gets inferred at the :=, whilst a def's type can change depending on what's written afterwards. I suspect this is what's happening, with different instances

Reid Barton (Feb 18 2022 at 15:47):

You can try putting by exact before the body of the definition but it's a bit black magic

Reid Barton (Feb 18 2022 at 15:49):

of := λ ⟨i, x⟩, free_product.of (is_free_group.of x)

Unfortunately, this is usually not a good idea

Reid Barton (Feb 18 2022 at 15:49):

of := λ p, free_product.of (is_free_group.of p.2)

Reid Barton (Feb 18 2022 at 15:52):

Specifically it's not a good idea when constructing data--it's okay in proofs

Joachim Breitner (Feb 18 2022 at 15:55):

Ah, that was is, thanks. Too bad – destructing pattern matches are so useful :-)

Reid Barton (Feb 18 2022 at 15:57):

I think this might not be an issue in Lean 4.

Zhengying (Mar 17 2022 at 08:50):

Did anybody try this GPT-f repo?
https://github.com/jesse-michael-han/lean-gptf
I'm wondering if the OpenAI API key required can be the same one when one uses GPT-3 etc?

Mario Carneiro (Mar 17 2022 at 08:51):

I believe GPT-f is down, see https://leanprover.zulipchat.com/#narrow/stream/274007-lean-gptf/topic/Lean.20GPT-f.20beta/near/273140603


Last updated: Dec 20 2023 at 11:08 UTC