Theorems · Theorem · group theory

IsFreeGroupoid.SpanningTree.endIsFree

∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)],
  IsFreeGroup (CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T))

Given a free groupoid and an arborescence of its generating quiver, the vertex group at the root is freely generated by loops coming from generating arrows in the complement of the tree.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

0 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence