lift_unique — Mathlib

English

If φ: Abelianization G →* A agrees with f on the image of G via Abelianization.of, then φ = lift f.

Русский

Если φ: Abelianization G →* A совпадает с f на образе G через Abelianization.of, то φ = lift f.

LaTeX

$$$$ \\forall \\phi : Abelianization(G) \\to_* A,\\; (\\forall x \\in G,\\; \\phi( Abelianization.of(x) ) = f(x)) \\Rightarrow \\phi = \\mathrm{lift}(f). $$$$

Lean4

theorem lift_unique
    (φ : Abelianization G →* A)
      -- hφ : φ agrees with f on the image of G in Gᵃᵇ

    (hφ : ∀ x : G, φ (Abelianization.of x) = f x) {x : Abelianization G} : φ x = lift f x :=
  QuotientGroup.induction_on x hφ

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