ofUniqueLift — Mathlib

English

If f satisfies the lifting property with respect to a type X, then G is free.

Русский

Если f удовлетворяет свойству подъёма по отношению к типу X, то G свободна.

LaTeX

$$IsFreeGroup(G)$$

Lean4

/-- 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.unique_lift`. -/
theorem ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G)
    (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a) : IsFreeGroup G :=
  (FreeGroupBasis.ofUniqueLift X of h).isFreeGroup

Похожие утверждения