Theorems · Theorem · group theory

IsFreeGroup.ofLift

∀ {G : Type u} [inst : Group G] (X : Type u) (of : X → G)
  (lift : {H : Type u} → [inst_1 : Group H] → (X → H) ≃ (G →* H)),
  (∀ {H : Type u} [inst_1 : Group H] (f : X → H) (a : X), (lift f) (of a) = f a) → IsFreeGroup G

If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here, the universal property is expressed as in IsFreeGroup.lift and its properties.

Defined in

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group