English
If a group G satisfies the universal property of a free group with respect to a type X via lift, then there exists a free group basis based on X.
Русский
Если группа G удовлетворяет универсальному свойству свободной группы по отношению к типу X через подъём, то существует базис свободной группы на X.
LaTeX
$$FreeGroupBasis(X,G) exists$$
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.lift` and its properties. -/
def 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) : FreeGroupBasis X G where
repr :=
MulEquiv.symm <|
MonoidHom.toMulEquiv (FreeGroup.lift of) (lift FreeGroup.of)
(by
apply FreeGroup.ext_hom; intro x
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift_apply_of, lift_of])
(by
let lift_symm_of : ∀ {H : Type u} [Group H], ∀ (f : G →* H) (a), lift.symm f a = f (of a) := by intro H _ f a;
simp [← lift_of (lift.symm f)]
apply lift.symm.injective; ext x
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift_apply_of, lift_of,
lift_symm_of])
