Theorems · Definition · group theory

IsFreeGroupoid.SpanningTree.homOfPath

{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} →
            Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a →
              (IsFreeGroupoid.SpanningTree.root'✝ T ⟶ a)

A path in the tree gives a hom, by composition.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

4 results in Mathlib

Foundations

Depth 12 from the axioms · uses Classical.choice

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence