# Abelian groups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Maša Žaucer, Victor Blanchi, favonia and maybemabeline.

Created on 2022-03-17.

module group-theory.abelian-groups where

Imports
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-embeddings
open import foundation.binary-equivalences
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.full-subtypes
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.interchange-law
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.central-elements-groups
open import group-theory.commutative-monoids
open import group-theory.commutator-subgroups
open import group-theory.commutators-of-elements-groups
open import group-theory.conjugation
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.monoids
open import group-theory.nullifying-group-homomorphisms
open import group-theory.pullbacks-subgroups
open import group-theory.semigroups
open import group-theory.subgroups
open import group-theory.subgroups-generated-by-families-of-elements-groups
open import group-theory.trivial-subgroups

open import lists.concatenation-lists
open import lists.lists

open import structured-types.pointed-types-equipped-with-automorphisms


## Idea

Abelian groups are groups of which the group operation is commutative. It is common to write abelian groups additively, i.e., to write

  x + y


for the group operation of an abelian group, 0 for its unit element, and -x for the inverse of x.

## Definition

### The condition of being an abelian group

is-abelian-prop-Group : {l : Level} → Group l → Prop l
is-abelian-prop-Group G =
Π-Prop
( type-Group G)
( λ x →
Π-Prop
( type-Group G)
( λ y →
Id-Prop (set-Group G) (mul-Group G x y) (mul-Group G y x)))

is-abelian-Group : {l : Level} → Group l → UU l
is-abelian-Group G = type-Prop (is-abelian-prop-Group G)

is-prop-is-abelian-Group :
{l : Level} (G : Group l) → is-prop (is-abelian-Group G)
is-prop-is-abelian-Group G =
is-prop-type-Prop (is-abelian-prop-Group G)


### The type of abelian groups

Ab : (l : Level) → UU (lsuc l)
Ab l = Σ (Group l) is-abelian-Group

module _
{l : Level} (A : Ab l)
where

group-Ab : Group l
group-Ab = pr1 A

set-Ab : Set l
set-Ab = set-Group group-Ab

type-Ab : UU l
type-Ab = type-Group group-Ab

is-set-type-Ab : is-set type-Ab
is-set-type-Ab = is-set-type-Group group-Ab

add-Ab : type-Ab → type-Ab → type-Ab

add-Ab' : type-Ab → type-Ab → type-Ab

{x y x' y' : type-Ab} → x ＝ x' → y ＝ y' → add-Ab x y ＝ add-Ab x' y'

semigroup-Ab : Semigroup l
semigroup-Ab = semigroup-Group group-Ab

is-group-Ab : is-group-Semigroup semigroup-Ab
is-group-Ab = is-group-Group group-Ab

has-zero-Ab : is-unital-Semigroup semigroup-Ab
has-zero-Ab = is-unital-Group group-Ab

zero-Ab : type-Ab
zero-Ab = unit-Group group-Ab

is-zero-Ab : type-Ab → UU l
is-zero-Ab = is-unit-Group group-Ab

is-zero-Ab' : type-Ab → UU l
is-zero-Ab' = is-unit-Group' group-Ab

is-prop-is-zero-Ab : (x : type-Ab) → is-prop (is-zero-Ab x)
is-prop-is-zero-Ab = is-prop-is-unit-Group group-Ab

is-zero-prop-Ab : type-Ab → Prop l
is-zero-prop-Ab = is-unit-prop-Group group-Ab

has-negatives-Ab : is-group-is-unital-Semigroup semigroup-Ab has-zero-Ab
has-negatives-Ab = has-inverses-Group group-Ab

neg-Ab : type-Ab → type-Ab
neg-Ab = inv-Group group-Ab

(x : type-Ab) → add-Ab (neg-Ab x) x ＝ zero-Ab

(x : type-Ab) → add-Ab x (neg-Ab x) ＝ zero-Ab

(a b c d : type-Ab) →
interchange-law-commutative-and-associative

( associative-add-Ab a b c) ∙
( inv (associative-add-Ab a c b))

( inv (associative-add-Ab a b c)) ∙

(x y : type-Ab) →
( distributive-inv-mul-Group group-Ab) ∙
( commutative-add-Ab (neg-Ab y) (neg-Ab x))

neg-neg-Ab : (x : type-Ab) → neg-Ab (neg-Ab x) ＝ x
neg-neg-Ab = inv-inv-Group group-Ab

neg-zero-Ab : neg-Ab zero-Ab ＝ zero-Ab
neg-zero-Ab = inv-unit-Group group-Ab

transpose-eq-neg-Ab :
{x y : type-Ab} → neg-Ab x ＝ y → x ＝ neg-Ab y
transpose-eq-neg-Ab = transpose-eq-inv-Group group-Ab

transpose-eq-neg-Ab' :
{x y : type-Ab} → x ＝ neg-Ab y → neg-Ab x ＝ y
transpose-eq-neg-Ab' = transpose-eq-inv-Group' group-Ab


### The underlying commutative monoid of an abelian group

module _
{l : Level} (A : Ab l)
where

monoid-Ab : Monoid l
pr1 monoid-Ab = semigroup-Ab A
pr1 (pr2 monoid-Ab) = zero-Ab A
pr1 (pr2 (pr2 monoid-Ab)) = left-unit-law-add-Ab A
pr2 (pr2 (pr2 monoid-Ab)) = right-unit-law-add-Ab A

commutative-monoid-Ab : Commutative-Monoid l
pr1 commutative-monoid-Ab = monoid-Ab


### The structure of an abelian group

structure-abelian-group :
{l1 : Level} → UU l1 → UU l1
structure-abelian-group X =
Σ (structure-group X) (λ p → is-abelian-Group (group-structure-group X p))

abelian-group-structure-abelian-group :
{l1 : Level} → (X : UU l1) → structure-abelian-group X → Ab l1
pr1 (abelian-group-structure-abelian-group X (p , q)) =
group-structure-group X p
pr2 (abelian-group-structure-abelian-group X (p , q)) = q


### Conjugation in an abelian group

module _
{l : Level} (A : Ab l)
where

equiv-conjugation-Ab : (x : type-Ab A) → type-Ab A ≃ type-Ab A
equiv-conjugation-Ab = equiv-conjugation-Group (group-Ab A)

conjugation-Ab : (x : type-Ab A) → type-Ab A → type-Ab A
conjugation-Ab = conjugation-Group (group-Ab A)

equiv-conjugation-Ab' : (x : type-Ab A) → type-Ab A ≃ type-Ab A
equiv-conjugation-Ab' = equiv-conjugation-Group' (group-Ab A)

conjugation-Ab' : (x : type-Ab A) → type-Ab A → type-Ab A
conjugation-Ab' = conjugation-Group' (group-Ab A)


### Commutators in an abelian group

module _
{l : Level} (A : Ab l)
where

commutator-Ab : type-Ab A → type-Ab A → type-Ab A
commutator-Ab x y = commutator-Group (group-Ab A) x y


### The commutator subgroup of an abelian group

module _
{l : Level} (A : Ab l)
where

family-of-commutators-Ab : type-Ab A × type-Ab A → type-Ab A
family-of-commutators-Ab = family-of-commutators-Group (group-Ab A)

commutator-subgroup-Ab : Subgroup l (group-Ab A)
commutator-subgroup-Ab = commutator-subgroup-Group (group-Ab A)


### Any abelian group element yields a type equipped with an automorphism

module _
{l : Level} (A : Ab l) (a : type-Ab A)
where

pointed-type-with-aut-Ab : Pointed-Type-With-Aut l
pointed-type-with-aut-Ab = pointed-type-with-aut-Group (group-Ab A) a


## Properties

### Addition on an abelian group is a binary equivalence

#### Addition on the left is an equivalence

module _
{l : Level} (A : Ab l)
where

left-subtraction-Ab : type-Ab A → type-Ab A → type-Ab A
left-subtraction-Ab = left-div-Group (group-Ab A)

ap-left-subtraction-Ab :
{x x' y y' : type-Ab A} → x ＝ x' → y ＝ y' →
left-subtraction-Ab x y ＝ left-subtraction-Ab x' y'
ap-left-subtraction-Ab = ap-left-div-Group (group-Ab A)

is-section-left-subtraction-Ab :
(x : type-Ab A) → (add-Ab A x ∘ left-subtraction-Ab x) ~ id
is-section-left-subtraction-Ab = is-section-left-div-Group (group-Ab A)

is-retraction-left-subtraction-Ab :
(x : type-Ab A) → (left-subtraction-Ab x ∘ add-Ab A x) ~ id
is-retraction-left-subtraction-Ab = is-retraction-left-div-Group (group-Ab A)

equiv-add-Ab : type-Ab A → (type-Ab A ≃ type-Ab A)


#### Addition on the right is an equivalence

module _
{l : Level} (A : Ab l)
where

right-subtraction-Ab : type-Ab A → type-Ab A → type-Ab A
right-subtraction-Ab = right-div-Group (group-Ab A)

ap-right-subtraction-Ab :
{x x' y y' : type-Ab A} → x ＝ x' → y ＝ y' →
right-subtraction-Ab x y ＝ right-subtraction-Ab x' y'
ap-right-subtraction-Ab = ap-right-div-Group (group-Ab A)

is-section-right-subtraction-Ab :
(x : type-Ab A) →
(add-Ab' A x ∘ (λ y → right-subtraction-Ab y x)) ~ id
is-section-right-subtraction-Ab = is-section-right-div-Group (group-Ab A)

is-retraction-right-subtraction-Ab :
(x : type-Ab A) →
((λ y → right-subtraction-Ab y x) ∘ add-Ab' A x) ~ id
is-retraction-right-subtraction-Ab =
is-retraction-right-div-Group (group-Ab A)

equiv-add-Ab' : type-Ab A → (type-Ab A ≃ type-Ab A)


#### Addition on an abelian group is a binary equivalence

module _
{l : Level} (A : Ab l)
where



### Addition on an abelian group is a binary embedding

module _
{l : Level} (A : Ab l)
where



### Addition on an abelian group is pointwise injective from both sides

module _
{l : Level} (A : Ab l)
where



### Transposing identifications in abelian groups

module _
{l : Level} (A : Ab l)
where

{x y z : type-Ab A} →
Id (add-Ab A x y) z → Id x (add-Ab A z (neg-Ab A y))

{x y z : type-Ab A} →
Id x (add-Ab A z (neg-Ab A y)) → add-Ab A x y ＝ z

{x y z : type-Ab A} →
Id (add-Ab A x y) z → Id y (add-Ab A (neg-Ab A x) z)

{x y z : type-Ab A} →
Id y (add-Ab A (neg-Ab A x) z) → Id (add-Ab A x y) z

{x y z w : type-Ab A} →
left-subtraction-Ab A x y ＝ right-subtraction-Ab A z w
double-transpose-eq-mul-Group (group-Ab A)

{x y z w : type-Ab A} →
right-subtraction-Ab A x y ＝ left-subtraction-Ab A z w
double-transpose-eq-mul-Group' (group-Ab A)


### Any idempotent element in an abelian group is zero

module _
{l : Level} (A : Ab l)
where

is-idempotent-Ab : type-Ab A → UU l
is-idempotent-Ab = is-idempotent-Group (group-Ab A)

is-zero-is-idempotent-Ab :
{x : type-Ab A} → is-idempotent-Ab x → is-zero-Ab A x
is-zero-is-idempotent-Ab = is-unit-is-idempotent-Group (group-Ab A)


### Taking negatives of elements of an abelian group is an equivalence

module _
{l : Level} (A : Ab l)
where

is-equiv-neg-Ab : is-equiv (neg-Ab A)
is-equiv-neg-Ab = is-equiv-inv-Group (group-Ab A)

equiv-equiv-neg-Ab : type-Ab A ≃ type-Ab A
equiv-equiv-neg-Ab = equiv-equiv-inv-Group (group-Ab A)


### Two elements x and y are equal iff -x + y = 0

module _
{l : Level} (A : Ab l)
where

eq-is-zero-left-subtraction-Ab :
{x y : type-Ab A} →
is-zero-Ab A (left-subtraction-Ab A x y) → x ＝ y
eq-is-zero-left-subtraction-Ab =
eq-is-unit-left-div-Group (group-Ab A)

is-zero-left-subtraction-Ab :
{x y : type-Ab A} →
x ＝ y → is-zero-Ab A (left-subtraction-Ab A x y)
is-zero-left-subtraction-Ab = is-unit-left-div-eq-Group (group-Ab A)


### Two elements x and y are equal iff x - y = 0

module _
{l : Level} (A : Ab l)
where

eq-is-zero-right-subtraction-Ab :
{x y : type-Ab A} →
is-zero-Ab A (right-subtraction-Ab A x y) → x ＝ y
eq-is-zero-right-subtraction-Ab =
eq-is-unit-right-div-Group (group-Ab A)

is-zero-right-subtraction-eq-Ab :
{x y : type-Ab A} →
x ＝ y → is-zero-Ab A (right-subtraction-Ab A x y)
is-zero-right-subtraction-eq-Ab =
is-unit-right-div-eq-Group (group-Ab A)


### The negative of -x + y is -y + x

module _
{l : Level} (A : Ab l)
where

neg-left-subtraction-Ab :
(x y : type-Ab A) →
neg-Ab A (left-subtraction-Ab A x y) ＝ left-subtraction-Ab A y x
neg-left-subtraction-Ab = inv-left-div-Group (group-Ab A)


### The negative of x - y is y - x

module _
{l : Level} (A : Ab l)
where

neg-right-subtraction-Ab :
(x y : type-Ab A) →
neg-Ab A (right-subtraction-Ab A x y) ＝ right-subtraction-Ab A y x
neg-right-subtraction-Ab = inv-right-div-Group (group-Ab A)


### The sum of -x + y and -y + z is -x + z

module _
{l : Level} (A : Ab l)
where

(x y z : type-Ab A) →
add-Ab A (left-subtraction-Ab A x y) (left-subtraction-Ab A y z) ＝
left-subtraction-Ab A x z


### The sum of x - y and y - z is x - z

module _
{l : Level} (A : Ab l)
where

(x y z : type-Ab A) →
add-Ab A (right-subtraction-Ab A x y) (right-subtraction-Ab A y z) ＝
right-subtraction-Ab A x z


### Conjugation is the identity function

Proof: Consider two elements x and y of an abelian group. Then

  (x + y) - x ＝ (y + x) - x ＝ y,


where the last step holds at once since the function _ - x is a retraction of the function _ + x.

Note that this is a fairly common way to make quick calculations.

module _
{l : Level} (A : Ab l)
where

is-identity-conjugation-Ab :
(x : type-Ab A) → conjugation-Ab A x ~ id
is-identity-conjugation-Ab x y =
( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙
( is-retraction-right-subtraction-Ab A x y)


### Laws for conjugation and addition

module _
{l : Level} (A : Ab l)
where

htpy-conjugation-Ab :
(x : type-Ab A) →
conjugation-Ab' A x ~ conjugation-Ab A (neg-Ab A x)
htpy-conjugation-Ab = htpy-conjugation-Group (group-Ab A)

htpy-conjugation-Ab' :
(x : type-Ab A) →
conjugation-Ab A x ~ conjugation-Ab' A (neg-Ab A x)
htpy-conjugation-Ab' = htpy-conjugation-Group' (group-Ab A)

conjugation-zero-Ab :
(x : type-Ab A) → conjugation-Ab A x (zero-Ab A) ＝ zero-Ab A
conjugation-zero-Ab = conjugation-unit-Group (group-Ab A)

(x y : type-Ab A) →
add-Ab A (neg-Ab A x) (conjugation-Ab A x y) ＝
right-subtraction-Ab A y x
right-conjugation-law-mul-Group (group-Ab A)

(x y : type-Ab A) →
add-Ab A x (conjugation-Ab' A x y) ＝ add-Ab A y x
right-conjugation-law-mul-Group' (group-Ab A)

(x y : type-Ab A) →
add-Ab A (conjugation-Ab A x y) x ＝ add-Ab A x y
left-conjugation-law-mul-Group (group-Ab A)

(x y : type-Ab A) →
add-Ab A (conjugation-Ab' A x y) (neg-Ab A x) ＝
left-subtraction-Ab A x y
left-conjugation-law-mul-Group' (group-Ab A)

(x y z : type-Ab A) →
conjugation-Ab A x (add-Ab A y z) ＝
add-Ab A (conjugation-Ab A x y) (conjugation-Ab A x z)
distributive-conjugation-mul-Group (group-Ab A)

conjugation-neg-Ab :
(x y : type-Ab A) →
conjugation-Ab A x (neg-Ab A y) ＝ neg-Ab A (conjugation-Ab A x y)
conjugation-neg-Ab = conjugation-inv-Group (group-Ab A)

conjugation-neg-Ab' :
(x y : type-Ab A) →
conjugation-Ab' A x (neg-Ab A y) ＝
neg-Ab A (conjugation-Ab' A x y)
conjugation-neg-Ab' = conjugation-inv-Group' (group-Ab A)

conjugation-left-subtraction-Ab :
(x y : type-Ab A) →
conjugation-Ab A x (left-subtraction-Ab A x y) ＝
right-subtraction-Ab A y x
conjugation-left-subtraction-Ab =
conjugation-left-div-Group (group-Ab A)

conjugation-left-subtraction-Ab' :
(x y : type-Ab A) →
conjugation-Ab A y (left-subtraction-Ab A x y) ＝
right-subtraction-Ab A y x
conjugation-left-subtraction-Ab' =
conjugation-left-div-Group' (group-Ab A)

conjugation-right-subtraction-Ab :
(x y : type-Ab A) →
conjugation-Ab' A y (right-subtraction-Ab A x y) ＝
left-subtraction-Ab A y x
conjugation-right-subtraction-Ab =
conjugation-right-div-Group (group-Ab A)

conjugation-right-subtraction-Ab' :
(x y : type-Ab A) →
conjugation-Ab' A x (right-subtraction-Ab A x y) ＝
left-subtraction-Ab A y x
conjugation-right-subtraction-Ab' =
conjugation-right-div-Group' (group-Ab A)


### Addition of a list of elements in an abelian group

module _
{l : Level} (A : Ab l)
where

add-list-Ab : list (type-Ab A) → type-Ab A

(l1 l2 : list (type-Ab A)) →
Id
preserves-concat-mul-list-Group (group-Ab A)


### A group is abelian if and only if every element is central

Proof: These two conditions are the same on the nose.

module _
{l : Level} (G : Group l)
where

is-abelian-every-element-central-Group :
((x : type-Group G) → is-central-element-Group G x) → is-abelian-Group G
is-abelian-every-element-central-Group = id

every-element-central-is-abelian-Group :
is-abelian-Group G → ((x : type-Group G) → is-central-element-Group G x)
every-element-central-is-abelian-Group = id


### A group is abelian if and only if every commutator is equal to the unit

Proof: For any two elements u and v in a group we have the logical equivalence

  (uv⁻¹ ＝ 1) ↔ (u ＝ v).


Since the commutator of x and y is defined as [x,y] := (xy)(yx)⁻¹, we see that the claim is a direct consequence of this logical equivalence.

module _
{l : Level} (G : Group l)
where

is-abelian-is-unit-commutator-Group :
((x y : type-Group G) → is-unit-Group G (commutator-Group G x y)) →
is-abelian-Group G
is-abelian-is-unit-commutator-Group H x y =
eq-is-unit-right-div-Group G (H x y)

is-abelian-is-unit-commutator-Group' :
((x y : type-Group G) → is-unit-Group' G (commutator-Group G x y)) →
is-abelian-Group G
is-abelian-is-unit-commutator-Group' H x y =
eq-is-unit-right-div-Group G (inv (H x y))

is-unit-commutator-is-abelian-Group :
is-abelian-Group G →
(x y : type-Group G) → is-unit-Group G (commutator-Group G x y)
is-unit-commutator-is-abelian-Group H x y =
is-unit-right-div-eq-Group G (H x y)

is-unit-commutator-is-abelian-Group' :
is-abelian-Group G →
(x y : type-Group G) → is-unit-Group' G (commutator-Group G x y)
is-unit-commutator-is-abelian-Group' H x y =
inv (is-unit-right-div-eq-Group G (H x y))

module _
{l : Level} (A : Ab l)
where

is-zero-commutator-Ab :
(x y : type-Ab A) → is-zero-Ab A (commutator-Ab A x y)
is-zero-commutator-Ab =

is-zero-commutator-Ab' :
(x y : type-Ab A) → is-zero-Ab' A (commutator-Ab A x y)
is-zero-commutator-Ab' =


### A group is abelian if and only if its commutator subgroup is trivial

Proof: We saw above that a group is abelian if and only if every commutator is the unit element. The latter condition holds if and only if the subgroup generated by the commutators, i.e., the commutator subgroup, is trivial.

module _
{l : Level} (G : Group l)
where

is-abelian-is-trivial-commutator-subgroup-Group :
is-trivial-Subgroup G (commutator-subgroup-Group G) →
is-abelian-Group G
is-abelian-is-trivial-commutator-subgroup-Group H =
is-abelian-is-unit-commutator-Group' G
( λ x y →
is-family-of-units-is-trivial-subgroup-family-of-elements-Group G
( family-of-commutators-Group G)
( H)
( x , y))

module _
{l : Level} (A : Ab l)
where

abstract
is-trivial-commutator-subgroup-Ab :
is-trivial-Subgroup (group-Ab A) (commutator-subgroup-Ab A)
is-trivial-commutator-subgroup-Ab =
is-trivial-subgroup-family-of-elements-Group
( group-Ab A)
( family-of-commutators-Ab A)
( λ (x , y) → is-zero-commutator-Ab' A x y)


### Every group homomorphism into an abelian group nullifies the commutator subgroup

Proof: Consider a group homomorphism f : G → A into an abelian group A. Our goal is to show that f nullifies the commutator subgroup [G,G], i.e., that [G,G] is contained in the kernel of f.

Since A is abelian it follows that the commutator subgroup of A is trivial. Furthermore, any group homomorphism maps the commutator subgroup to the commutator subgroup, i.e., we have f [G,G] ⊆ [A,A]. Since the commutator subgroup [A,A] is trivial, this means that f nullifies the commutator subgroup of G.

module _
{l1 l2 : Level} (G : Group l1) (A : Ab l2)
where

nullifies-commutator-normal-subgroup-hom-group-Ab :
(f : hom-Group G (group-Ab A)) →
nullifies-normal-subgroup-hom-Group G
( group-Ab A)
( f)
( commutator-normal-subgroup-Group G)
nullifies-commutator-normal-subgroup-hom-group-Ab f =
transitive-leq-Subgroup G
( commutator-subgroup-Group G)
( pullback-Subgroup G
( group-Ab A)
( f)
( commutator-subgroup-Group (group-Ab A)))
( pullback-Subgroup G (group-Ab A) f (trivial-Subgroup (group-Ab A)))
( λ x → is-trivial-commutator-subgroup-Ab A _)
( preserves-commutator-subgroup-hom-Group G (group-Ab A) f)

is-equiv-hom-nullifying-hom-group-Ab :
is-equiv
( hom-nullifying-hom-Group G
( group-Ab A)
( commutator-normal-subgroup-Group G))
is-equiv-hom-nullifying-hom-group-Ab =
is-equiv-inclusion-is-full-subtype
( λ f →
nullifies-normal-subgroup-prop-hom-Group G
( group-Ab A)
( f)
( commutator-normal-subgroup-Group G))
( nullifies-commutator-normal-subgroup-hom-group-Ab)

compute-nullifying-hom-group-Ab :
nullifying-hom-Group G (group-Ab A) (commutator-normal-subgroup-Group G) ≃
hom-Group G (group-Ab A)
compute-nullifying-hom-group-Ab =
equiv-inclusion-is-full-subtype
( λ f →
nullifies-normal-subgroup-prop-hom-Group G
( group-Ab A)
( f)
( commutator-normal-subgroup-Group G))
( nullifies-commutator-normal-subgroup-hom-group-Ab)