# 4 Abstract Algebra

This chapter follows the book Basic algebra by Nathan Jacobson. It builds upon and extends the formalism in Exploring the Structure of an Algebra Text with Locales by Clemens Ballarin. You can import it from AFP (see 2.15)

```
theory XXX
imports Main "Jacobson_Basic_Algebra.Group_Theory"
begin
end
```

We will add our own improvements and extensions to this library. The modified code can be found on github.

## 4.1 Semigroups

Semigroup is a set `M`

equipped with a `composition`

(also called “multiplication”) operation `⋅`

which is associative, that is `(a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)`

.

```
locale semigroup =
fixes M and composition (infixl "⋅" 70)
assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M"
and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)"
```

Because this definition of `semigroup`

fixes two constants `M`

and `composition`

,
most math textbooks would say that `monoid`

is a tuple `(M,⋅)`

.

Most axioms are similar to those in 2.14.1 but one is new.
The axiom `composition_closed`

says that the operation is closed, meaning that if we only operate on elements from `M`

we will never go outside of this set. This axiom was missing in 2.14.1 which was severely limiting
because without `M`

and `composition_closed`

it is impossible to define subsemigroups.

```
locale subsemigroup = semigroup M "(⋅)"
for N and M and composition (infixl "⋅" 70) +
assumes subset: "N ⊆ M"
and sub_composition_closed: "⟦ a ∈ N; b ∈ N ⟧ ⟹ a ⋅ b ∈ N"
```

The `for`

keyword specifies that `semigroup`

is a prerequisite for `subsemigroup`

. It is equivalent to the following (more familiar 2.14.1) syntax definition

```
locale subsemigroup = semigroup +
fixes N
assumes subset: "N ⊆ M"
and sub_composition_closed: "[| a ∈ N; b ∈ N |] ⟹ a · b ∈ N"
```

with the only difference being the order of fixed constants (previously it was `N M composition unit`

and now its `M composition unit N`

).
In fact this latter definition (without `for`

) is merely a syntactic sugar for the former one (with `for`

).

The axiom `sub_composition_closed`

states that a subsemigroup is a subset `N`

of semigroup `M`

such that the operation `·`

is closed in `N`

.

Every subsemigroup is also a semigroup, which is expressed using `sublocale`

command.

```
context subsemigroup begin
lemma sub [intro, simp]:
"a ∈ N ⟹ a ∈ M"
using subset by blast
sublocale sub: semigroup N "(⋅)"
by unfold_locales (auto simp: sub_composition_closed)
end (* subsemigroup *)
```

The brackets around `(⋅)`

are necessary, otherwise you will get syntax error.
Note that in the definition of `subsemigroup`

we included `semigroup M "(⋅)"`

as a prerequisite but
now we are proving `semigroup N "(⋅)"`

.
Once the proof is done you will see

`local.sub.semigroup_axioms: semigroup N (⋅)`

in the “Find Theorems” tab but it will only show up if you place your cursor inside the `subsemigroup`

context (this is what `local`

stands for).

## 4.2 Monoids

Monoid is a set `M`

equipped with a `composition`

(also called “multiplication”) associative operation `⋅`

and a `unit`

(also called “neutral”) element `𝟭`

. Every monoid is a semigroup, therefore we include
`semigroup M "(⋅)"`

as a prerequisite for `monoid`

.

```
text ‹Def 1.1› (* this is definition 1.1 from the Basic algebra book*)
text ‹p 28, ll 28--30› (* you can find it on page 28 *)
locale monoid =
semigroup M "(⋅)" for M and composition (infixl "⋅" 70) and unit ("𝟭") +
assumes unit_closed [intro, simp]: "𝟭 ∈ M"
and left_unit [intro, simp]: "a ∈ M ⟹ 𝟭 ⋅ a = a"
and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ 𝟭 = a"
```

Because this definition of `monoid`

fixes three constants `M`

, `composition`

and `uni`

,
most math textbooks would say that `monoid`

is a triple `(M,⋅,𝟭)`

.

Most axioms are similar to those in 2.14.2. We can define submonoids similarly as before.

```
text ‹p 29, ll 27--28›
locale submonoid = monoid M "(⋅)" 𝟭
for N and M and composition (infixl "⋅" 70) and unit ("𝟭") +
assumes subset: "N ⊆ M"
and sub_composition_closed: "⟦ a ∈ N; b ∈ N ⟧ ⟹ a ⋅ b ∈ N"
and sub_unit_closed: "𝟭 ∈ N"
```

As an example we can show that `nat`

is a monoid under the addition operation
## Proof

```
theory Test
imports "Jacobson_Basic_Algebra.Group_Theory"
begin
hide_type nat
no_notation plus (infixl "+" 65) and Groups.zero_class.zero ("0")
datatype nat = Zero ("0") | Suc nat
primrec plus :: "nat ⇒ nat ⇒ nat" (infixl "+" 65) where
"0 + y = y" |
"(Suc x) + y = Suc (x + y)"
interpretation plus: monoid "UNIV" plus Zero
proof
fix a b c :: "nat"
show "a ∈ UNIV ⟹ b ∈ UNIV ⟹ a + b ∈ UNIV"
by simp_all
show "0 ∈ UNIV"
by simp
show "a ∈ UNIV ⟹ b ∈ UNIV ⟹ c ∈ UNIV ⟹ a + b + c = a + (b + c)"
by (simp, induct_tac a, auto)
show "a ∈ UNIV ⟹ 0 + a = a"
by simp
show "a ∈ UNIV ⟹ a + 0 = a"
by (simp, induct_tac a, auto)
qed
end
```

## Proof

Adding two even numbers together must yield another even number, hence the monoid is closed in the set of even numbers.

```
theory Test
imports "Jacobson_Basic_Algebra.Group_Theory"
begin
hide_type nat
no_notation plus (infixl "+" 65) and Groups.zero_class.zero ("0")
datatype nat = Zero ("0") | Suc nat
primrec plus :: "nat ⇒ nat ⇒ nat" (infixl "+" 65) where
l_zero: "0 + y = y" | (* we assign the name l_zero to this equation so that we can use it like a theorem *)
suc_dist: "(Suc x) + y = Suc (x + y)"
inductive_set even :: "nat set" where
zero_is_even[intro!]: "0 ∈ even" |
step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even"
(* Note: you can check the two following types in the Query tab *)
(* Test.even :: "nat set" *)
(* Group_Theory.monoid :: "'a set ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ bool" *)
interpretation plus: monoid "even" plus Zero
proof
fix a b c :: "nat"
show "a ∈ even ⟹ b ∈ even ⟹ a + b ∈ even"
apply(erule even.induct)
(* we perform induction as defined by the inductive_set
1. b ∈ even ⟹ 0 + b ∈ even
2. ⋀n. b ∈ even ⟹ n ∈ even ⟹ n + b ∈ even ⟹ Suc (Suc n) + b ∈ even
*)
apply(simp) (* this solves the 1. goal *)
apply(subst suc_dist) (* ⋀n. b ∈ even ⟹ n ∈ even ⟹ n + b ∈ even ⟹ Suc (Suc n + b) ∈ even *)
apply(subst suc_dist) (* ⋀n. b ∈ even ⟹ n ∈ even ⟹ n + b ∈ even ⟹ Suc (Suc (n + b)) ∈ even *)
apply(rule step) (* ⋀n. b ∈ even ⟹ n ∈ even ⟹ n + b ∈ even ⟹ n + b ∈ even *)
apply(assumption) (* the "n + b ∈ even" is already among premises *)
done
show "0 ∈ even"
by(rule zero_is_even)
show "a ∈ even ⟹ b ∈ even ⟹ c ∈ even ⟹ a + b + c = a + (b + c)"
by(erule even.induct, auto)
show "a ∈ even ⟹ 0 + a = a"
by simp
show "a ∈ even ⟹ a + 0 = a"
by (erule even.induct, auto)
qed
end
```

Every submonoid is also a monoid.

```
context submonoid begin
text ‹p 29, ll 27--28›
lemma sub [intro, simp]:
"a ∈ N ⟹ a ∈ M"
using subset by blast
text ‹p 29, ll 32--33›
sublocale sub: monoid N "(⋅)" 𝟭
by unfold_locales (auto simp: sub_composition_closed sub_unit_closed)
end
```

The `submonoid`

predicate (locales are predicates 2.14.1) is transitive, meaning that if `K`

is
a submonoid of `N`

and `N`

is a submonoid of `M`

then `K`

is a submonoid of `M`

.

```
text ‹p 29, ll 33--34›
theorem submonoid_transitive:
assumes "submonoid K N composition unit"
and "submonoid N M composition unit"
shows "submonoid K M composition unit"
proof -
interpret K: submonoid K N composition unit by fact
interpret M: submonoid N M composition unit by fact
show ?thesis by unfold_locales auto
qed
```

To understand what this proof does, click for more explanation below.
## Proof explanation

```
theorem submonoid_transitive:
assumes "submonoid K N composition unit"
and "submonoid N M composition unit"
shows "submonoid K M composition unit"
proof -
interpret K: submonoid K N composition unit by fact (* This works analogically to the `fixes` command *)
interpret M: submonoid N M composition unit by fact (* which allows us to use K and M in the proof. *)
show ?thesis (* This is shorthand for: "submonoid K M composition unit" *)
apply(unfold_locales)
(* Current goals:
1. K ⊆ M
2. ⋀a b. a ∈ K ⟹ b ∈ K ⟹ composition a b ∈ K
3. unit ∈ K
*)
apply(rule "Set.subset_trans"[of K N M])
(* Use query tab to find the theorem and check the type of subset_trans
Set.subset_trans: ?A ⊆ ?B ⟹ ?B ⊆ ?C ⟹ ?A ⊆ ?C
The [of K N M] says that ?A ?B and ?C should be substituted with K N and M yielding rule
K ⊆ N ⟹ N ⊆ M ⟹ K ⊆ M
Its application transforms the goal "K ⊆ M" into two new goals
1. K ⊆ N
2. N ⊆ M
3. ⋀a b. a ∈ K ⟹ b ∈ K ⟹ composition a b ∈ K
4. unit ∈ K
*)
apply(rule submonoid.subset[of K N composition unit])
(* Use query tab to find the theorem and check its type
Group_Theory.submonoid.subset: submonoid ?N ?M ?composition ?unit ⟹ ?N ⊆ ?M
Application of this rule results in
1. submonoid K N composition unit
2. N ⊆ M
3. ⋀a b. a ∈ K ⟹ b ∈ K ⟹ composition a b ∈ K
4. unit ∈ K
*)
apply(fact) (* "submonoid K N composition unit" is among premises *)
apply(rule submonoid.subset[of N M composition unit])
apply(fact) (* This solves the second subgoal analogically. We are now left with
1. ⋀a b. a ∈ K ⟹ b ∈ K ⟹ composition a b ∈ K
2. unit ∈ K
*)
apply(rule local.K.sub.composition_closed)
(*
1. ⋀a b. a ∈ K ⟹ b ∈ K ⟹ a ∈ K
2. ⋀a b. a ∈ K ⟹ b ∈ K ⟹ b ∈ K
3. unit ∈ K
*)
apply(assumption)
apply(assumption)
(*
1. unit ∈ K
*)
apply(rule local.K.sub_unit_closed)
done
qed
```

### 4.2.1 Transformations

A very important example of monoid is the operation of function composition.
Consider some set `S`

```
text ‹p 28, l 23›
locale transformations =
fixes S :: "'a set"
(* assumes non_vacuous: "S ≠ {}" *) (* Jacobson requires this but we don't need it, strange. *)
```

then the set of all functions `S →⇩E S`

(2.13) is a monoid under `compose`

operation

```
text ‹Monoid of all transformations›
text ‹p 28, ll 23--24›
sublocale transformations ⊆ monoid "S →⇩E S" "compose S" "identity S"
by unfold_locales (auto simp: PiE_def compose_eq compose_assoc Id_compose compose_Id)
```

and `identity`

is is the neutral element

`abbreviation "identity S ≡ (λx ∈ S. x)"`

## 4.3 Inverse elements

An element `u`

of monoid `M`

is invertible if there exist inverse element `v`

such that `u ⋅ v = 𝟭`

and `v ⋅ u = 𝟭`

.

```
context monoid begin
text ‹p 31, ll 3--5›
definition invertible where "u ∈ M ⟹ invertible u ⟷ (∃v ∈ M. u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭)"
```

For example the inverse of `1`

under addition operation (`plus`

) is `-1`

because `1 + (-1) = 0`

and `0`

is the neutral element of addition. The inverse of `1`

under multiplication is `1`

because `1 * 1 = 1`

and `1`

is the neutral element of multiplication.

## Introduction and elimination rules needed for automated proofs

```
text ‹p 31, ll 3--5›
lemma invertibleI [intro]:
"⟦ u ⋅ v = 𝟭; v ⋅ u = 𝟭; u ∈ M; v ∈ M ⟧ ⟹ invertible u"
unfolding invertible_def by fast
text ‹p 31, ll 3--5›
lemma invertibleE [elim]:
"⟦ invertible u; ⋀v. ⟦ u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭; v ∈ M ⟧ ⟹ P; u ∈ M ⟧ ⟹ P"
unfolding invertible_def by fast
```

The inverse element is unique

```
text ‹p 31, ll 6--7›
theorem inverse_unique:
"⟦ u ⋅ v' = 𝟭; v ⋅ u = 𝟭; u ∈ M; v ∈ M; v' ∈ M ⟧ ⟹ v = v'"
by (metis associative left_unit right_unit)
```

because if `u ⋅ v' = 𝟭`

and `v ⋅ u = 𝟭`

then

```
v ⋅ (u ⋅ v') = v ⋅ 𝟭
(v ⋅ u) ⋅ v' = v ⋅ 𝟭
𝟭 ⋅ v' = v ⋅ 𝟭
v' = v ⋅ 𝟭
v' = v
v = v'
```

## More detailed proof

Here we are using Isar structured proof syntax. This allows us to use `from`

…`have`

to divide the proof into intermediate stepping stones for better readability.

```
theorem inverse_unique:
assumes uv1:"u ⋅ v' = 𝟭"
assumes vu1:"v ⋅ u = 𝟭"
assumes um:"u ∈ M"
assumes vm:"v ∈ M"
assumes v'm:"v' ∈ M"
shows "v = v'"
proof -
from uv1 have "v ⋅ (u ⋅ v') = v ⋅ 𝟭"
apply (rule subst) (* 1. v ⋅ (u ⋅ v') = v ⋅ (u ⋅ v') *)
apply (rule refl) (* No subgoals! *)
done
from this um vm v'm have "v ⋅ u ⋅ v' = v ⋅ 𝟭" (*the keyword 'this' refers to the previous stepping stone "v ⋅ (u ⋅ v') = v ⋅ 𝟭" *)
apply (subst associative) (* 4 subgoals: *)
(*
1. v ⋅ (u ⋅ v') = v ⋅ 𝟭 ⟹ u ∈ M ⟹ v ∈ M ⟹ v' ∈ M ⟹ v ∈ M
2. v ⋅ (u ⋅ v') = v ⋅ 𝟭 ⟹ u ∈ M ⟹ v ∈ M ⟹ v' ∈ M ⟹ u ∈ M
3. v ⋅ (u ⋅ v') = v ⋅ 𝟭 ⟹ u ∈ M ⟹ v ∈ M ⟹ v' ∈ M ⟹ v' ∈ M
4. v ⋅ (u ⋅ v') = v ⋅ 𝟭 ⟹ u ∈ M ⟹ v ∈ M ⟹ v' ∈ M ⟹ v ⋅ (u ⋅ v') = v ⋅ 𝟭
*)
apply (assumption) (* each subgoal occurs among the assumptions *)
apply (assumption)
apply (assumption)
apply (assumption)
done
from this vu1 have "𝟭 ⋅ v' = v ⋅ 𝟭"
apply(subst vu1[symmetric]) (* 1. v ⋅ u ⋅ v' = v ⋅ 𝟭 ⟹ v ⋅ u = 𝟭 ⟹ v ⋅ u ⋅ v' = v ⋅ 𝟭 *)
apply(assumption) (* No subgoals! *)
done
from v'm this have "v' = v ⋅ 𝟭"
apply(subst left_unit[symmetric]) (* two subgoals: *)
(*
1. v' ∈ M ⟹ 𝟭 ⋅ v' = v ⋅ 𝟭 ⟹ v' ∈ M
2. v' ∈ M ⟹ 𝟭 ⋅ v' = v ⋅ 𝟭 ⟹ 𝟭 ⋅ v' = v ⋅ 𝟭
*)
apply(assumption) (* each subgoal occurs among the assumptions *)
apply(assumption)
done
from vm this show "v = v'"
apply(subst right_unit[symmetric]) (* 2 subgoals: *)
(*
1. v ∈ M ⟹ v' = v ⋅ 𝟭 ⟹ v ∈ M
2. v ∈ M ⟹ v' = v ⋅ 𝟭 ⟹ v ⋅ 𝟭 = v'
*)
apply(assumption) (* 1. v ∈ M ⟹ v' = v ⋅ 𝟭 ⟹ v ⋅ 𝟭 = v' *)
apply(rule sym) (* 1. v ∈ M ⟹ v' = v ⋅ 𝟭 ⟹ v' = v ⋅ 𝟭 *)
apply(assumption) (* No subgoals! *)
done
qed
```

##
More detailed proof (using `unfolding`

)

```
theorem inverse_unique:
assumes uv1: "u ⋅ v' = 𝟭"
assumes vu1: "v ⋅ u = 𝟭"
assumes um: "u ∈ M"
assumes vm: "v ∈ M"
assumes v'm: "v' ∈ M"
shows "v = v'"
proof -
have "v ⋅ (u ⋅ v') = v ⋅ 𝟭" unfolding uv1 by (rule refl)
from this have "v ⋅ u ⋅ v' = v ⋅ 𝟭" unfolding associative[OF vm um v'm] by assumption
from this have "𝟭 ⋅ v' = v ⋅ 𝟭" unfolding vu1 by assumption
from this have "v' = v ⋅ 𝟭" unfolding left_unit[OF v'm] by assumption
from this show "v = v'" unfolding right_unit[OF vm] by (rule sym)
qed
```

##
More detailed proof (using `also have`

)

```
theorem inverse_unique:
assumes uv1: "u ⋅ v' = 𝟭"
assumes vu1: "v ⋅ u = 𝟭"
assumes um: "u ∈ M"
assumes vm: "v ∈ M"
assumes v'm: "v' ∈ M"
shows "v = v'"
proof -
have ‹v = v ⋅ 𝟭› using right_unit[OF vm, symmetric] .
also have ‹... = v ⋅ (u ⋅ v')› unfolding uv1 ..
also have ‹... = v ⋅ u ⋅ v'› using associative[OF vm um v'm, symmetric] .
also have ‹... = 𝟭 ⋅ v'› unfolding vu1 ..
finally show ?thesis unfolding left_unit[OF v'm] .
qed
```

Now that we know the inverse is unique, we can use `THE`

to define an inverse function

```
text ‹p 31, l 7›
definition inverse where "inverse = (λu ∈ M. THE v. v ∈ M ∧ u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭)"
```

The keyword `THE`

is a sister of Hilbert’s epsilon operator `SOME`

(2.12.5.3)
Notice that this definition requires both `u ⋅ v = 𝟭`

and `v ⋅ u = 𝟭`

.
If only `u ⋅ v = 𝟭`

holds then
`v`

is the right inverse of `u`

.
If only `v ⋅ u =𝟭`

holds then
`v`

is the left inverse of `u`

.
If `v`

is both left and right inverse then `v`

is THE `inverse`

of `u`

.

If inverse does not exist then it is `undefined`

```
text ‹p 31, l 7›
lemma inverse_undefined [intro, simp]:
"u ∉ M ⟹ inverse u = undefined"
by (simp add: inverse_def)
```

If it does exist then it is guaranteed belong to `M`

```
text ‹p 31, l 7›
lemma invertible_inverse_closed [intro, simp]:
"⟦ invertible u; u ∈ M ⟧ ⟹ inverse u ∈ M"
using inverse_equality by auto
```

Clearly the inverse of neutral element is the element itself

```
text ‹p 31, l 7›
lemma inverse_unit [simp]: "inverse 𝟭 = 𝟭"
using inverse_equality by blast
```

The inverse of an inverse returns back the same element

```
text ‹p 31, l 8›
theorem invertible_inverse_inverse [simp]:
"⟦ invertible u; u ∈ M ⟧ ⟹ inverse (inverse u) = u"
by (simp add: inverse_equality)
```

The inverses are preserved in submonoids

```
context submonoid begin
text ‹p 31, l 7›
lemma submonoid_invertible [intro, simp]:
"⟦ sub.invertible u; u ∈ N ⟧ ⟹ invertible u"
using invertibleI by blast
text ‹p 31, l 7›
lemma submonoid_inverse_closed [intro, simp]:
"⟦ sub.invertible u; u ∈ N ⟧ ⟹ inverse u ∈ N"
using inverse_equality by auto
```

The `sub.invertible u`

refers to `u`

being invertible in the submonoid `N`

,
while `invertible u`

refers to `u`

being invertible in the original monoid `M`

. The `sub`

itself refers to the
##
label we gave before in the `sublocale`

command.

```
context submonoid begin
text ‹p 29,ll 32--33›
sublocale sub: monoid N "(⋅)" 𝟭
by unfold_locales (auto simp: sub_composition_closed sub_unit_closed)
end
```

It says that any function or predicate (like `invertible`

) defined in `monoid`

can be applied to `submonoid`

.
`⟦invertible u; u ∈ N ⟧ ⟹ sub.invertible u`

is not true.
## Counterexample

As a counterexample take the monoid`M`

of integers `int set`

(…`-2`

,`-1`

,`0`

,`1`

,`2`

…) with `+`

operation and `0`

neutral element
together with submonoid `N`

consisting of non-negative numbers (`0`

,`1`

,`2`

…). Then each positive number is `invertible`

in the original `M`

but not `sub.invertible`

in `N`

.
## 4.4 Groups

If all elements are invertible (the inverse always exists) then we call such monoid a *group*

```
text ‹Def 1.2›
text ‹p 31, ll 9--10›
locale group =
monoid G "(⋅)" 𝟭 for G and composition (infixl "⋅" 70) and unit ("𝟭") +
assumes invertible [simp, intro]: "u ∈ G ⟹ invertible u"
```

Subgroups are submonoids of groups whose inverse elements belong to that submonoid.

```
text ‹p 31, ll 11--12›
locale subgroup = submonoid G M "(⋅)" 𝟭 + sub: group G "(⋅)" 𝟭
for G and M and composition (infixl "⋅" 70) and unit ("𝟭")
begin
text ‹Reasoning about @{term invertible} and @{term inverse} in subgroups.›
text ‹p 31, ll 11--12›
lemma subgroup_inverse_equality [simp]:
"u ∈ G ⟹ inverse u = sub.inverse u"
by (simp add: inverse_equality)
text ‹p 31, ll 11--12›
lemma subgroup_inverse_iff [simp]:
"⟦ invertible x; x ∈ M ⟧ ⟹ inverse x ∈ G ⟷ x ∈ G"
using invertible_inverse_inverse sub.invertible_inverse_closed by fastforce
end (* subgroup *)
```

In other words, subgroups are subsets of groups that are groups themselves and contain the neutral element.

For example `int`

integers are group under addition `+`

and `0`

is the neutral element. Every integer `i`

has an inverse element `-i`

. An example of subgroup are the even integers `...,-4, -2, 0, 2, 4,...`

but the odd integers are not a subgroup because they do not contain a neutral element nor are closed under addition (sum of two odd numbers gives an even number). Natural numbers `nat`

are not a group because `-i`

is not a `nat`

for any `i`

except `0`

.
Lists `'a list`

are a monoid under append `@`

operation but not a group.

Just like for submonoids, being a subgroup is a transitive relation

```
lemma subgroup_transitive [trans]:
assumes "subgroup K H composition unit"
and "subgroup H G composition unit"
shows "subgroup K G composition unit"
proof -
interpret K: subgroup K H composition unit by fact
interpret H: subgroup H G composition unit by fact
show ?thesis by unfold_locales auto
qed
```

To know whether some set `G`

is a subgroup of some group `M`

it is enough to check whether the neutral element belongs to `G`

, the group operation is closed `g ⋅ h ∈ G`

in `G`

and all
elements have their inverses in `G`

.

```
text ‹Jacobson states both directions, but the other one is trivial.›
text ‹p 31, ll 12--15›
theorem subgroupI:
fixes G
assumes subset [THEN subsetD, intro]: "G ⊆ M"
and [intro]: "𝟭 ∈ G"
and [intro]: "⋀g h. ⟦ g ∈ G; h ∈ G ⟧ ⟹ g ⋅ h ∈ G"
and [intro]: "⋀g. g ∈ G ⟹ invertible g"
and [intro]: "⋀g. g ∈ G ⟹ inverse g ∈ G"
shows "subgroup G M (⋅) 𝟭"
proof -
interpret sub: monoid G "(⋅)" 𝟭 by unfold_locales auto
show ?thesis
proof unfold_locales
fix u assume [intro]: "u ∈ G" show "sub.invertible u"
using invertible_left_inverse invertible_right_inverse by blast
qed auto
qed
```

The set of all invertible element of some monoid `M`

```
text ‹p 31, l 16›
definition "Units = {u ∈ M. invertible u}"
```

forms a subgroup

```
text ‹p 31, ll 16--21›
interpretation units: subgroup Units M
proof (rule subgroupI)
fix u1 u2
assume Units [THEN mem_UnitsD, simp]: "u1 ∈ Units" "u2 ∈ Units"
have "(u1 ⋅ u2) ⋅ (inverse u2 ⋅ inverse u1) = (u1 ⋅ (u2 ⋅ inverse u2)) ⋅ inverse u1"
by (simp add: associative del: invertible_left_inverse invertible_right_inverse)
also have "… = 𝟭" by simp
finally have inv1: "(u1 ⋅ u2) ⋅ (inverse u2 ⋅ inverse u1) = 𝟭" by simp ― ‹ll 16--18›
have "(inverse u2 ⋅ inverse u1) ⋅ (u1 ⋅ u2) = (inverse u2 ⋅ (inverse u1 ⋅ u1)) ⋅ u2"
by (simp add: associative del: invertible_left_inverse invertible_right_inverse)
also have "… = 𝟭" by simp
finally have inv2: "(inverse u2 ⋅ inverse u1) ⋅ (u1 ⋅ u2) = 𝟭" by simp ― ‹l 9, ``and similarly''›
show "u1 ⋅ u2 ∈ Units" using inv1 inv2 invertibleI mem_UnitsI by auto
qed (auto simp: Units_def)
```

Composition of inverses is an inverse of compositions

```
text ‹p 31, l 22›
lemma inverse_composition_commute:
assumes [simp]: "invertible x" "invertible y" "x ∈ M" "y ∈ M"
shows "inverse (x ⋅ y) = inverse y ⋅ inverse x"
proof -
have "inverse (x ⋅ y) ⋅ (x ⋅ y) = (inverse y ⋅ inverse x) ⋅ (x ⋅ y)"
by (simp add: invertible_left_inverse2 associative)
then show ?thesis by (simp del: invertible_left_inverse)
qed
```

### 4.4.1 Transformations

Let’s consider the example monoid of transformations.
A function `α`

from `S`

to `S`

has an inverse *α ^{-1}* if

*α(α*and

^{-1}(s))=s*α*holds for all

^{-1}(α(s))=s`s ∈ S`

. Such α^{-1}can exist only if α is a bijection (2.12.5.3).

```
context transformations begin
text ‹p 31, ll 25--26›
theorem invertible_is_bijective:
assumes dom: "α ∈ S →⇩E S"
shows "invertible α ⟷ bij_betw α S S"
proof -
from dom interpret map α S S by unfold_locales
show ?thesis by (auto simp add: bij_betw_iff_has_inverse invertible_def)
qed
```

Therefore, the set of bijective functions forms a group

```
text ‹p 31, ll 26--27›
theorem Units_bijective:
"Units = {α ∈ S →⇩E S. bij_betw α S S}"
unfolding Units_def by (auto simp add: invertible_is_bijective)
```

This group has very special properties and occurs in many places. Mathematicians gave it
a special name and call this set the *symmetric group*. When the domain `S`

is finite and has
`n`

elements then the standard notation for this group is * S_{n}* (The bold

**S**stands for “symmetric”. The fact that domain is denoted by

`S`

is purely coincidental).```
text ‹p 31, ll 28--29›
abbreviation "Sym ≡ Units"
text ‹p 31, ll 26--28›
sublocale symmetric: group "Sym" "compose S" "identity S"
by (fact group_of_Units)
end (* transformations *)
```

Subgroups `G`

of a symmetric group `Sym`

(over domain `S`

) are an
important object in the Cayley theorem, therefore,
we create a dedicated locale just for them

```
text ‹p 32, ll 18--19›
locale transformation_group =
transformations S + symmetric: subgroup G Sym "compose S" "identity S" for G and S
begin
```

## Some simple properties of transformation group.

```
text ‹p 32, ll 18--19›
lemma transformation_group_closed [intro, simp]:
"⟦ α ∈ G; x ∈ S ⟧ ⟹ α x ∈ S"
using bij_betwE by blast
text ‹p 32, ll 18--19›
lemma transformation_group_undefined [intro, simp]:
"⟦ α ∈ G; x ∉ S ⟧ ⟹ α x = undefined"
by (metis compose_def symmetric.sub.right_unit restrict_apply)
end (* transformation_group *)
```

## 4.5 Homomorphisms

We intuitively know that there is a certain correspondence between natural numbers `nat`

and
length of list `'a list`

. Consider appending two lists `A @ B = C`

, for example

`value "[1,4,3] @ [6,8,3]::nat list " (* yields "[1, 4, 3, 6, 8, 3]" *)`

In order to know the length of `C`

it is enough to know the length of `A`

and `B`

and add the two numbers together.
We can write this as

`value "length ([1,4,3] @ [6,8,3::nat]) = length ([1,4,3::nat]) + length([6,8,3::nat])"`

In computer programming, such correspondences between various objects are very common and we can take advantage of them to optimize the code (for example, in C we could preallocate an array of the right length before concatenating two other arrays using memcpy)

Some other examples are

```
definition b2n :: "bool ⇒ nat" where
"b2n b = (if b then 1 else 0)"
(* nat is a monoid under max operation *)
value "b2n(True ∨ False) = max (b2n True) (b2n False)"
(* nat is a monoid under min operation *)
value "b2n(True ∧ False) = min (b2n True) (b2n False)"
(* int is a monoid under both min and max operation *)
value "max (abs (-4)::int) (abs (-5)::int) = abs (min (-4) (-5)::int)"
```

We can see a common pattern emerging among all of those examples. There is some function `f`

that translates elements of one monoid into another and it distributes over the monoid operations
`f(a * b) = f(a) + f(b)`

.
This leads us to the definition of monoid morphism.

```
locale monoid_morphism =
map η M M'+ source: monoid M "(⋅)" 𝟭 + target: monoid M' "(⋅')" "𝟭'"
for η and M and composition (infixl "⋅" 70) and unit ("𝟭")
and M' and composition' (infixl "⋅''" 70) and unit' ("𝟭''") +
assumes commutes_with_composition: "⟦ x ∈ M; y ∈ M ⟧ ⟹ η x ⋅' η y = η (x ⋅ y)"
begin
text ‹p 58, l 33; p 59, ll 1--2›
notation source.invertible ("invertible _" [100] 100)
notation source.inverse ("inverse _" [100] 100)
notation target.invertible ("invertible'' _" [100] 100)
notation target.inverse ("inverse'' _" [100] 100)
end (* monoid_homomorphism *)
```

In other words, morphism `η`

is a `map η M M'`

(see 3.1) from monoid `M`

to monoid `M'`

such that `η x ⋅' η y = η (x ⋅ y)`

holds.

**Important note!** The term “morphism” is not typically encountered in abstract algebra textbooks.
I borrowed this term from category theory, where its definition is different and more general than ours.
The reason why we need `monoid_morphism`

is because there are certain intricate details
in the definition of isomorphism (which we are yet to introduce)
that a typical mathematician can state informally but in Isabelle we have to be much more rigorous.

Monoid *homomorphism* is a special case of morphism such that `η x ⋅' η y = η (x ⋅ y)`

holds **and** the neutral element 𝟭 (from monoid `M`

) is mapped to
the neutral element `η 𝟭 = 𝟭'`

(in monoid `M'`

).

```
text ‹Def 1.6›
text ‹p 58, l 33; p 59, ll 1--2›
locale monoid_homomorphism = monoid_morphism η M "(⋅)" 𝟭 M' "(⋅')" "𝟭'"
for η and M and composition (infixl "⋅" 70) and unit ("𝟭")
and M' and composition' (infixl "⋅''" 70) and unit' ("𝟭''") +
assumes commutes_with_unit: "η 𝟭 = 𝟭'"
```

A `monoid_homomorphism`

can be surjective or injective, analogically as it was defined for `map`

.
When the homomorphism is surjective we call it an epimorphism. When it’s injective, it’s called monomorphism.

```
text ‹p 59, ll 29--30›
locale monoid_epimorphism = monoid_homomorphism + surjective_map η M M'
text ‹p 59, l 30›
locale monoid_monomorphism = monoid_homomorphism + injective_map η M M'
```

### 4.5.1 Isomorphisms

When a homomorphism is both surjective and injective then it is bijective. Such homomorphism
is called an isomorphism. However, this is where Isabelle departs from informal mathematics.
We will not define isomorphism as `monoid_homomorphism + bijective_map η M M'`

because a much simpler and more elegant definition is as follows

`locale monoid_isomorphism = bijective_map η M M' + monoid_morphism`

This definition does not assume `commutes_with_unit`

axiom because it follows from
`commutes_with_composition`

and `bijective`

axioms.

```
context monoid_isomorphism begin
theorem commutes_with_unit: "η 𝟭 = 𝟭'"
proof -
{
fix y assume "y ∈ M'"
then obtain x where nxy:"η x = y" "x ∈ M" by (metis image_iff surjective)
then have "η x ⋅' η 𝟭 = η x" using commutes_with_composition by auto
then have "y ⋅' η 𝟭 = y" using nxy by auto
}
then show "η 𝟭 = 𝟭'" by fastforce
qed
```

## Proof explanation.

The proof is very readable if you know that the curly braces`{ }`

are used to state a sub-theorem that fixes `"y ∈ M'"`

and shows `"y ⋅' η 𝟭 = y"`

. Therefore
the curly braces are to be understood as a lemma *for all*. And then from this sub-theorem the final result

`y ∈ M'`

we have `y ⋅' η 𝟭 = y`

`η 𝟭 = 𝟭'`

follows. The `fastforce`

is one of many automated theorem solvers that Isabelle has to offer.
Every isomorphism is a homomorphism.

```
sublocale hom: monoid_homomorphism η M "(⋅)" 𝟭 M' "(⋅')" "𝟭'"
by(unfold_locales, rule commutes_with_unit)
end (* monoid_isomorphism *)
```

An isomorphism is also an epimorphism and monomorphism.

```
text ‹p 59, ll 30--31›
sublocale monoid_isomorphism ⊆ monoid_epimorphism
by unfold_locales (auto simp: commutes_with_composition commutes_with_unit)
text ‹p 59, ll 30--31›
sublocale monoid_isomorphism ⊆ monoid_monomorphism
by unfold_locales (auto simp: commutes_with_composition commutes_with_unit)
```

Isomorphisms allow us to treat two monoids as if they were the same.
This has many implications in computer science. For example instead of multiplying two
real numbers `a*b`

we can add their logarithms `log (a * b) = log a + log b`

.
This isomorphism is used a lot in statistics and machine learning. It allows for
more stable, accurate and faster computation of small probabilities. It is also the basis for
variational inference
which lead to predictive coding
and has been proposed as a model of information processing in the real brain.

Suppose there are two monoids `ℳ`

and `ℳ'`

such that
`(M, composition, unit) = ℳ`

`(M', composition', unit') = ℳ'`

(recall that monoid is a triple 4.2).
Then we say that the two monoids are isomorphic `ℳ ≅⇩M ℳ'`

if there exists some isomorphism `η`

between them.

```
text ‹p 37, l 10›
definition isomorphic_as_monoids (infixl "≅⇩M" 50)
where "ℳ ≅⇩M ℳ' ⟷ (let (M, composition, unit) = ℳ; (M', composition', unit') = ℳ' in
(∃η. monoid_isomorphism η M composition unit M' composition' unit'))"
```

It doesn’t matter whether the isomorphism `η`

is from `M`

to `M'`

or from `M'`

to `M`

.
The following theorem states that the inverse η^{-1} (written as `restrict (inv_into M η) M'`

)
is also an isomorphism.

```
context monoid_isomorphism begin
text ‹p 37, ll 30--33›
theorem inverse_monoid_isomorphism:
"monoid_isomorphism (restrict (inv_into M η) M') M' (⋅') 𝟭' M (⋅) 𝟭"
using commutes_with_composition commutes_with_unit surjective
by unfold_locales auto
end (* monoid_isomorphism *)
```

Therefore if `ℳ`

is isomorphic to `ℳ'`

then `ℳ'`

is isomorphic to `ℳ`

.

```
text ‹p 37, ll 28--29›
theorem isomorphic_as_monoids_symmetric:
"(M, composition, unit) ≅⇩M (M', composition', unit') ⟹ (M', composition', unit') ≅⇩M (M, composition, unit)"
by (simp add: isomorphic_as_monoids_def) (meson monoid_isomorphism.inverse_monoid_isomorphism)
```

This already gives us a hint that `≅⇩M`

may be an equivalence relation (3.2).

## 4.6 Rings

Everything we studied before was some set `M`

equipped with only one operation `⋅`

.
We called this operation simply “composition”. Now we are going one step further
and consider sets with two operations `+`

and `⋅`

. Calling both of them
“composition” would be confusing, therefore, we will instead refer to `+`

as “additive” operation and `⋅`

as “multiplicative” operation
(or “addition” and “multiplication” for short).

For example numbers can be added and multiplied as usual. Another more interesting example
as sets which can be added by taking their union (`A∪B`

as `A+B`

) and multiplied by taking their Cartesian product
(`A×B`

as `A⋅B`

). Another example are polynomials and formal power serie. An example related to statistics and machine learning
are probabilities whose addition `p(A)+p(B) = p(A∨B)`

gives us the probabilitiy of either `A`

or `B`

happening, whereas multiplication `p(A)⋅p(B) = p(A∧B)`

is the probability of both `A`

and `B`

events occurring (assuming they are independent).

```
text ‹Def 2.1›
text ‹p 86, ll 20--28›
locale ring = additive: abelian_group R "(+)" 𝟬 + multiplicative: monoid R "(⋅)" 𝟭
for R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭") +
assumes distributive: "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ a ⋅ (b + c) = a ⋅ b + a ⋅ c"
"⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ (b + c) ⋅ a = b ⋅ a + c ⋅ a"
begin
text ‹p 86, ll 20--28›
notation additive.inverse ("- _" [66] 65)
abbreviation subtraction (infixl "-" 65) where "a - b ≡ a + (- b)" (* or, alternatively, a definition *)
end (* ring *)
```