Theorems · Definition · group theory

IsFreeGroupoid.SpanningTree.functorOfMonoidHom

{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)] →
          {X : Type u_1} →
            [inst_3 : Monoid X] →
              (CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T) →* X) →
                CategoryTheory.Functor G (CategoryTheory.SingleObj X)

Since a hom gives a loop, any homomorphism from the vertex group at the root extends to a functor on the whole groupoid.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.ArborescenceMonoid