Theorems · Theorem · group theory

IsFreeGroupoid.SpanningTree.homOfPath.eq_def

∀ {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 : G)
  (x_1 : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) x),
  IsFreeGroupoid.SpanningTree.homOfPath T x_1 =
    match x, x_1 with
    | .(Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)), Quiver.Path.nil =>
      CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)
    | x, p.cons f =>
      CategoryTheory.CategoryStruct.comp (IsFreeGroupoid.SpanningTree.homOfPath T p)
        (Sum.recOn (↑f) (fun e => IsFreeGroupoid.of e) fun e => CategoryTheory.inv (IsFreeGroupoid.of e))

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses Classical.choice

Assumes

CategoryTheory.GroupoidIsFreeGroupoidQuiver.Arborescence