# Abelian groups

Content created by Fredrik Bakke.

Created on 2024-02-07.

module finite-group-theory.finite-abelian-groups where

Imports
open import finite-group-theory.finite-groups

open import foundation.equivalences
open import foundation.identity-types
open import foundation.interchange-law
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.conjugation
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups

open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types


## Idea

Abelian groups are groups of which the group operation is commutative

## Definition

### The condition of being an abelian group

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

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-𝔽

finite-abelian-group-is-finite-Ab :
{l : Level} → (A : Ab l) → is-finite (type-Ab A) → Ab-𝔽 l
pr1 (finite-abelian-group-is-finite-Ab A f) =
finite-group-is-finite-Group (group-Ab A) f
pr2 (finite-abelian-group-is-finite-Ab A f) = pr2 A

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

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

group-Ab-𝔽 : Group l
group-Ab-𝔽 = group-Group-𝔽 finite-group-Ab-𝔽

finite-type-Ab-𝔽 : 𝔽 l
finite-type-Ab-𝔽 = finite-type-Group-𝔽 finite-group-Ab-𝔽

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

is-finite-type-Ab-𝔽 : is-finite type-Ab-𝔽
is-finite-type-Ab-𝔽 = is-finite-type-Group-𝔽 finite-group-Ab-𝔽

set-Ab-𝔽 : Set l
set-Ab-𝔽 = set-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-𝔽

ab-Ab-𝔽 : Ab l
pr1 ab-Ab-𝔽 = group-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-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

(x y : type-Ab-𝔽) →

neg-neg-Ab-𝔽 : (x : type-Ab-𝔽) → neg-Ab-𝔽 (neg-Ab-𝔽 x) ＝ x
neg-neg-Ab-𝔽 = neg-neg-Ab ab-Ab-𝔽

neg-zero-Ab-𝔽 : neg-Ab-𝔽 zero-Ab-𝔽 ＝ zero-Ab-𝔽
neg-zero-Ab-𝔽 = neg-zero-Ab ab-Ab-𝔽


### 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)


## Properties

### There is a finite number of ways to equip a finite type with the structure of an abelian group

module _
{l : Level}
(X : 𝔽 l)
where

structure-abelian-group-𝔽 : UU l
structure-abelian-group-𝔽 =
Σ ( structure-group-𝔽 X)
( λ g → is-abelian-Group-𝔽 (finite-group-structure-group-𝔽 X g))

finite-abelian-group-structure-abelian-group-𝔽 :
structure-abelian-group-𝔽 → Ab-𝔽 l
pr1 (finite-abelian-group-structure-abelian-group-𝔽 (m , c)) =
finite-group-structure-group-𝔽 X m
pr2 (finite-abelian-group-structure-abelian-group-𝔽 (m , c)) = c

is-finite-structure-abelian-group-𝔽 :
is-finite structure-abelian-group-𝔽
is-finite-structure-abelian-group-𝔽 =
is-finite-Σ
( is-finite-structure-group-𝔽 X)
( λ g →
is-finite-Π
( is-finite-type-𝔽 X)
( λ x →
is-finite-Π
( is-finite-type-𝔽 X)
( λ y → is-finite-eq-𝔽 X)))