free groups

Stream: maths

[Joachim Breitner]

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]

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]

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]

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

[Kyle Miller]

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

[David Wärn]

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

[Joachim Breitner]

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]

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

[David Wärn]

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]

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]

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

[Joachim Breitner]

(hmm, wait)

[Joachim Breitner]

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

[Joachim Breitner]

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]

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]

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

[Reid Barton]

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

Unfortunately, this is usually not a good idea

[Reid Barton]

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

[Reid Barton]

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

[Joachim Breitner]

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

[Reid Barton]

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

[Zhengying]

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]

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