unique_lift — Mathlib

English

The universal property provides existence and uniqueness of lift for any function from generators to H.

Русский

Универсальное свойство обеспечивает существование и уникальность подъёма для любой функции от генераторов в H.

LaTeX

$$([Generators G] → H) has a unique lift to G →* H$$

Lean4

/-- The universal property of a free group: A function from the generators of `G` to another
group extends in a unique way to a homomorphism from `G`.

Note that since `IsFreeGroup.lift` is expressed as a bijection, it already
expresses the universal property. -/
theorem unique_lift (f : Generators G → H) : ∃! F : G →* H, ∀ a, F (of a) = f a := by
  simpa only [funext_iff] using lift.symm.bijective.existsUnique f

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