Theorems · Definition · group theory

IsFreeGroupoid.SpanningTree.loopOfHom

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

Any hom in G can be made into a loop, by conjugating with treeHoms.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

3 results in Mathlib

Foundations

Depth 15 from the axioms · uses Classical.choice

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence