English
The functorial construction lift establishes an equivalence between group homomorphisms G → A (A abelian) and Abelianization G → A.
Русский
Конструкция lift устанавливает эквивалентность между гомоморфизмами групп G → A (A абелева) и Abelianization G → A.
LaTeX
$$$$ \\text{lift} : (G \\to_* A) \\simeq (\\mathrm{Abelianization}(G) \\to_* A). $$$$
Lean4
/-- If `f : G → A` is a group homomorphism to an abelian group, then `lift f` is the unique map
from the abelianization of a `G` to `A` that factors through `f`. -/
def lift : (G →* A) ≃ (Abelianization G →* A)
where
toFun f := QuotientGroup.lift _ f fun _ h => MonoidHom.mem_ker.2 <| commutator_subset_ker _ h
invFun F := F.comp of
right_inv _ := MonoidHom.ext fun x => QuotientGroup.induction_on x fun _ => rfl
