ofLift — Mathlib

English

If a group G satisfies universal lifting property, then it is free.

Русский

Если группа 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.lift` and its
properties. -/
theorem ofLift {G : Type u} [Group G] (X : Type u) (of : X → G) (lift : ∀ {H : Type u} [Group H], (X → H) ≃ (G →* H))
    (lift_of : ∀ {H : Type u} [Group H], ∀ (f : X → H) (a), lift f (of a) = f a) : IsFreeGroup G :=
  (FreeGroupBasis.ofLift X of lift lift_of).isFreeGroup

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