Vertex groups of free groupoids are free

The last step of Lemma 4.2 (lem:mesh-walk-free, scalar-normalization.tex): "Contracting spanning trees gives a graph. Its edges outside a spanning tree freely generate the fundamental group." Mathlib proves this for a connected free groupoid (IsFreeGroupoid.endIsFreeOfConnectedFree, by a spanning tree). Here the free groupoid on any quiver is shown to be free in Mathlib's sense, and the vertex group at X₀ is identified with the vertex group of the free groupoid on the connected component of X₀.

@[instance_reducible]

instance MultiplicativeBasisDeformations.FreeVertex.isFreeGroupoid (W : Type u) [Quiver W] : IsFreeGroupoid (Quiver.FreeGroupoid W)

The free groupoid on a quiver is a free groupoid.

def MultiplicativeBasisDeformations.FreeVertex.Reach {U : Type u} [Quiver U] (X Y : U) : Prop

Reachability by zigzags of arrows.

def MultiplicativeBasisDeformations.FreeVertex.Comp {U : Type u} [Quiver U] (X₀ : U) : Type u

The connected component of X₀, as a full subquiver.

@[instance_reducible]

instance MultiplicativeBasisDeformations.FreeVertex.instQuiverComp {U : Type u} [Quiver U] (X₀ : U) : Quiver (Comp X₀)

def MultiplicativeBasisDeformations.FreeVertex.base {U : Type u} [Quiver U] (X₀ : U) : Comp X₀

The base point of the component.

theorem MultiplicativeBasisDeformations.FreeVertex.reach_of_hom {U : Type u} [Quiver U] (X₀ : U) {Y Z : U} (hY : Reach X₀ Y) : ∀ (x : Y ⟶ Z), Reach X₀ Z

theorem MultiplicativeBasisDeformations.FreeVertex.reach_of_hom' {U : Type u} [Quiver U] (X₀ : U) {Y Z : U} (hZ : Reach X₀ Z) : ∀ (x : Y ⟶ Z), Reach X₀ Y

def MultiplicativeBasisDeformations.FreeVertex.incl {U : Type u} [Quiver U] (X₀ : U) : Comp X₀ ⥤q U

The inclusion of the component.

def MultiplicativeBasisDeformations.FreeVertex.ι {U : Type u} [Quiver U] (X₀ : U) : CategoryTheory.Functor (Quiver.FreeGroupoid (Comp X₀)) (Quiver.FreeGroupoid U)

The induced functor of free groupoids.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FreeVertex.obC {U : Type u} [Quiver U] (X₀ : U) (Y : Comp X₀) : Quiver.FreeGroupoid (Comp X₀)

theorem MultiplicativeBasisDeformations.FreeVertex.ι_of {U : Type u} [Quiver U] (X₀ : U) {Y Z : Comp X₀} (e : Y ⟶ Z) : (ι X₀).map ((Quiver.FreeGroupoid.of (Comp X₀)).map e) = (Quiver.FreeGroupoid.of U).map (have this := e; this)

theorem MultiplicativeBasisDeformations.FreeVertex.nonempty_hom {U : Type u} [Quiver U] (X₀ Y Z : U) (h : Relation.EqvGen (fun (a b : U) => Nonempty (a ⟶ b)) Y Z) (hY : Reach X₀ Y) : Nonempty (obC X₀ ⟨Y, hY⟩ ⟶ obC X₀ ⟨Z, ⋯⟩)

The component is connected.

instance MultiplicativeBasisDeformations.FreeVertex.isConnected {U : Type u} [Quiver U] (X₀ : U) : CategoryTheory.IsConnected (Quiver.FreeGroupoid (Comp X₀))

Injectivity: conjugating back to the base point

noncomputable def MultiplicativeBasisDeformations.FreeVertex.γ {U : Type u} [Quiver U] (X₀ : U) (Y : Comp X₀) : obC X₀ (base X₀) ⟶ obC X₀ Y

Chosen morphisms from the base point.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FreeVertex.E {U : Type u} [Quiver U] (X₀ : U) : Type u

The vertex group at the base point.

def MultiplicativeBasisDeformations.FreeVertex.pt {U : Type u} [Quiver U] (X₀ : U) (Y : Quiver.FreeGroupoid (Comp X₀)) : Comp X₀

The underlying vertex of an object.

noncomputable def MultiplicativeBasisDeformations.FreeVertex.γ' {U : Type u} [Quiver U] (X₀ : U) (Y : Quiver.FreeGroupoid (Comp X₀)) : obC X₀ (base X₀) ⟶ Y

γ on objects of the free groupoid.

noncomputable def MultiplicativeBasisDeformations.FreeVertex.conj {U : Type u} [Quiver U] (X₀ : U) : CategoryTheory.Functor (Quiver.FreeGroupoid (Comp X₀)) (CategoryTheory.SingleObj (E X₀))

Conjugation to the base point, as a functor to the vertex group.

def MultiplicativeBasisDeformations.FreeVertex.mk {U : Type u} [Quiver U] (X₀ Y : U) (h : Reach X₀ Y) : Comp X₀

A vertex of the component.

noncomputable def MultiplicativeBasisDeformations.FreeVertex.lab {U : Type u} [Quiver U] (X₀ : U) : U ⥤q CategoryTheory.SingleObj (E X₀)

The labelling of the arrows of U by conjugated loops.

noncomputable def MultiplicativeBasisDeformations.FreeVertex.F {U : Type u} [Quiver U] (X₀ : U) : CategoryTheory.Functor (Quiver.FreeGroupoid U) (CategoryTheory.SingleObj (E X₀))

The functor F of the labelling.

theorem MultiplicativeBasisDeformations.FreeVertex.ι_F {U : Type u} [Quiver U] (X₀ : U) : (ι X₀).comp (F X₀) = conj X₀

theorem MultiplicativeBasisDeformations.FreeVertex.ι_injective {U : Type u} [Quiver U] (X₀ : U) {f g : obC X₀ (base X₀) ⟶ obC X₀ (base X₀)} (h : (ι X₀).map f = (ι X₀).map g) : f = g

Surjectivity: walks from the component stay in it

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FreeVertex.cls {U : Type u} [Quiver U] {Y Z : U} (p : Quiver.Path (have this := Y; this) Z) : (Quiver.FreeGroupoid.of U).obj Y ⟶ (Quiver.FreeGroupoid.of U).obj Z

The class of a walk in the free groupoid.

theorem MultiplicativeBasisDeformations.FreeVertex.surj_aux {U : Type u} [Quiver U] (X₀ : U) {Y : U} (hY : Reach X₀ Y) {Z : U} (p : Quiver.Path (have this := Y; this) Z) : ∃ (hZ : Reach X₀ Z) (g : obC X₀ (mk X₀ Y hY) ⟶ obC X₀ (mk X₀ Z hZ)), (ι X₀).map g = cls p

theorem MultiplicativeBasisDeformations.FreeVertex.ι_surjective {U : Type u} [Quiver U] (X₀ : U) (g : (Quiver.FreeGroupoid.of U).obj X₀ ⟶ (Quiver.FreeGroupoid.of U).obj X₀) : ∃ (f : obC X₀ (base X₀) ⟶ obC X₀ (base X₀)), (ι X₀).map f = g

theorem MultiplicativeBasisDeformations.FreeVertex.isFreeGroup_end {U : Type u} [Quiver U] (X₀ : U) : IsFreeGroup (CategoryTheory.End ((Quiver.FreeGroupoid.of U).obj X₀))

Vertex groups of free groupoids are free (the spanning-tree step of Lemma 4.2).