English
If a group G admits a universal lifting property for X, then there is a FreeGroupBasis X G.
Русский
Если группа G допускает универсальное свойство подъёма для X, то существует FreeGroupBasis X G.
LaTeX
$$∃ B : FreeGroupBasis X G$$
Lean4
/-- 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.unique_lift`. -/
def 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) : FreeGroupBasis X G :=
let lift {H : Type u} [Group H] : (X → H) ≃ (G →* H) :=
{ toFun := fun f => Classical.choose (h f)
invFun := fun F => F ∘ of
left_inv := fun f => funext (Classical.choose_spec (h f)).left
right_inv := fun F => ((Classical.choose_spec (h (F ∘ of))).right F fun _ => rfl).symm }
let lift_of {H : Type u} [Group H] (f : X → H) (a : X) : lift f (of a) = f a := congr_fun (lift.symm_apply_apply f) a
ofLift X of @lift @lift_of
