Theorems · Theorem · group theory

IsFreeGroupoid.SpanningTree.loopOfHom_eq_id

∀ {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 : IsFreeGroupoid.Generators G},
  ∀ e ∈ Quiver.wideSubquiverSymmetrify T a b,
    IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e) =
      CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)

Turning an edge in the spanning tree into a loop gives the identity loop.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence