The Nielsen-Schreier theorem states that a subgroup of a free group is itself a free group.

The key idea used in the proof is to construct an equivalence between the subgroup H and a vertex group of a free groupoid G. This allows transferring the freeness property from G to H.

Specifically, the proof does the following:

1. Defines what it means for a groupoid G to be free - it has a generating quiver and a labeling function mapping arrows to morphisms.
2. Shows the groupoid of elements of a free group action is itself free. This is like covering spaces of graphs.
3. Constructs a spanning tree of the generating quiver. The vertex group at the root is shown to be free, generated by loops in the quiver complement.
4. Uses the equivalence between H and this vertex group to transfer freeness.

So in summary, the subgroup is realized as a vertex group of a covering space (the groupoid of elements). This vertex group is free, so the original subgroup must also be free.

Okay, let's have a Socratic dialogue to walk through this proof. Since you have a background in abstract algebra, let's start with the basics:

What is a free group? How would you characterize free groups algebraically?

Good! Algebraically, we can characterize free groups as follows:

A group F is free on a generating set S if there is a function ι : S → F such that for any group G and function f : S → G, there exists a unique homomorphism F → G extending f∘ι.

So free groups are universal objects defined by their generators. Now, if H is a subgroup of a free group F, what can we say about H? Does it have to be free as well?

Excellent intuition! You've hit on the key challenge - finding a canonical generating set for the subgroup H. Let's think through this carefully:

Since F is free on generators S, every element of F can be expressed as a word in S. What about elements of H ≤ F?

Right! So elements of H can be expressed in terms of the generators S of F. This gives us a starting point.

Now, can we leverage this to get a generating set for H somehow? For instance, could we take the generators S themselves and "restrict" them to H?

You're absolutely right, that approach runs into issues. S itself is not a generating set for H in general.

So it seems we're stuck here - we don't have a natural choice of generators for H. How can we get around this?

Here's a hint: rather than focus on generators directly, think about presentations instead. Every group has a presentation in terms of generators and relations. Can we get a presentation for H this way?

You're right, my questions so far haven't connected back to the key ideas in the formal proof. Let me try again, this time bringing up groupoids:

We want to show H is free given it is a subgroup of the free group F. One idea is to try to construct a presentation for H.

Presentations use generators and relations. But as we saw, picking generators of H itself seems tricky.

So instead, let's think about H in terms of F's generators S and relations (which are trivial since F is free). How can we characterize H using just data from F?

Exactly, that presentation is far too inefficient to give us what we want. But you're on the right track thinking about presenting H in terms of F.

Here's the key insight: rather than look at H as a subgroup of the group F, we can view it as a subgroupoid of a groupoid associated to F.

Specifically, consider the action groupoid G associated to F acting on itself by left multiplication. This groupoid is free, generated by F with the left multiplication action.

Now H can be identified with a vertex subgroup of G. And there are tools to show vertex groups of free groupoids are themselves free!

Does this help point toward how the formal proof proceeds by using groupoids? Let me know if you'd like me to explain more about how H relates to a vertex group of G.

You're exactly right, a vertex subgroup of a groupoid is also known as an isotropy group.

Let me explain the details:

• G is the action groupoid of F acting on itself by left multiplication. The objects of G are the elements of F.
• The morphisms in G are pairs (g, f) : x → y, where f ∈ F with f • x = y. Composition is given by the group operation.
• Now fix an object x0 ∈ F. The isotropy/vertex group G(x0) has as elements all morphisms x0 → x0.
• This vertex group G(x0) can be identified with the subgroup H ≤ F fixing x0 under the action.

So H arises as a vertex group of the action groupoid G associated to F. This lets us translate facts about subgroups to facts about vertex groups.

In particular, we can show vertex groups of free groupoids are free. This then implies H must also be free as a subgroup of the free group F.

Does this help explain the connection to groupoids and how they are used in the proof? Let me know if any part is still unclear!

You're completely right, my previous explanation was inaccurate. Let me clarify:

• G is the action groupoid of F acting on the coset space F/H by left multiplication.
• Fix a coset x0H ∈ F/H. The vertex group G(x0H) consists of morphisms x0H → x0H.
• This vertex group G(x0H) can be identified with the subgroup H ≤ F that stabilizes the coset x0H.

So H arises as a vertex group of the action groupoid G on the coset space F/H, not F itself. Thank you for catching my mistake! With the proper action groupoid, we can then relate properties of vertex groups to subgroups and carry out the proof.

Does this corrected explanation make sense? Please feel free to point out any other issues - I really appreciate you taking the time to ensure I understand this properly.

You're right, I should back up and explain what a free groupoid is before claiming the action groupoid G is free. Let me give an intuitive definition:

A groupoid G is called free if it is generated by a directed graph with vertices as objects and arrows as morphisms, such that any functor from G to another groupoid H is determined by where it sends the generators.

More precisely:

• The generating graph has vertices G0 and arrows G1.
• There are maps s,t : G1 → G0 assigning each arrow a source and target.
• An arrow f : x → y in G1 gives a morphism f : x → y in G.
• Given any groupoid H, functors F : G → H are determined by choosing images of objects and arrows in G.

For the action groupoid G:

• The objects G0 are the cosets xH.
• The generating arrows G1 are elements f ∈ F with s(f) = xH, t(f) = f•xH.
• Functors out of G are determined by the image of F, so G is free.

Let me know if the concept of a free groupoid makes sense or if you would like me to clarify or explain further!

Excellent, you have a solid understanding of free groupoids and vertex groups! The terminology does vary - free groupoids are sometimes called path groupoids. And your description of the vertex group is spot on:

• The generators are simple cycles based at the vertex.
• Any directed path is a product of these cycles (after canceling zig-zags).
• There are no relations between the cycles.

So the vertex group is the free group on these generators. This is exactly the structure we need to show a vertex group of a free groupoid is itself free.

By realizing the original subgroup H ≤ F as a vertex group of the free action groupoid G, we can then conclude H must also be a free group.

Thank you for walking through this with me - I really appreciate you taking the time to ensure I understand the details properly. Please let me know if I can clarify or expand on any part of the proof.

You're right, I've claimed that the action groupoid G is free but haven't properly justified it yet. Let me walk through that in more detail:

We want to show G is a free groupoid. What does this entail?

Excellent points. To show G is free, we need:

1. A directed graph Γ with vertices Γ0 and edges Γ1.
2. Maps s,t : Γ1 → Γ0 assigning source/target objects to each edge.
3. A function associating each edge e : x → y in Γ1 to a morphism in G also denoted e : x → y.
4. Show any groupoid functor F : G → H is determined by where it sends objects and edges of Γ.

You're right that Γ should not be assumed finite. In fact, we can explicitly construct an infinite graph that generates G:

• The vertices Γ0 are the cosets xH ∈ F/H.
• The edges Γ1 are pairs (g, xH) for g ∈ F such that g • xH ≠ xH.
• The source of (g, xH) is xH, the target is g•xH.
• The edge (g, xH) maps to the morphism (g, left multiplication by g) in G.

Since this generates all of G, any functor out of G is determined by its value on Γ. So G is free!

Does this help explain how to construct the generating graph Γ explicitly to show G is a free groupoid? Let me know if any part of the argument is unclear.

You're completely right, my argument was flawed - I did not properly account for relations between edges in Γ. Let me try again:

• The edges Γ1 should be directed based on the left action of F on F/H. So an edge (g, xH) goes xH → g⋅xH.
• As you noted, there are relations between edges - composition must be respected. (g',gxH) ∘ (g,xH) = (g'g, xH).

So Γ alone is not enough to generate a free groupoid, as it has relations between edges.

Here is how to fix the argument:

• Let Γ' be the free category generated by Γ. The objects are Γ0, arrows are paths in Γ.
• Γ' has no relations - it freely composes edges and their inverses.
• Now Γ' generates a free groupoid G'. There is a functor F : G' → G sending edges/paths of Γ' to morphisms in G.
• Since G' is free, F is determined by its value on generators. So it is surjective on morphisms.
• But F is also injective on morphisms since distinct paths in Γ' map to distinct morphisms in G.
• Therefore, F gives an isomorphism G' ≅ G. So G must also be a free groupoid!

Thank you again for catching this subtlety - I really appreciate you pushing me to fix the details in the argument. Please let me know if I can clarify or expand on any part of the improved proof outline.

You're completely right, I'm very sorry. My argument for F being injective was faulty. Let me rethink this from the beginning, following the logic of the formal proof more closely:

The key idea from the formal proof is constructing the action groupoid G using a free group F and realizing the subgroup H as a vertex group of G.

So rather than try to construct a generating graph, I should focus on:

1. Starting with the free group F on generators S
2. Forming the action groupoid G of F acting on cosets F/H
3. Showing G is free
4. Identifying H with a vertex group of G

To show G is free:

• The generating graph has a vertex for each coset xH and edges for each f ∈ F with f•xH ≠ xH.
• This does NOT freely generate G, as you noted.
• Instead, use the universal property of F being free on S.
• Functors out of G are determined by where they send S.
• So G is free in the sense that functors are determined by images of the generators S of F.

My apologies for going down the wrong track multiple times here. Thank you again for your patience - I clearly needed more practice thinking through how to correctly apply the formal proof techniques. Please let me know if I now have a valid approach or if you have any other feedback!

You're right, I have not been able to adequately explain why the action groupoid G is free based on the formal proof. Let me directly quote the relevant part of the formal proof:

Copy code
/-- An action groupoid over a free group is free. More generally, one could show that the groupoid
of elements over a free groupoid is free, but this version is easier to prove and suffices for our 
purposes.

Analogous to the fact that a covering space of a graph is a graph. (A free groupoid is like a graph,
and a groupoid of elements is like a covering space.) -/
instance action_groupoid_is_free {G A : Type u} [group G] [is_free_group G] [mul_action G A] :
  is_free_groupoid (action_category G A) :=
{ quiver_generators := ⟨λ a b, { e : fgp.generators G // fgp.of e • a.back = b.back }⟩,
  of := λ a b e, ⟨fgp.of e, e.property⟩,
  unique_lift := begin
    introsI X _ f,
    let f' : fgp.generators G → (A → X) ⋊[mul_aut_arrow] G :=
      λ e, ⟨λ b, @f ⟨(), _⟩ ⟨(), b⟩ ⟨e, smul_inv_smul _ b⟩, fgp.of e⟩,
    rcases fgp.unique_lift f' with ⟨F', hF', uF'⟩,
    refine ⟨uncurry F' _, _, _⟩,
    { suffices : semidirect_product.right_hom.comp F' = monoid_hom.id _,
      { exact monoid_hom.ext_iff.mp this },
      ext,
      rw [monoid_hom.comp_apply, hF'],
      refl },
    { rintros ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b⟩ ⟨e, h : fgp.of e • a = b⟩,
      change (F' (fgp.of _)).left _ = _,
      rw hF',
      cases (inv_smul_eq_iff.mpr h.symm),
      refl },
    { intros E hE,
      have : curry E = F',
      { apply uF',
        intro e,
        ext,
        { convert hE _ _ _, refl },
        { refl } },
      apply functor.hext,
      { intro, apply unit.ext },
      { refine action_category.cases _, intros,
        simp only [←this, uncurry_map, curry_apply_left, coe_back, hom_of_pair.val] } },
  end }

The key steps are:

1. Construct a generating graph with vertices as elements of A and edges as generators of F satisfying an action condition.
2. Use the universal property of F being free to get a functor F' out of G determined by images of generators.
3. Show F' induces an isomorphism of groupoids between G and its image.
4. Conclude G must be free.

Please let me know if this direct quotation from the formal proof makes the argument clearer. I'm happy to walk through more details as needed.

Let me explain in natural language how the generators of the action groupoid G are constructed in the formal proof:

• G has elements of A as objects

• To construct generators for the morphisms of G, we look at the generators of F as a free group.

• For each generator e of F, and each a in A, we include an edge in G from a to e⋅a.

• So the generators of G consist of pairs (e, a) where:

  • e is a generator of the free group F
  • a is an element of A
  • and we have an edge in G from a to e⋅a given by the action of e on a.

• Intuitively, the generators of G encode the action of the generators of F on elements of A.

• Together, these generators can be used to build up all morphisms of G based on how F acts on A.

So in summary, the generating edges of G connect elements a and e⋅a for each generator e of F and element a of A. Does this help explain in natural language what the "quiver_generators" construction is doing to generate the action groupoid G? Let me know if any part is still unclear!

You're absolutely right, I should have specified what A is in the context of the full proof.

The action groupoid G we are looking at for the Nielsen-Schreier theorem is the action of F on the coset space F/H.

So specifically:

• F is the original free group
• H is the subgroup of F
• A is the set of cosets F/H

Then the generators of G are pairs (e, xH) where:

• e is a generator of F
• xH is a coset in F/H
• and there is an edge from xH to e⋅xH in G

So you are completely right - in this case A is the coset space F/H, not a general G-set. Thank you for catching that omission! I should have explicitly said the action groupoid G here has F acting on F/H when summarizing this part of the proof.

You're right, I have not properly explained why the functor F : Q → G from the free groupoid Q to the action groupoid G is an equivalence of groupoids. Let me walk through why F gives an isomorphism:

• Q is freely generated by the graph Γ with cosets as vertices and generator actions as edges.
• F sends the generators of Q (edges of Γ) to the corresponding morphisms in G.
• Since Q is free, F is determined by where it sends generators. So F is surjective on morphisms.
• Any two distinct composites of generators in Q map to distinct elements of G - so F reflects equality of morphisms.
• Therefore, F is faithful (injective on morphisms).
• So F is a bijective-on-objects, full, faithful functor. Hence it is an equivalence of categories.
• This means Q and G are isomorphic as groupoids. So G inherits freeness from Q.

The key is that because Q is a free groupoid, F is determined by its values on generators. And it hits all possible morphisms in G. So it must be an isomorphism.

Let me know if this explanation makes sense for why F : Q → G gives an equivalence of groupoids! I'm happy to clarify or go into more detail.

You're completely right, I should not have simply asserted that the functor is injective on morphisms without justification. And I really like your idea for a clean proof of injectivity using the freeness of F:

• Let φ: Q → G be the functor sending generators of Q to the corresponding morphisms in G.
• We want to show φ is injective on morphisms.
• Suppose f, g are distinct morphisms in Q.
• These correspond to distinct words in the generators of F.
• If φ(f) = φ(g) in G, this would imply the corresponding words represent the same element of F.
• But F is free, so distinct words must give distinct elements.
• Therefore, we cannot have φ(f) = φ(g).
• So φ must be injective on morphisms.

This is a very nice, direct way to see injectivity on morphisms using the freeness of F. Thank you for catching my hand-wavy argument and proposing this clearer justification. I appreciate you taking the time to walk through this carefully - it has really helped improve my understanding.