Theorems · Theorem · group theory

IsFreeGroupoid.path_nonempty_of_hom

∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G] {a b : G},
  Nonempty (a ⟶ b) → Nonempty (Quiver.Path (IsFreeGroupoid.symgen✝ a) (IsFreeGroupoid.symgen✝ b))

If there exists a morphism a → b in a free groupoid, then there also exists a zigzag from a to b in the generating quiver.

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.GroupoidIsFreeGroupoid