Theorems · Definition · group theory

IsFreeGroupoid.SpanningTree.treeHom

{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)] →
          (a : G) → IsFreeGroupoid.SpanningTree.root'✝ T ⟶ a

For every vertex a, there is a canonical hom from the root, given by the path in the tree.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

4 results in Mathlib

Foundations

Depth 13 from the axioms · uses Classical.choice

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence