Documentation

TauCeti.GroupTheory.Abelianization.Basic

Elementary facts about the abelianization #

Conjugate elements have the same image in the abelianization (Abelianization.of_inv_mul_mul), and written additively, the abelianization map sends products to sums in either order (Abelianization.ofMul_of_add_ofMul_of). An element has trivial image exactly when it lies in the commutator subgroup (Abelianization.of_eq_one_iff), so the abelianization map of a commutative group is injective (Abelianization.of_injective), and isomorphisms out of an abelianization are determined by their values on classes (Abelianization.mulEquiv_ext). Every element of the additive abelianization is the class of a group element (Abelianization.exists_eq_ofMul_of). The abelianization of a product of two groups is the product of their abelianizations (Abelianization.prodMulEquiv).

source
@[simp]
theorem Abelianization.of_inv_mul_mul {G : Type u_1} [Group G] (p q : G) :
of (p⁻¹ * q * p) = of q

Conjugate elements have the same image in the abelianization.

source
theorem Abelianization.ofMul_of_add_ofMul_of {G : Type u_1} [Group G] (p q : G) :
Additive.ofMul (of p) + Additive.ofMul (of q) = Additive.ofMul (of (q * p))

Written additively, the abelianization map sends the product q * p to the sum of the images of p and q.

source
@[simp]
theorem Abelianization.of_eq_one_iff {G : Type u_1} [Group G] {g : G} :
of g = 1 ↔ g ∈ commutator G

An element has trivial image in the abelianization exactly when it is in the commutator subgroup.

source
theorem Abelianization.exists_eq_ofMul_of {G : Type u_1} [Group G] (x : Additive (Abelianization G)) :
∃ (g : G), x = Additive.ofMul (of g)

Written additively, every element of the abelianization is the class of a group element.

source
theorem Abelianization.of_injective {G : Type u_1} [Group G] [IsMulCommutative G] :
Function.Injective ⇑of

The abelianization map of a commutative group is injective.

source
theorem Abelianization.mulEquiv_ext {G : Type u_1} [Group G] {M : Type u_2} [Monoid M] {e e' : Abelianization G ≃* M} (h : ∀ (x : G), e (of x) = e' (of x)) :
e = e'

Two isomorphisms out of an abelianization agree if they agree on the classes of elements.

source
def Abelianization.prodMulEquiv {G : Type u_1} [Group G] (H : Type u_2) [Group H] :
Abelianization (G × H) ≃* Abelianization G × Abelianization H

The abelianization of a product of two groups is the product of their abelianizations: the class of (g, h) corresponds to the pair of the classes of g and h.

Instances For
    source
    @[simp]
    theorem Abelianization.prodMulEquiv_of {G : Type u_1} [Group G] (H : Type u_2) [Group H] (gh : G × H) :
    (prodMulEquiv H) (of gh) = (of gh.1, of gh.2)