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

and that even numbers form a submonoid.

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.

Note that the reverse implication ⟦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 α(α^-1(s))=s and α^-1(α(s))=s holds for all 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 y ∈ M' we have y ⋅' η 𝟭 = y. And then from this sub-theorem the final result η 𝟭 = 𝟭' 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.5.2 Translations

TODO

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

4.7 Fields

TODO