Theorems · Theorem · group theory

IsFreeGroupoid.ext_functor_iff

∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G] {X : Type v} [inst_2 : Group X]
  {f g : CategoryTheory.Functor G (CategoryTheory.SingleObj X)},
  f = g ↔ ∀ (a b : IsFreeGroupoid.Generators G) (e : a ⟶ b), f.map (IsFreeGroupoid.of e) = g.map (IsFreeGroupoid.of e)

Defined in

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

CategoryTheory.GroupoidIsFreeGroupoidGroup