Theorems · Definition · group theory

Abelianization.lift

{G : Type u} → [inst : Group G] → {A : Type v} → [inst_1 : CommGroup A] → (G →* A) ≃ (Abelianization G →* A)

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.

Defined in

Mathlib.GroupTheory.Abelianization.Defs

Cited by

9 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupCommGroup