Theorems · Theorem · group theory

IsFreeGroupoid.SpanningTree.treeHom_eq

∀ {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}
  (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a),
  IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T p

Any path to a gives treeHom T a, since paths in the tree are unique.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses Classical.choice

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence