Documentation

Mathlib.GroupTheory.Abelianization.Defs

The abelianization of a group #

This file defines the commutator and the abelianization of a group. It furthermore prepares for the result that the abelianization is left adjoint to the forgetful functor from abelian groups to groups, which can be found in Mathlib/Algebra/Category/Grp/Adjunctions.lean.

Main definitions #

Group.Abelianization: defines the abelianization of a group G as the quotient of a group by its commutator subgroup.
Group.Abelianization.map: lifts a group homomorphism to a homomorphism between the abelianizations.
MulEquiv.abelianizationCongr: Isomorphic groups have isomorphic abelianizations.

def Group.Abelianization (G : Type u) [Group G] :

The abelianization of the group G is the quotient of G by its commutator subgroup.

Equations

Group.Abelianization G = (G ⧸ commutator G)

Instances For

def AddGroup.Abelianization (G : Type u) [AddGroup G] :

The abelianization of the additive group G is the quotient of G by its commutator subgroup.

Equations

AddGroup.Abelianization G = (G ⧸ addCommutator G)

Instances For

@[instance_reducible]

instance Group.instCommGroupAbelianization (G : Type u) [Group G] :

CommGroup (Abelianization G)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance AddGroup.instAddCommGroupAbelianization (G : Type u) [AddGroup G] :

AddCommGroup (Abelianization G)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Group.Abelianization.instInhabited (G : Type u) [Group G] :

Inhabited (Abelianization G)

Equations

Group.Abelianization.instInhabited G = { default := 1 }

@[instance_reducible]

instance AddGroup.Abelianization.instInhabited (G : Type u) [AddGroup G] :

Inhabited (Abelianization G)

Equations

AddGroup.Abelianization.instInhabited G = { default := 0 }

def Group.Abelianization.of {G : Type u} [Group G] :

G →* Abelianization G

of is the canonical projection from the group G to its abelianization.

Equations

Group.Abelianization.of = { toFun := QuotientGroup.mk, map_one' := ⋯, map_mul' := ⋯ }

Instances For

def AddGroup.Abelianization.of {G : Type u} [AddGroup G] :

G →+ Abelianization G

of is the canonical projection from the additive group G to its abelianization.

Equations

AddGroup.Abelianization.of = { toFun := QuotientAddGroup.mk, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem Group.Abelianization.mk_eq_of {G : Type u} [Group G] (a : G) :

Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a = of a

@[simp]

theorem AddGroup.Abelianization.mk_eq_of {G : Type u} [AddGroup G] (a : G) :

Quot.mk (⇑(QuotientAddGroup.leftRel (addCommutator G))) a = of a

@[simp]

theorem Group.Abelianization.ker_of (G : Type u) [Group G] :

of.ker = commutator G

@[simp]

theorem AddGroup.Abelianization.ker_of (G : Type u) [AddGroup G] :

of.ker = addCommutator G

theorem Group.Abelianization.commutator_le_ker {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : G →* A) :

commutator G ≤ f.ker

theorem AddGroup.Abelianization.addCommutator_le_ker {G : Type u} [AddGroup G] {A : Type v} [AddGroup A] [IsAddCommutative A] (f : G →+ A) :

addCommutator G ≤ f.ker

def Group.Abelianization.lift {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative 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 G to A that factors through f.

Equations

One or more equations did not get rendered due to their size.

Instances For

def AddGroup.Abelianization.lift {G : Type u} [AddGroup G] {A : Type v} [AddGroup A] [IsAddCommutative A] :

(G →+ A) ≃ (Abelianization G →+ A)

If f : G → A is an additive group homomorphism to an abelian group, then lift f is the unique map from the abelianization of G to A that factors through f.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Group.Abelianization.lift_apply_of {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : G →* A) (x : G) :

(lift f) (of x) = f x

@[simp]

theorem AddGroup.Abelianization.lift_apply_of {G : Type u} [AddGroup G] {A : Type v} [AddGroup A] [IsAddCommutative A] (f : G →+ A) (x : G) :

(lift f) (of x) = f x

theorem Group.Abelianization.coe_lift_symm {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] :

⇑lift.symm = fun (x : Abelianization G →* A) => x.comp of

theorem AddGroup.Abelianization.coe_lift_symm {G : Type u} [AddGroup G] {A : Type v} [AddGroup A] [IsAddCommutative A] :

⇑lift.symm = fun (x : Abelianization G →+ A) => x.comp of

@[simp]

theorem Group.Abelianization.lift_symm_apply {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : Abelianization G →* A) :

lift.symm f = f.comp of

@[simp]

theorem AddGroup.Abelianization.lift_symm_apply {G : Type u} [AddGroup G] {A : Type v} [AddGroup A] [IsAddCommutative A] (f : Abelianization G →+ A) :

lift.symm f = f.comp of

theorem Group.Abelianization.lift_unique {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : G →* A) (φ : Abelianization G →* A) (hφ : ∀ (x : G), φ (of x) = f x) {x : Abelianization G} :

φ x = (lift f) x

theorem AddGroup.Abelianization.lift_unique {G : Type u} [AddGroup G] {A : Type v} [AddGroup A] [IsAddCommutative A] (f : G →+ A) (φ : Abelianization G →+ A) (hφ : ∀ (x : G), φ (of x) = f x) {x : Abelianization G} :

φ x = (lift f) x

@[simp]

theorem Group.Abelianization.lift_of {G : Type u} [Group G] :

lift of = MonoidHom.id (Abelianization G)

@[simp]

theorem AddGroup.Abelianization.lift_of {G : Type u} [AddGroup G] :

lift of = AddMonoidHom.id (Abelianization G)

theorem Group.Abelianization.hom_ext {G : Type u} [Group G] {A : Type v} [Monoid A] (φ ψ : Abelianization G →* A) (h : φ.comp of = ψ.comp of) :

φ = ψ

theorem AddGroup.Abelianization.hom_ext {G : Type u} [AddGroup G] {A : Type v} [AddMonoid A] (φ ψ : Abelianization G →+ A) (h : φ.comp of = ψ.comp of) :

φ = ψ

theorem Group.Abelianization.hom_ext_iff {G : Type u} [Group G] {A : Type v} [Monoid A] {φ ψ : Abelianization G →* A} :

φ = ψ ↔ φ.comp of = ψ.comp of

theorem AddGroup.Abelianization.hom_ext_iff {G : Type u} [AddGroup G] {A : Type v} [AddMonoid A] {φ ψ : Abelianization G →+ A} :

φ = ψ ↔ φ.comp of = ψ.comp of

def Group.Abelianization.map {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) :

Abelianization G →* Abelianization H

The map operation of the Abelianization functor.

Equations

Group.Abelianization.map f = Group.Abelianization.lift (Group.Abelianization.of.comp f)

Instances For

def AddGroup.Abelianization.map {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (f : G →+ H) :

Abelianization G →+ Abelianization H

The map operation of the Abelianization functor.

Equations

AddGroup.Abelianization.map f = AddGroup.Abelianization.lift (AddGroup.Abelianization.of.comp f)

Instances For

@[simp]

theorem Group.Abelianization.lift_of_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) :

lift (of.comp f) = map f

Use map as the preferred simp normal form.

@[simp]

theorem AddGroup.Abelianization.lift_of_comp {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (f : G →+ H) :

lift (of.comp f) = map f

Use map as the preferred simp normal form.

@[simp]

theorem Group.Abelianization.map_of {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) (x : G) :

(map f) (of x) = of (f x)

@[simp]

theorem AddGroup.Abelianization.map_of {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (f : G →+ H) (x : G) :

(map f) (of x) = of (f x)

@[simp]

theorem Group.Abelianization.map_id {G : Type u} [Group G] :

map (MonoidHom.id G) = MonoidHom.id (Abelianization G)

@[simp]

theorem AddGroup.Abelianization.map_id {G : Type u} [AddGroup G] :

map (AddMonoidHom.id G) = AddMonoidHom.id (Abelianization G)

@[simp]

theorem Group.Abelianization.map_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] (g : H →* I) :

(map g).comp (map f) = map (g.comp f)

@[simp]

theorem AddGroup.Abelianization.map_comp {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (f : G →+ H) {I : Type w} [AddGroup I] (g : H →+ I) :

(map g).comp (map f) = map (g.comp f)

@[simp]

theorem Group.Abelianization.map_map_apply {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] {g : H →* I} {x : Abelianization G} :

(map g) ((map f) x) = (map (g.comp f)) x

@[simp]

theorem AddGroup.Abelianization.map_map_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (f : G →+ H) {I : Type w} [AddGroup I] {g : H →+ I} {x : Abelianization G} :

(map g) ((map f) x) = (map (g.comp f)) x

def MulEquiv.abelianizationCongr {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) :

Group.Abelianization G ≃* Group.Abelianization H

Isomorphic groups have isomorphic abelianizations.

Equations

e.abelianizationCongr = { toFun := ⇑(Group.Abelianization.map e.toMonoidHom), invFun := ⇑(Group.Abelianization.map e.symm.toMonoidHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

def AddEquiv.abelianizationCongr {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (e : G ≃+ H) :

AddGroup.Abelianization G ≃+ AddGroup.Abelianization H

Isomorphic additive groups have isomorphic abelianizations.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Group.abelianizationCongr_of {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) (x : G) :

e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)

@[simp]

theorem AddGroup.abelianizationCongr_of {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (e : G ≃+ H) (x : G) :

e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)

@[simp]

theorem Group.abelianizationCongr_refl {G : Type u} [Group G] :

(MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G)

@[simp]

theorem AddGroup.abelianizationCongr_refl {G : Type u} [AddGroup G] :

(AddEquiv.refl G).abelianizationCongr = AddEquiv.refl (Abelianization G)

@[simp]

theorem Group.abelianizationCongr_symm {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) :

e.abelianizationCongr.symm = e.symm.abelianizationCongr

@[simp]

theorem AddGroup.abelianizationCongr_symm {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (e : G ≃+ H) :

e.abelianizationCongr.symm = e.symm.abelianizationCongr

@[simp]

theorem Group.abelianizationCongr_trans {G : Type u} [Group G] {H : Type v} [Group H] {I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) :

e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr

@[simp]

theorem AddGroup.abelianizationCongr_trans {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] {I : Type v} [AddGroup I] (e : G ≃+ H) (e₂ : H ≃+ I) :

e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr

def Group.Abelianization.equivOfComm {H : Type u_1} [CommGroup H] :

H ≃* Abelianization H

An Abelian group is equivalent to its own abelianization.

Equations

Group.Abelianization.equivOfComm = { toFun := ⇑Group.Abelianization.of, invFun := ⇑(Group.Abelianization.lift (MonoidHom.id H)), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

def AddGroup.Abelianization.equivOfComm {H : Type u_1} [AddCommGroup H] :

H ≃+ Abelianization H

An additive Abelian group is equivalent to its own abelianization.

Equations

AddGroup.Abelianization.equivOfComm = { toFun := ⇑AddGroup.Abelianization.of, invFun := ⇑(AddGroup.Abelianization.lift (AddMonoidHom.id H)), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem Group.Abelianization.equivOfComm_apply {H : Type u_1} [CommGroup H] (a : H) :

equivOfComm a = of a

@[simp]

theorem AddGroup.Abelianization.equivOfComm_apply {H : Type u_1} [AddCommGroup H] (a : H) :

equivOfComm a = of a

@[simp]

theorem Group.Abelianization.equivOfComm_symm_apply {H : Type u_1} [CommGroup H] (a : Abelianization H) :

equivOfComm.symm a = (lift (MonoidHom.id H)) a

@[simp]

theorem AddGroup.Abelianization.equivOfComm_symm_apply {H : Type u_1} [AddCommGroup H] (a : Abelianization H) :

equivOfComm.symm a = (lift (AddMonoidHom.id H)) a

@[instance_reducible]

instance Group.instUniqueAbelianization (G : Type u) [Group G] [Unique G] :

Unique (Abelianization G)

Equations

Group.instUniqueAbelianization G = Quotient.instUniqueQuotient (QuotientGroup.leftRel (commutator G))

@[instance_reducible]

instance AddGroup.instUniqueAbelianization (G : Type u) [AddGroup G] [Unique G] :

Unique (Abelianization G)

Equations

AddGroup.instUniqueAbelianization G = Quotient.instUniqueQuotient (QuotientAddGroup.leftRel (addCommutator G))

@[deprecated Group.Abelianization (since := "2026-11-03")]

def Abelianization (G : Type u) [Group G] :

Alias of Group.Abelianization.

The abelianization of the group G is the quotient of G by its commutator subgroup.

Equations

Abelianization = Group.Abelianization

Instances For

@[deprecated Group.Abelianization.instInhabited (since := "2026-11-03")]

def Abelianization.instInhabited (G : Type u) [Group G] :

Inhabited (Group.Abelianization G)

Alias of Group.Abelianization.instInhabited.

Equations

Abelianization.instInhabited = Group.Abelianization.instInhabited

Instances For

@[deprecated Group.Abelianization.of (since := "2026-11-03")]

def Abelianization.of {G : Type u} [Group G] :

G →* Group.Abelianization G

Alias of Group.Abelianization.of.

of is the canonical projection from the group G to its abelianization.

Equations

@Abelianization.of = @Group.Abelianization.of

Instances For

@[deprecated Group.Abelianization.mk_eq_of (since := "2026-11-03")]

theorem Abelianization.mk_eq_of {G : Type u} [Group G] (a : G) :

Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a = Group.Abelianization.of a

Alias of Group.Abelianization.mk_eq_of.

@[deprecated Group.Abelianization.ker_of (since := "2026-11-03")]

theorem Abelianization.ker_of (G : Type u) [Group G] :

Group.Abelianization.of.ker = commutator G

Alias of Group.Abelianization.ker_of.

@[deprecated Group.Abelianization.commutator_le_ker (since := "2026-11-03")]

theorem Abelianization.commutator_le_ker {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : G →* A) :

commutator G ≤ f.ker

Alias of Group.Abelianization.commutator_le_ker.

@[deprecated AddGroup.Abelianization.addCommutator_le_ker (since := "2026-11-03")]

theorem Abelianization.addCommutator_le_ker {G : Type u} [AddGroup G] {A : Type v} [AddGroup A] [IsAddCommutative A] (f : G →+ A) :

addCommutator G ≤ f.ker

Alias of AddGroup.Abelianization.addCommutator_le_ker.

@[deprecated Group.Abelianization.commutator_le_ker (since := "2026-10-17")]

theorem Abelianization.commutator_subset_ker {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : G →* A) :

commutator G ≤ f.ker

Alias of Group.Abelianization.commutator_le_ker.

@[deprecated Group.Abelianization.lift (since := "2026-11-03")]

def Abelianization.lift {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] :

(G →* A) ≃ (Group.Abelianization G →* A)

Alias of Group.Abelianization.lift.

If f : G → A is a group homomorphism to an abelian group, then lift f is the unique map from the abelianization of G to A that factors through f.

Equations

@Abelianization.lift = @Group.Abelianization.lift

Instances For

@[deprecated Group.Abelianization.lift_apply_of (since := "2026-11-03")]

theorem Abelianization.lift_apply_of {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : G →* A) (x : G) :

(Group.Abelianization.lift f) (Group.Abelianization.of x) = f x

Alias of Group.Abelianization.lift_apply_of.

@[deprecated Group.Abelianization.coe_lift_symm (since := "2026-11-03")]

theorem Abelianization.coe_lift_symm {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] :

⇑Group.Abelianization.lift.symm = fun (x : Group.Abelianization G →* A) => x.comp Group.Abelianization.of

Alias of Group.Abelianization.coe_lift_symm.

@[deprecated Group.Abelianization.lift_symm_apply (since := "2026-11-03")]

theorem Abelianization.lift_symm_apply {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : Group.Abelianization G →* A) :

Group.Abelianization.lift.symm f = f.comp Group.Abelianization.of

Alias of Group.Abelianization.lift_symm_apply.

@[deprecated Group.Abelianization.lift_unique (since := "2026-11-03")]

theorem Abelianization.lift_unique {G : Type u} [Group G] {A : Type v} [Group A] [IsMulCommutative A] (f : G →* A) (φ : Group.Abelianization G →* A) (hφ : ∀ (x : G), φ (Group.Abelianization.of x) = f x) {x : Group.Abelianization G} :

φ x = (Group.Abelianization.lift f) x

Alias of Group.Abelianization.lift_unique.

@[deprecated Group.Abelianization.lift_of (since := "2026-11-03")]

theorem Abelianization.lift_of {G : Type u} [Group G] :

Group.Abelianization.lift Group.Abelianization.of = MonoidHom.id (Group.Abelianization G)

Alias of Group.Abelianization.lift_of.

@[deprecated Group.Abelianization.hom_ext (since := "2026-11-03")]

theorem Abelianization.hom_ext {G : Type u} [Group G] {A : Type v} [Monoid A] (φ ψ : Group.Abelianization G →* A) (h : φ.comp Group.Abelianization.of = ψ.comp Group.Abelianization.of) :

φ = ψ

Alias of Group.Abelianization.hom_ext.

@[deprecated Group.Abelianization.hom_ext_iff (since := "2026-11-03")]

theorem Abelianization.hom_ext_iff {G : Type u} [Group G] {A : Type v} [Monoid A] {φ ψ : Group.Abelianization G →* A} :

φ = ψ ↔ φ.comp Group.Abelianization.of = ψ.comp Group.Abelianization.of

Alias of Group.Abelianization.hom_ext_iff.

@[deprecated Group.Abelianization.map (since := "2026-11-03")]

def Abelianization.map {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) :

Group.Abelianization G →* Group.Abelianization H

Alias of Group.Abelianization.map.

The map operation of the Abelianization functor.

Equations

@Abelianization.map = @Group.Abelianization.map

Instances For

@[deprecated Group.Abelianization.lift_of_comp (since := "2026-11-03")]

theorem Abelianization.lift_of_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) :

Group.Abelianization.lift (Group.Abelianization.of.comp f) = Group.Abelianization.map f

Alias of Group.Abelianization.lift_of_comp.

Use map as the preferred simp normal form.

@[deprecated Group.Abelianization.map_of (since := "2026-11-03")]

theorem Abelianization.map_of {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) (x : G) :

(Group.Abelianization.map f) (Group.Abelianization.of x) = Group.Abelianization.of (f x)

Alias of Group.Abelianization.map_of.

@[deprecated Group.Abelianization.map_id (since := "2026-11-03")]

theorem Abelianization.map_id {G : Type u} [Group G] :

Group.Abelianization.map (MonoidHom.id G) = MonoidHom.id (Group.Abelianization G)

Alias of Group.Abelianization.map_id.

@[deprecated Group.Abelianization.map_comp (since := "2026-11-03")]

theorem Abelianization.map_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] (g : H →* I) :

(Group.Abelianization.map g).comp (Group.Abelianization.map f) = Group.Abelianization.map (g.comp f)

Alias of Group.Abelianization.map_comp.

@[deprecated Group.Abelianization.map_map_apply (since := "2026-11-03")]

theorem Abelianization.map_map_apply {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] {g : H →* I} {x : Group.Abelianization G} :

(Group.Abelianization.map g) ((Group.Abelianization.map f) x) = (Group.Abelianization.map (g.comp f)) x

Alias of Group.Abelianization.map_map_apply.

@[deprecated Group.abelianizationCongr_of (since := "2026-11-03")]

theorem abelianizationCongr_of {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) (x : G) :

e.abelianizationCongr (Group.Abelianization.of x) = Group.Abelianization.of (e x)

Alias of Group.abelianizationCongr_of.

@[deprecated Group.abelianizationCongr_refl (since := "2026-11-03")]

theorem abelianizationCongr_refl {G : Type u} [Group G] :

(MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Group.Abelianization G)

Alias of Group.abelianizationCongr_refl.

@[deprecated Group.abelianizationCongr_symm (since := "2026-11-03")]

theorem abelianizationCongr_symm {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) :

e.abelianizationCongr.symm = e.symm.abelianizationCongr

Alias of Group.abelianizationCongr_symm.

@[deprecated Group.abelianizationCongr_trans (since := "2026-11-03")]

theorem abelianizationCongr_trans {G : Type u} [Group G] {H : Type v} [Group H] {I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) :

e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr

Alias of Group.abelianizationCongr_trans.

@[deprecated Group.Abelianization.equivOfComm (since := "2026-11-03")]

def Abelianization.equivOfComm {H : Type u_1} [CommGroup H] :

H ≃* Group.Abelianization H

Alias of Group.Abelianization.equivOfComm.

An Abelian group is equivalent to its own abelianization.

Equations

@Abelianization.equivOfComm = @Group.Abelianization.equivOfComm

Instances For

@[deprecated Group.Abelianization.equivOfComm_apply (since := "2026-11-03")]

theorem Abelianization.equivOfComm_apply {H : Type u_1} [CommGroup H] (a : H) :

Group.Abelianization.equivOfComm a = Group.Abelianization.of a

Alias of Group.Abelianization.equivOfComm_apply.

@[deprecated Group.Abelianization.equivOfComm_symm_apply (since := "2026-11-03")]

theorem Abelianization.equivOfComm_symm_apply {H : Type u_1} [CommGroup H] (a : Group.Abelianization H) :

Group.Abelianization.equivOfComm.symm a = (Group.Abelianization.lift (MonoidHom.id H)) a

Alias of Group.Abelianization.equivOfComm_symm_apply.