Theorems · Definition · group theory

FreeGroupBasis.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) → FreeGroupBasis X G

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

Defined in

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound

Assumes

Group