Theorems · Theorem · group theory

IsFreeGroupoid.SpanningTree.functorOfMonoidHom_obj

∀ {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] (f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T) →* X) (x : G),
  (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f).obj x = ()

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.ArborescenceMonoid