# Theory Set_Theory

(*
Copyright (c) 2014-2019 by Clemens Ballarin
*)

theory Set_Theory imports "HOL-Library.FuncSet" begin

hide_const map
hide_const partition

no_notation divide (infixl "'/" 70)
no_notation inverse_divide (infixl "'/" 70)

text ‹
Each statement in the formal text is annotated with the location of the originating statement
in Jacobson's text @{cite Jacobson1985}.  Each fact that Jacobson states explicitly is marked
as @{command theorem} unless it is translated to a @{command sublocale} declaration.
Literal quotations from Jacobson's text are reproduced in double quotes.

Auxiliary results needed for the formalisation that cannot be found in Jacobson's text are marked
as @{command lemma} or are @{command interpretation}s.  Such results are annotated with the
location of a related statement.  For example, the introduction rule of a constant is annotated
with the location of the definition of the corresponding operation.
›

section ‹Concepts from Set Theory.  The Integers›

subsection ‹The Cartesian Product Set.  Maps›

text ‹Maps as extensional HOL functions›
text ‹p 5, ll 21--25›
locale map =
fixes α and S and T
assumes graph [intro, simp]: "α ∈ S →⇩E T"
begin

text ‹p 5, ll 21--25›
lemma map_closed [intro, simp]:
"a ∈ S ⟹ α a ∈ T"
using graph by fast

text ‹p 5, ll 21--25›
lemma map_undefined [intro]:
"a ∉ S ⟹ α a = undefined"
using graph by fast

end (* map *)

text ‹p 7, ll 7--8›
locale surjective_map = map + assumes surjective [intro]: "α  S = T"

text ‹p 7, ll 8--9›
locale injective_map = map + assumes injective [intro, simp]: "inj_on α S"

text ‹Enables locale reasoning about the inverse @{term "restrict (inv_into S α) T"} of @{term α}.›
text ‹p 7, ll 9--10›
locale bijective =
fixes α and S and T
assumes bijective [intro, simp]: "bij_betw α S T"

text ‹
Exploit existing knowledge about @{term bij_betw} rather than extending @{locale surjective_map}
and @{locale injective_map}.
›
text ‹p 7, ll 9--10›
locale bijective_map = map + bijective begin

text ‹p 7, ll 9--10›
sublocale surjective_map by unfold_locales (simp add: bij_betw_imp_surj_on)

text ‹p 7, ll 9--10›
sublocale injective_map using bij_betw_def by unfold_locales fast

text ‹p 9, ll 12--13›
sublocale inverse: map "restrict (inv_into S α) T" T S
by unfold_locales (simp add: inv_into_into surjective)

text ‹p 9, ll 12--13›
sublocale inverse: bijective "restrict (inv_into S α) T" T S
by unfold_locales (simp add: bij_betw_inv_into surjective)

end (* bijective_map *)

text ‹p 8, ll 14--15›
abbreviation "identity S ≡ (λx ∈ S. x)"

context map begin

text ‹p 8, ll 18--20; p 9, ll 1--8›
theorem bij_betw_iff_has_inverse:
"bij_betw α S T ⟷ (∃β ∈ T →⇩E S. compose S β α = identity S ∧ compose T α β = identity T)"
(is "_ ⟷ (∃β ∈ T →⇩E S. ?INV β)")
proof
let ?inv = "restrict (inv_into S α) T"
assume "bij_betw α S T"
then have "?INV ?inv" and "?inv ∈ T →⇩E S"
by (simp_all add: compose_inv_into_id bij_betw_imp_surj_on compose_id_inv_into bij_betw_imp_funcset bij_betw_inv_into)
then show "∃β ∈ T →⇩E S. ?INV β" ..
next
assume "∃β ∈ T →⇩E S. ?INV β"
then obtain β where "α ∈ S → T" "β ∈ T → S" "⋀x. x ∈ S ⟹ β (α x) = x" "⋀y. y ∈ T ⟹ α (β y) = y"
by (metis PiE_restrict compose_eq graph restrict_PiE restrict_apply)
then show "bij_betw α S T" by (rule bij_betwI)
qed

end (* map *)

subsection ‹Equivalence Relations.  Factoring a Map Through an Equivalence Relation›

text ‹p 11, ll 6--11›
locale equivalence =
fixes S and E
assumes closed [intro, simp]: "E ⊆ S × S"
and reflexive [intro, simp]: "a ∈ S ⟹ (a, a) ∈ E"
and symmetric [sym]: "(a, b) ∈ E ⟹ (b, a) ∈ E"
and transitive [trans]: "⟦ (a, b) ∈ E; (b, c) ∈ E ⟧ ⟹ (a, c) ∈ E"
begin

text ‹p 11, ll 6--11›
lemma left_closed [intro]: (* inefficient as a simp rule *)
"(a, b) ∈ E ⟹ a ∈ S"
using closed by blast

text ‹p 11, ll 6--11›
lemma right_closed [intro]: (* inefficient as a simp rule *)
"(a, b) ∈ E ⟹ b ∈ S"
using closed by blast

end (* equivalence *)

text ‹p 11, ll 16--20›
locale partition =
fixes S and P
assumes subset: "P ⊆ Pow S"
and non_vacuous: "{} ∉ P"
and complete: "⋃P = S"
and disjoint: "⟦ A ∈ P; B ∈ P; A ≠ B ⟧ ⟹ A ∩ B = {}"

context equivalence begin

text ‹p 11, ll 24--26›
definition "Class = (λa ∈ S. {b ∈ S. (b, a) ∈ E})"

text ‹p 11, ll 24--26›
lemma Class_closed [dest]:
"⟦ a ∈ Class b; b ∈ S ⟧ ⟹ a ∈ S"
unfolding Class_def by auto

text ‹p 11, ll 24--26›
lemma Class_closed2 [intro, simp]:
"a ∈ S ⟹ Class a ⊆ S"
unfolding Class_def by auto

text ‹p 11, ll 24--26›
lemma Class_undefined [intro, simp]:
"a ∉ S ⟹ Class a = undefined"
unfolding Class_def by simp

text ‹p 11, ll 24--26›
lemma ClassI [intro, simp]:
"(a, b) ∈ E ⟹ a ∈ Class b"
unfolding Class_def by (simp add: left_closed right_closed)

text ‹p 11, ll 24--26›
lemma Class_revI [intro, simp]:
"(a, b) ∈ E ⟹ b ∈ Class a"
by (blast intro: symmetric)

text ‹p 11, ll 24--26›
lemma ClassD [dest]:
"⟦ b ∈ Class a; a ∈ S ⟧ ⟹ (b, a) ∈ E"
unfolding Class_def by simp

text ‹p 11, ll 30--31›
theorem Class_self [intro, simp]:
"a ∈ S ⟹ a ∈ Class a"
unfolding Class_def by simp

text ‹p 11, l 31; p 12, l 1›
theorem Class_Union [simp]:
"(⋃a∈S. Class a) = S"
by blast

text ‹p 11, ll 2--3›
theorem Class_subset:
"(a, b) ∈ E ⟹ Class a ⊆ Class b"
proof
fix a and b and c
assume "(a, b) ∈ E" and "c ∈ Class a"
then have "(c, a) ∈ E" by auto
also note ‹(a, b) ∈ E›
finally have "(c, b) ∈ E" by simp
then show "c ∈ Class b" by auto
qed

text ‹p 11, ll 3--4›
theorem Class_eq:
"(a, b) ∈ E ⟹ Class a = Class b"
by (auto intro!: Class_subset intro: symmetric)

text ‹p 12, ll 1--5›
theorem Class_equivalence:
"⟦ a ∈ S; b ∈ S ⟧ ⟹ Class a = Class b ⟷ (a, b) ∈ E"
proof
fix a and b
assume "a ∈ S" "b ∈ S" "Class a = Class b"
then have "a ∈ Class a" by auto
also note ‹Class a = Class b›
finally show "(a, b) ∈ E" by (fast intro: ‹b ∈ S›)
qed (rule Class_eq)

text ‹p 12, ll 5--7›
theorem not_disjoint_implies_equal:
assumes not_disjoint: "Class a ∩ Class b ≠ {}"
assumes closed: "a ∈ S" "b ∈ S"
shows "Class a = Class b"
proof -
from not_disjoint and closed obtain c where witness: "c ∈ Class a ∩ Class b" by fast
with closed have "(a, c) ∈ E" by (blast intro: symmetric)
also from witness and closed have "(c, b) ∈ E" by fast
finally show ?thesis by (rule Class_eq)
qed

text ‹p 12, ll 7--8›
definition "Partition = Class  S"

text ‹p 12, ll 7--8›
lemma Class_in_Partition [intro, simp]:
"a ∈ S ⟹ Class a ∈ Partition"
unfolding Partition_def by fast

text ‹p 12, ll 7--8›
theorem partition:
"partition S Partition"
proof
fix A and B
assume closed: "A ∈ Partition" "B ∈ Partition"
then obtain a and b where eq: "A = Class a" "B = Class b" and ab: "a ∈ S" "b ∈ S"
unfolding Partition_def by auto
assume distinct: "A ≠ B"
then show "A ∩ B = {}"
proof (rule contrapos_np)
assume not_disjoint: "A ∩ B ≠ {}"
then show "A = B" by (simp add: eq) (metis not_disjoint_implies_equal ab)
qed
qed (auto simp: Partition_def)

end (* equivalence *)

context partition begin

text ‹p 12, ll 9--10›
theorem block_exists:
"a ∈ S ⟹ ∃A. a ∈ A ∧ A ∈ P"
using complete by blast

text ‹p 12, ll 9--10›
theorem block_unique:
"⟦ a ∈ A; A ∈ P; a ∈ B; B ∈ P ⟧ ⟹ A = B"
using disjoint by blast

text ‹p 12, ll 9--10›
lemma block_closed [intro]: (* inefficient as a simp rule *)
"⟦ a ∈ A; A ∈ P ⟧ ⟹ a ∈ S"
using complete by blast

text ‹p 12, ll 9--10›
lemma element_exists:
"A ∈ P ⟹ ∃a ∈ S. a ∈ A"
by (metis non_vacuous block_closed all_not_in_conv)

text ‹p 12, ll 9--10›
definition "Block = (λa ∈ S. THE A. a ∈ A ∧ A ∈ P)"

text ‹p 12, ll 9--10›
lemma Block_closed [intro, simp]:
assumes [intro]: "a ∈ S" shows "Block a ∈ P"
proof -
obtain A where "a ∈ A" "A ∈ P" using block_exists by blast
then show ?thesis
apply (auto simp: Block_def)
apply (rule theI2)
apply (auto dest: block_unique)
done
qed

text ‹p 12, ll 9--10›
lemma Block_undefined [intro, simp]:
"a ∉ S ⟹ Block a = undefined"
unfolding Block_def by simp

text ‹p 12, ll 9--10›
lemma Block_self:
"⟦ a ∈ A; A ∈ P ⟧ ⟹ Block a = A"
apply (rule the_equality)
apply (auto dest: block_unique)
done

text ‹p 12, ll 10--11›
definition "Equivalence = {(a, b) . ∃A ∈ P. a ∈ A ∧ b ∈ A}"

text ‹p 12, ll 11--12›
theorem equivalence: "equivalence S Equivalence"
proof
show "Equivalence ⊆ S × S" unfolding Equivalence_def using subset by auto
next
fix a
assume "a ∈ S"
then show "(a, a) ∈ Equivalence" unfolding Equivalence_def using complete by auto
next
fix a and b
assume "(a, b) ∈ Equivalence"
then show "(b, a) ∈ Equivalence" unfolding Equivalence_def by auto
next
fix a and b and c
assume "(a, b) ∈ Equivalence" "(b, c) ∈ Equivalence"
then show "(a, c) ∈ Equivalence" unfolding Equivalence_def using disjoint by auto
qed

text ‹Temporarily introduce equivalence associated to partition.›
text ‹p 12, ll 12--14›
interpretation equivalence S Equivalence by (rule equivalence)

text ‹p 12, ll 12--14›
theorem Class_is_Block:
assumes "a ∈ S" shows "Class a = Block a"
proof -
from ‹a ∈ S› and block_exists obtain A where block: "a ∈ A ∧ A ∈ P" by blast
show ?thesis
apply (rule theI2)
apply (rule block)
apply (metis block block_unique)
apply (auto dest: block_unique simp: Equivalence_def)
done
qed

text ‹p 12, l 14›
lemma Class_equals_Block:
"Class = Block"
proof
fix x show "Class x = Block x"
by (cases "x ∈ S") (auto simp: Class_is_Block)
qed

text ‹p 12, l 14›
theorem partition_of_equivalence:
"Partition = P"
by (auto simp add: Partition_def Class_equals_Block image_iff) (metis Block_self element_exists)

end (* partition *)

context equivalence begin

text ‹p 12, ll 14--17›
interpretation partition S Partition by (rule partition)

text ‹p 12, ll 14--17›
theorem equivalence_of_partition:
"Equivalence = E"
unfolding Equivalence_def unfolding Partition_def by auto (metis ClassD Class_closed Class_eq)

end (* equivalence *)

text ‹p 12, l 14›
sublocale partition ⊆ equivalence S Equivalence
rewrites "equivalence.Partition S Equivalence = P" and "equivalence.Class S Equivalence = Block"
apply (rule equivalence)
apply (rule partition_of_equivalence)
apply (rule Class_equals_Block)
done

text ‹p 12, ll 14--17›
sublocale equivalence ⊆ partition S Partition
rewrites "partition.Equivalence Partition = E" and "partition.Block S Partition = Class"
apply (rule partition)
apply (rule equivalence_of_partition)
apply (metis equivalence_of_partition partition partition.Class_equals_Block)
done

text ‹Unfortunately only effective on input›
text ‹p 12, ll 18--20›
notation equivalence.Partition (infixl "'/" 75)

context equivalence begin

text ‹p 12, ll 18--20›
lemma representant_exists [dest]: "A ∈ S / E ⟹ ∃a∈S. a ∈ A ∧ A = Class a"
by (metis Block_self element_exists)

text ‹p 12, ll 18--20›
lemma quotient_ClassE: "A ∈ S / E ⟹ (⋀a. a ∈ S ⟹ P (Class a)) ⟹ P A"
using representant_exists by blast

end (* equivalence *)

text ‹p 12, ll 21--23›
sublocale equivalence ⊆ natural: surjective_map Class S "S / E"
by unfold_locales force+

text ‹Technical device to achieve Jacobson's syntax; context where @{text α} is not a parameter.›
text ‹p 12, ll 25--26›
locale fiber_relation_notation = fixes S :: "'a set" begin

text ‹p 12, ll 25--26›
definition Fiber_Relation ("E'(_')") where "Fiber_Relation α = {(x, y). x ∈ S ∧ y ∈ S ∧ α x = α y}"

end (* fiber_relation_notation *)

text ‹
Context where classes and the induced map are defined through the fiber relation.
This will be the case for monoid homomorphisms but not group homomorphisms.
›
text ‹Avoids infinite interpretation chain.›
text ‹p 12, ll 25--26›
locale fiber_relation = map begin

text ‹Install syntax›
text ‹p 12, ll 25--26›
sublocale fiber_relation_notation .

text ‹p 12, ll 26--27›
sublocale equivalence where E = "E(α)"
unfolding Fiber_Relation_def by unfold_locales auto

text ‹define $\bar{\alpha}$ by $\bar{\alpha}(\bar{a}) = \alpha(a)$''›
text ‹p 13, ll 8--9›
definition "induced = (λA ∈ S / E(α). THE b. ∃a ∈ A. b = α a)"

text ‹p 13, l 10›
theorem Fiber_equality:
"⟦ a ∈ S; b ∈ S ⟧ ⟹ Class a = Class b ⟷ α a = α b"
unfolding Class_equivalence unfolding Fiber_Relation_def by simp

text ‹p 13, ll 8--9›
theorem induced_Fiber_simp [simp]:
assumes [intro, simp]: "a ∈ S" shows "induced (Class a) = α a"
proof -
have "(THE b. ∃a∈Class a. b = α a) = α a"
by (rule the_equality) (auto simp: Fiber_equality [symmetric] Block_self block_closed)
then show ?thesis unfolding induced_def by simp
qed

text ‹p 13, ll 10--11›
interpretation induced: map induced "S / E(α)" T
proof (unfold_locales, rule)
fix A
assume [intro, simp]: "A ∈ S / E(α)"
obtain a where a: "a ∈ S" "a ∈ A" using element_exists by auto
have "(THE b. ∃a∈A. b = α a) ∈ T"
apply (rule theI2)
using a apply (auto simp: Fiber_equality [symmetric] Block_self block_closed)
done
then show "induced A ∈ T" unfolding induced_def by simp

text ‹p 13, ll 12--13›
sublocale induced: injective_map induced "S / E(α)" T
proof
show "inj_on induced Partition"
unfolding inj_on_def
by (metis Fiber_equality Block_self element_exists induced_Fiber_simp)
qed

text ‹p 13, ll 16--19›
theorem factorization_lemma:
"a ∈ S ⟹ compose S induced Class a = α a"

text ‹p 13, ll 16--19›
theorem factorization [simp]: "compose S induced Class = α"
by (rule ext) (simp add: compose_def map_undefined)

text ‹p 14, ll 2--4›
theorem uniqueness:
assumes map: "β ∈ S / E(α) →⇩E T"
and factorization: "compose S β Class = α"
shows "β = induced"
proof
fix A
show "β A = induced A"
proof (cases "A ∈ S / E(α)")
case True
then obtain a where [simp]: "A = Class a" "a ∈ S" by fast
then have "β (Class a) = α a" by (metis compose_eq factorization)
also have "… = induced (Class a)" by simp
finally show ?thesis by simp
qed (simp add: induced_def PiE_arb [OF map])
qed

end (* fiber_relation *)

end


# Theory Group_Theory

(*
Copyright (c) 2014-2019 by Clemens Ballarin
*)

theory Group_Theory imports Set_Theory begin

hide_const monoid
hide_const group
hide_const inverse

no_notation quotient (infixl "'/'/" 90)

section ‹Monoids and Groups›

subsection ‹Monoids of Transformations and Abstract Monoids›

text ‹Def 1.1›
text ‹p 28, ll 28--30›
locale monoid =
fixes M and composition (infixl "⋅" 70) and unit ("𝟭")
assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M"
and unit_closed [intro, simp]: "𝟭 ∈ M"
and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)"
and left_unit [intro, simp]: "a ∈ M ⟹ 𝟭 ⋅ a = a"
and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ 𝟭 = a"

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"
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 (* submonoid *)

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

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

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)

text ‹@{term N} is a monoid of transformations of the set @{term S}.›
text ‹p 29, ll 34--36›
locale transformation_monoid =
transformations S + submonoid M "S →⇩E S" "compose S" "identity S" for M and S
begin

text ‹p 29, ll 34--36›
lemma transformation_closed [intro, simp]:
"⟦ α ∈ M; x ∈ S ⟧ ⟹ α x ∈ S"
by (metis PiE_iff sub)

text ‹p 29, ll 34--36›
lemma transformation_undefined [intro, simp]:
"⟦ α ∈ M; x ∉ S ⟧ ⟹ α x = undefined"
by (metis PiE_arb sub)

end (* transformation_monoid *)

subsection ‹Groups of Transformations and Abstract Groups›

context monoid begin

text ‹Invertible elements›

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

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

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)

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

text ‹p 31, l 7›
theorem inverse_equality:
"⟦ u ⋅ v = 𝟭; v ⋅ u = 𝟭; u ∈ M; v ∈ M ⟧ ⟹ inverse u = v"
unfolding inverse_def using inverse_unique by simp blast

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

text ‹p 31, l 7›
lemma inverse_undefined [intro, simp]:
"u ∉ M ⟹ inverse u = undefined"

text ‹p 31, l 7›
lemma invertible_left_inverse [simp]:
"⟦ invertible u; u ∈ M ⟧ ⟹ inverse u ⋅ u = 𝟭"
using inverse_equality by auto

text ‹p 31, l 7›
lemma invertible_right_inverse [simp]:
"⟦ invertible u; u ∈ M ⟧ ⟹ u ⋅ inverse u = 𝟭"
using inverse_equality by auto

text ‹p 31, l 7›
lemma invertible_left_cancel [simp]:
"⟦ invertible x; x ∈ M; y ∈ M; z ∈ M ⟧ ⟹ x ⋅ y = x ⋅ z ⟷ y = z"
by (metis associative invertible_def left_unit)

text ‹p 31, l 7›
lemma invertible_right_cancel [simp]:
"⟦ invertible x; x ∈ M; y ∈ M; z ∈ M ⟧ ⟹ y ⋅ x = z ⋅ x ⟷ y = z"
by (metis associative invertible_def right_unit)

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

text ‹p 31, ll 7--8›
theorem invertible_inverse_invertible [intro, simp]:
"⟦ invertible u; u ∈ M ⟧ ⟹ invertible (inverse u)"
using invertible_left_inverse invertible_right_inverse by blast

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

end (* monoid *)

context submonoid begin

text ‹Reasoning about @{term invertible} and @{term inverse} in submonoids.›

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

end (* submonoid *)

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"

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"

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

text ‹p 31, ll 11--12›
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

context monoid begin

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

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

text ‹p 31, l 16›
lemma mem_UnitsI:
"⟦ invertible u; u ∈ M ⟧ ⟹ u ∈ Units"
unfolding Units_def by clarify

text ‹p 31, l 16›
lemma mem_UnitsD:
"⟦ u ∈ Units ⟧ ⟹ invertible u ∧ u ∈ M"
unfolding Units_def by clarify

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)

text ‹p 31, ll 21--22›
theorem group_of_Units [intro, simp]:
"group Units (⋅) 𝟭"
..

text ‹p 31, l 19›
lemma composition_invertible [simp, intro]:
"⟦ invertible x; invertible y; x ∈ M; y ∈ M ⟧ ⟹ invertible (x ⋅ y)"
using mem_UnitsD mem_UnitsI by blast

text ‹p 31, l 20›
lemma unit_invertible:
"invertible 𝟭"
by fast

text ‹Useful simplification rules›
text ‹p 31, l 22›
lemma invertible_right_inverse2:
"⟦ invertible u; u ∈ M; v ∈ M ⟧ ⟹ u ⋅ (inverse u ⋅ v) = v"
by (simp add: associative [THEN sym])

text ‹p 31, l 22›
lemma invertible_left_inverse2:
"⟦ invertible u; u ∈ M; v ∈ M ⟧ ⟹ inverse u ⋅ (u ⋅ v) = v"
by (simp add: associative [THEN sym])

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)"
then show ?thesis by (simp del: invertible_left_inverse)
qed

end (* monoid *)

text ‹p 31, l 24›
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

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)

text ‹p 31, ll 26--27›
lemma Units_bij_betwI [intro, simp]:
"α ∈ Units ⟹ bij_betw α S S"

text ‹p 31, ll 26--27›
lemma Units_bij_betwD [dest, simp]:
"⟦ α ∈ S →⇩E S; bij_betw α S S ⟧ ⟹ α ∈ Units"
unfolding Units_bijective by simp

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

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

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

subsection ‹Isomorphisms.  Cayley's Theorem›

text ‹Def 1.3›
text ‹p 37, ll 7--11›
locale monoid_isomorphism =
bijective_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)"
and commutes_with_unit: "η 𝟭 = 𝟭'"

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'))"

text ‹p 37, ll 11--12›
locale monoid_isomorphism' =
bijective_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)"

text ‹p 37, ll 11--12›
sublocale monoid_isomorphism ⊆ monoid_isomorphism'

text ‹Both definitions are equivalent.›
text ‹p 37, ll 12--15›
sublocale monoid_isomorphism' ⊆ monoid_isomorphism
proof unfold_locales
{
fix y assume "y ∈ M'"
then obtain x where "η x = y" "x ∈ M" by (metis image_iff surjective)
then have "y ⋅' η 𝟭 = y" using commutes_with_composition by auto
}
then show "η 𝟭 = 𝟭'" by fastforce

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

text ‹We only need that @{term η} is symmetric.›
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)

text ‹p 38, l 4›
locale left_translations_of_monoid = monoid begin

(*
We take the liberty of omitting "left_" from the name of the translation operation.  The derived
transformation monoid and group won't be qualified with "left" either.  This avoids qualifications
such as "left.left_...".  In contexts where left and right translations are used simultaneously,
notably subgroup_of_group, qualifiers are needed.
*)

text ‹p 38, ll 5--7›
definition translation ("'(_')⇩L") where "translation = (λa ∈ M. λx ∈ M. a ⋅ x)"

text ‹p 38, ll 5--7›
lemma translation_map [intro, simp]:
"a ∈ M ⟹ (a)⇩L ∈ M →⇩E M"
unfolding translation_def by simp

text ‹p 38, ll 5--7›
lemma Translations_maps [intro, simp]:
"translation  M ⊆ M →⇩E M"

text ‹p 38, ll 5--7›
lemma translation_apply:
"⟦ a ∈ M; b ∈ M ⟧ ⟹ (a)⇩L b = a ⋅ b"
unfolding translation_def by auto

text ‹p 38, ll 5--7›
lemma translation_exist:
"f ∈ translation  M ⟹ ∃a ∈ M. f = (a)⇩L"
by auto

text ‹p 38, ll 5--7›
lemmas Translations_E [elim] = translation_exist [THEN bexE]

text ‹p 38, l 10›
theorem translation_unit_eq [simp]:
"identity M = (𝟭)⇩L"
unfolding translation_def by auto

text ‹p 38, ll 10--11›
theorem translation_composition_eq [simp]:
assumes [simp]: "a ∈ M" "b ∈ M"
shows "compose M (a)⇩L (b)⇩L = (a ⋅ b)⇩L"
unfolding translation_def by rule (simp add: associative compose_def)

(* Activate @{locale monoid} to simplify subsequent proof. *)
text ‹p 38, ll 7--9›
sublocale transformation: transformations M .

text ‹p 38, ll 7--9›
theorem Translations_transformation_monoid:
"transformation_monoid (translation  M) M"
by unfold_locales auto

text ‹p 38, ll 7--9›
sublocale transformation: transformation_monoid "translation  M" M
by (fact Translations_transformation_monoid)

text ‹p 38, l 12›
sublocale map translation M "translation  M"

text ‹p 38, ll 12--16›
theorem translation_isomorphism [intro]:
"monoid_isomorphism translation M (⋅) 𝟭 (translation  M) (compose M) (identity M)"
proof unfold_locales
have "inj_on translation M"
proof (rule inj_onI)
fix a b
assume [simp]: "a ∈ M" "b ∈ M" "(a)⇩L = (b)⇩L"
have "(a)⇩L 𝟭 = (b)⇩L 𝟭" by simp
then show "a = b" by (simp add: translation_def)
qed
then show "bij_betw translation M (translation  M)"
qed simp_all

text ‹p 38, ll 12--16›
sublocale monoid_isomorphism translation M "(⋅)" 𝟭 "translation  M" "compose M" "identity M" ..

end (* left_translations_of_monoid *)

context monoid begin

text ‹p 38, ll 1--2›
interpretation left_translations_of_monoid ..

text ‹p 38, ll 1--2›
theorem cayley_monoid:
"∃M' composition' unit'. transformation_monoid M' M ∧ (M, (⋅), 𝟭) ≅⇩M (M', composition', unit')"
by (simp add: isomorphic_as_monoids_def) (fast intro: Translations_transformation_monoid)

end (* monoid *)

text ‹p 38, l 17›
locale left_translations_of_group = group begin

text ‹p 38, ll 17--18›
sublocale left_translations_of_monoid where M = G ..

text ‹p 38, ll 17--18›
notation translation ("'(_')⇩L")

text ‹
The group of left translations is a subgroup of the symmetric group,
hence @{term transformation.sub.invertible}.
›
text ‹p 38, ll 20--22›
theorem translation_invertible [intro, simp]:
assumes [simp]: "a ∈ G"
shows "transformation.sub.invertible (a)⇩L"
proof
show "compose G (a)⇩L (inverse a)⇩L = identity G" by simp
next
show "compose G (inverse a)⇩L (a)⇩L = identity G" by simp
qed auto

text ‹p 38, ll 19--20›
theorem translation_bijective [intro, simp]:
"a ∈ G ⟹ bij_betw (a)⇩L G G"
by (blast intro: transformation.invertible_is_bijective [THEN iffD1])

text ‹p 38, ll 18--20›
theorem Translations_transformation_group:
"transformation_group (translation  G) G"
proof unfold_locales
show "(translation  G) ⊆ transformation.Sym"
unfolding transformation.Units_bijective by auto
next
fix α
assume α: "α ∈ translation  G"
then obtain a where a: "a ∈ G" and eq: "α = (a)⇩L" ..
with translation_invertible show "transformation.sub.invertible α" by simp
qed auto

text ‹p 38, ll 18--20›
sublocale transformation: transformation_group "translation  G" G
by (fact Translations_transformation_group)

end (* left_translations_of_group *)

context group begin

text ‹p 38, ll 2--3›
interpretation left_translations_of_group ..

text ‹p 38, ll 2--3›
theorem cayley_group:
"∃G' composition' unit'. transformation_group G' G ∧ (G, (⋅), 𝟭) ≅⇩M (G', composition', unit')"
by (simp add: isomorphic_as_monoids_def) (fast intro: Translations_transformation_group)

end (* group *)

text ‹Exercise 3›

text ‹p 39, ll 9--10›
locale right_translations_of_group = group begin

text ‹p 39, ll 9--10›
definition translation ("'(_')⇩R") where "translation = (λa ∈ G. λx ∈ G. x ⋅ a)"

text ‹p 39, ll 9--10›
abbreviation "Translations ≡ translation  G"

text ‹The isomorphism that will be established is a map different from @{term translation}.›
text ‹p 39, ll 9--10›
interpretation aux: map translation G Translations

text ‹p 39, ll 9--10›
lemma translation_map [intro, simp]:
"a ∈ G ⟹ (a)⇩R ∈ G →⇩E G"
unfolding translation_def by simp

text ‹p 39, ll 9--10›
lemma Translation_maps [intro, simp]:
"Translations ⊆ G →⇩E G"

text ‹p 39, ll 9--10›
lemma translation_apply:
"⟦ a ∈ G; b ∈ G ⟧ ⟹ (a)⇩R b = b ⋅ a"
unfolding translation_def by auto

text ‹p 39, ll 9--10›
lemma translation_exist:
"f ∈ Translations ⟹ ∃a ∈ G. f = (a)⇩R"
by auto

text ‹p 39, ll 9--10›
lemmas Translations_E [elim] = translation_exist [THEN bexE]

text ‹p 39, ll 9--10›
lemma translation_unit_eq [simp]:
"identity G = (𝟭)⇩R"
unfolding translation_def by auto

text ‹p 39, ll 10--11›
lemma translation_composition_eq [simp]:
assumes [simp]: "a ∈ G" "b ∈ G"
shows "compose G (a)⇩R (b)⇩R = (b ⋅ a)⇩R"
unfolding translation_def by rule (simp add: associative compose_def)

text ‹p 39, ll 10--11›
sublocale transformation: transformations G .

text ‹p 39, ll 10--11›
lemma Translations_transformation_monoid:
"transformation_monoid Translations G"
by unfold_locales auto

text ‹p 39, ll 10--11›
sublocale transformation: transformation_monoid Translations G
by (fact Translations_transformation_monoid)

text ‹p 39, ll 10--11›
lemma translation_invertible [intro, simp]:
assumes [simp]: "a ∈ G"
shows "transformation.sub.invertible (a)⇩R"
proof
show "compose G (a)⇩R (inverse a)⇩R = identity G" by simp
next
show "compose G (inverse a)⇩R (a)⇩R = identity G" by simp
qed auto

text ‹p 39, ll 10--11›
lemma translation_bijective [intro, simp]:
"a ∈ G ⟹ bij_betw (a)⇩R G G"
by (blast intro: transformation.invertible_is_bijective [THEN iffD1])

text ‹p 39, ll 10--11›
theorem Translations_transformation_group:
"transformation_group Translations G"
proof unfold_locales
show "Translations ⊆ transformation.Sym"
unfolding transformation.Units_bijective by auto
next
fix α
assume α: "α ∈ Translations"
then obtain a where a: "a ∈ G" and eq: "α = (a)⇩R" ..
with translation_invertible show "transformation.sub.invertible α" by simp
qed auto

text ‹p 39, ll 10--11›
sublocale transformation: transformation_group Translations G
by (rule Translations_transformation_group)

text ‹p 39, ll 10--11›
lemma translation_inverse_eq [simp]:
assumes [simp]: "a ∈ G"
shows "transformation.sub.inverse (a)⇩R = (inverse a)⇩R"
proof (rule transformation.sub.inverse_equality)
show "compose G (a)⇩R (inverse a)⇩R = identity G" by simp
next
show "compose G (inverse a)⇩R (a)⇩R = identity G" by simp
qed auto

text ‹p 39, ll 10--11›
theorem translation_inverse_monoid_isomorphism [intro]:
"monoid_isomorphism (λa∈G. transformation.symmetric.inverse (a)⇩R) G (⋅) 𝟭 Translations (compose G) (identity G)"
(is "monoid_isomorphism ?inv _ _ _ _ _ _")
proof unfold_locales
show "?inv ∈ G →⇩E Translations" by (simp del: translation_unit_eq)
next
note bij_betw_compose [trans]
have "bij_betw inverse G G"
by (rule bij_betwI [where g = inverse]) auto
also have "bij_betw translation G Translations"
by (rule bij_betwI [where g = "λα∈Translations. α 𝟭"]) (auto simp: translation_apply)
finally show "bij_betw ?inv G Translations"
by (simp cong: bij_betw_cong add: compose_eq del: translation_unit_eq)
next
fix x and y
assume [simp]: "x ∈ G" "y ∈ G"
show "compose G (?inv x) (?inv y) = (?inv (x ⋅ y))" by (simp add: inverse_composition_commute del: translation_unit_eq)
next
show "?inv 𝟭 = identity G" by (simp del: translation_unit_eq) simp
qed

text ‹p 39, ll 10--11›
sublocale monoid_isomorphism
"λa∈G. transformation.symmetric.inverse (a)⇩R" G "(⋅)" 𝟭 Translations "compose G" "identity G" ..

end (* right_translations_of_group *)

subsection ‹Generalized Associativity.  Commutativity›

text ‹p 40, l 27; p 41, ll 1--2›
locale commutative_monoid = monoid +
assumes commutative: "⟦ x ∈ M; y ∈ M ⟧ ⟹ x ⋅ y = y ⋅ x"

text ‹p 41, l 2›
locale abelian_group = group + commutative_monoid G "(⋅)" 𝟭

subsection ‹Orbits.  Cosets of a Subgroup›

context transformation_group begin

text ‹p 51, ll 18--20›
definition Orbit_Relation
where "Orbit_Relation = {(x, y). x ∈ S ∧ y ∈ S ∧ (∃α ∈ G. y = α x)}"

text ‹p 51, ll 18--20›
lemma Orbit_Relation_memI [intro]:
"⟦ ∃α ∈ G. y = α x; x ∈ S ⟧ ⟹ (x, y) ∈ Orbit_Relation"
unfolding Orbit_Relation_def by auto

text ‹p 51, ll 18--20›
lemma Orbit_Relation_memE [elim]:
"⟦ (x, y) ∈ Orbit_Relation; ⋀α. ⟦ α ∈ G; x ∈ S; y = α x ⟧ ⟹ Q ⟧ ⟹ Q"
unfolding Orbit_Relation_def by auto

text ‹p 51, ll 20--23, 26--27›
sublocale orbit: equivalence S Orbit_Relation
proof (unfold_locales, auto simp: Orbit_Relation_def)
fix x
assume x: "x ∈ S"
then have id: "x = identity S x" by simp
with x show "∃α ∈ G. x = α x" by fast
fix α
assume α: "α ∈ G"
with x id have y: "x = compose S (symmetric.inverse α) α x" by auto
with x α show "∃α' ∈ G. x = α' (α x)"
by (metis compose_eq symmetric.sub.invertible symmetric.submonoid_inverse_closed)
fix β
assume β: "β ∈ G"
with x have "β (α x) = compose S β α x" by (simp add: compose_eq)
with α β show "∃γ ∈ G. β (α x) = γ x" by fast
qed

text ‹p 51, ll 23--24›
theorem orbit_equality:
"x ∈ S ⟹ orbit.Class x = {α x | α. α ∈ G}"
by (simp add: orbit.Class_def) (blast intro: orbit.symmetric dest: orbit.symmetric)

end (* transformation_group *)

context monoid_isomorphism begin

text ‹p 52, ll 16--17›
theorem image_subgroup:
assumes "subgroup G M (⋅) 𝟭"
shows "subgroup (η  G) M' (⋅') 𝟭'"
proof -
interpret subgroup G M "(⋅)" 𝟭 by fact
interpret image: monoid "η  G" "(⋅')" "𝟭'"
by unfold_locales (auto simp add: commutes_with_composition commutes_with_unit [symmetric])
show ?thesis
proof (unfold_locales, auto)
fix x
assume x: "x ∈ G"
show "image.invertible (η x)"
proof
show "η (sub.inverse x) ∈ η  G" using x by simp
qed (auto simp: x commutes_with_composition commutes_with_unit)
qed
qed

end (* monoid_isomorphism *)

text ‹
Technical device to achieve Jacobson's notation for @{text Right_Coset} and @{text Left_Coset}.  The
definitions are pulled out of @{text subgroup_of_group} to a context where @{text H} is not a parameter.
›
text ‹p 52, l 20›
locale coset_notation = fixes composition (infixl "⋅" 70)  begin

text ‹Equation 23›
text ‹p 52, l 20›
definition Right_Coset (infixl "|⋅" 70) where "H |⋅ x = {h ⋅ x | h. h ∈ H}"

text ‹p 53, ll 8--9›
definition Left_Coset (infixl "⋅|" 70) where "x ⋅| H = {x ⋅ h | h. h ∈ H}"

text ‹p 52, l 20›
lemma Right_Coset_memI [intro]:
"h ∈ H ⟹ h ⋅ x ∈ H |⋅ x"
unfolding Right_Coset_def by blast

text ‹p 52, l 20›
lemma Right_Coset_memE [elim]:
"⟦ a ∈ H |⋅ x; ⋀h. ⟦ h ∈ H; a = h ⋅ x ⟧ ⟹ P ⟧ ⟹ P"
unfolding Right_Coset_def by blast

text ‹p 53, ll 8--9›
lemma Left_Coset_memI [intro]:
"h ∈ H ⟹ x ⋅ h ∈ x ⋅| H"
unfolding Left_Coset_def by blast

text ‹p 53, ll 8--9›
lemma Left_Coset_memE [elim]:
"⟦ a ∈ x ⋅| H; ⋀h. ⟦ h ∈ H; a = x ⋅ h ⟧ ⟹ P ⟧ ⟹ P"
unfolding Left_Coset_def by blast

end (* coset_notation *)

text ‹p 52, l 12›
locale subgroup_of_group = subgroup H G "(⋅)" 𝟭 + coset_notation "(⋅)" + group G "(⋅)" 𝟭
for H and G and composition (infixl "⋅" 70) and unit ("𝟭")
begin

text ‹p 52, ll 12--14›
interpretation left: left_translations_of_group ..
interpretation right: right_translations_of_group ..

text ‹
@{term "left.translation  H"} denotes Jacobson's @{text "H⇩L(G)"} and
@{term "left.translation  G"} denotes Jacobson's @{text "G⇩L"}.
›

text ‹p 52, ll 16--18›
theorem left_translations_of_subgroup_are_transformation_group [intro]:
"transformation_group (left.translation  H) G"
proof -
have "subgroup (left.translation  H) (left.translation  G) (compose G) (identity G)"
by (rule left.image_subgroup) unfold_locales
also have "subgroup (left.translation  G) left.transformation.Sym (compose G) (identity G)" ..
finally interpret right_coset: subgroup "left.translation  H" left.transformation.Sym "compose G" "identity G" .
show ?thesis ..
qed

text ‹p 52, l 18›
interpretation transformation_group "left.translation  H" G ..

text ‹p 52, ll 19--20›
theorem Right_Coset_is_orbit:
"x ∈ G ⟹ H |⋅ x = orbit.Class x"
using left.translation_apply by (auto simp: orbit_equality Right_Coset_def) (metis imageI sub)

text ‹p 52, ll 24--25›
theorem Right_Coset_Union:
"(⋃x∈G. H |⋅ x) = G"

text ‹p 52, l 26›
theorem Right_Coset_bij:
assumes G [simp]: "x ∈ G" "y ∈ G"
shows "bij_betw (inverse x ⋅ y)⇩R (H |⋅ x) (H |⋅ y)"
proof (rule bij_betw_imageI)
show "inj_on (inverse x ⋅ y)⇩R (H |⋅ x)"
by (fastforce intro: inj_onI simp add: Right_Coset_is_orbit right.translation_apply orbit.block_closed)
next
show "(inverse x ⋅ y)⇩R  (H |⋅ x) = H |⋅ y"
by (force simp add: right.translation_apply associative invertible_right_inverse2)
qed

text ‹p 52, ll 25--26›
theorem Right_Cosets_cardinality:
"⟦ x ∈ G; y ∈ G ⟧ ⟹ card (H |⋅ x) = card (H |⋅ y)"
by (fast intro: bij_betw_same_card Right_Coset_bij)

text ‹p 52, l 27›
theorem Right_Coset_unit:
"H |⋅ 𝟭 = H"

text ‹p 52, l 27›
theorem Right_Coset_cardinality:
"x ∈ G ⟹ card (H |⋅ x) = card H"
using Right_Coset_unit Right_Cosets_cardinality unit_closed by presburger

text ‹p 52, ll 31--32›
definition "index = card orbit.Partition"

text ‹Theorem 1.5›
text ‹p 52, ll 33--35; p 53, ll 1--2›
theorem lagrange:
"finite G ⟹ card G = card H * index"
unfolding index_def
apply (subst card_partition)
apply (auto simp: finite_UnionD orbit.complete orbit.disjoint)
apply (metis Right_Coset_cardinality Right_Coset_is_orbit orbit.Block_self orbit.element_exists)
done

end (* subgroup_of_group *)

text ‹Left cosets›

context subgroup begin

text ‹p 31, ll 11--12›
lemma image_of_inverse [intro, simp]:
"x ∈ G ⟹ x ∈ inverse  G"
by (metis image_eqI sub.invertible sub.invertible_inverse_closed sub.invertible_inverse_inverse subgroup_inverse_equality)

end (* subgroup *)

context group begin

(* Does Jacobson show this somewhere? *)
text ‹p 53, ll 6--7›
lemma inverse_subgroupI:
assumes sub: "subgroup H G (⋅) 𝟭"
shows "subgroup (inverse  H) G (⋅) 𝟭"
proof -
from sub interpret subgroup H G "(⋅)" 𝟭 .
interpret inv: monoid "inverse  H" "(⋅)" 𝟭
by unfold_locales (auto simp del: subgroup_inverse_equality)
interpret inv: group "inverse  H" "(⋅)" 𝟭
by unfold_locales (force simp del: subgroup_inverse_equality)
show ?thesis
by unfold_locales (auto simp del: subgroup_inverse_equality)
qed

text ‹p 53, ll 6--7›
lemma inverse_subgroupD:
assumes sub: "subgroup (inverse  H) G (⋅) 𝟭"
and inv: "H ⊆ Units"
shows "subgroup H G (⋅) 𝟭"
proof -
from sub have "subgroup (inverse  inverse  H) G (⋅) 𝟭" by (rule inverse_subgroupI)
moreover from inv [THEN subsetD, simplified Units_def] have "inverse  inverse  H = H"
by (simp cong: image_cong add: image_comp)
ultimately show ?thesis by simp
qed

end (* group *)

context subgroup_of_group begin

text ‹p 53, l 6›
interpretation right_translations_of_group ..

text ‹
@{term "translation  H"} denotes Jacobson's @{text "H⇩R(G)"} and
@{term "Translations"} denotes Jacobson's @{text "G⇩R"}.
›

text ‹p 53, ll 6--7›
theorem right_translations_of_subgroup_are_transformation_group [intro]:
"transformation_group (translation  H) G"
proof -
have "subgroup ((λa∈G. transformation.symmetric.inverse (a)⇩R)  H) Translations (compose G) (identity G)"
by (rule image_subgroup) unfold_locales
also have "subgroup Translations transformation.Sym (compose G) (identity G)" ..
finally interpret left_coset: subgroup "translation  H" transformation.Sym "compose G" "identity G"
by (auto intro: transformation.symmetric.inverse_subgroupD cong: image_cong
simp: image_image transformation.symmetric.Units_def simp del: translation_unit_eq)
show ?thesis ..
qed

text ‹p 53, ll 6--7›
interpretation transformation_group "translation  H" G ..

text ‹Equation 23 for left cosets›
text ‹p 53, ll 7--8›
theorem Left_Coset_is_orbit:
"x ∈ G ⟹ x ⋅| H = orbit.Class x"
using translation_apply
by (auto simp: orbit_equality Left_Coset_def) (metis imageI sub)

end (* subgroup_of_group *)

subsection ‹Congruences.  Quotient Monoids and Groups›

text ‹Def 1.4›
text ‹p 54, ll 19--22›
locale monoid_congruence = monoid + equivalence where S = M +
assumes cong: "⟦ (a, a') ∈ E; (b, b') ∈ E ⟧ ⟹ (a ⋅ b, a' ⋅ b') ∈ E"
begin

text ‹p 54, ll 26--28›
theorem Class_cong:
"⟦ Class a = Class a'; Class b = Class b'; a ∈ M; a' ∈ M; b ∈ M; b' ∈ M ⟧ ⟹ Class (a ⋅ b) = Class (a' ⋅ b')"

text ‹p 54, ll 28--30›
definition quotient_composition (infixl "[⋅]" 70)
where "quotient_composition = (λA ∈ M / E. λB ∈ M / E. THE C. ∃a ∈ A. ∃b ∈ B. C = Class (a ⋅ b))"

text ‹p 54, ll 28--30›
theorem Class_commutes_with_composition:
"⟦ a ∈ M; b ∈ M ⟧ ⟹ Class a [⋅] Class b = Class (a ⋅ b)"
by (auto simp: quotient_composition_def intro: Class_cong [OF Class_eq Class_eq] del: equalityI)

text ‹p 54, ll 30--31›
theorem quotient_composition_closed [intro, simp]:
"⟦ A ∈ M / E; B ∈ M / E ⟧ ⟹ A [⋅] B ∈ M / E"
by (erule quotient_ClassE)+ (simp add: Class_commutes_with_composition)

text ‹p 54, l 32; p 55, ll 1--3›
sublocale quotient: monoid "M / E" "([⋅])" "Class 𝟭"
by unfold_locales (auto simp: Class_commutes_with_composition associative elim!: quotient_ClassE)

end (* monoid_congruence *)

text ‹p 55, ll 16--17›
locale group_congruence = group + monoid_congruence where M = G begin

text ‹p 55, ll 16--17›
notation quotient_composition (infixl "[⋅]" 70)

text ‹p 55, l 18›
theorem Class_right_inverse:
"a ∈ G ⟹ Class a [⋅] Class (inverse a) = Class 𝟭"

text ‹p 55, l 18›
theorem Class_left_inverse:
"a ∈ G ⟹ Class (inverse a) [⋅] Class a = Class 𝟭"

text ‹p 55, l 18›
theorem Class_invertible:
"a ∈ G ⟹ quotient.invertible (Class a)"
by (blast intro!: Class_right_inverse Class_left_inverse)+

text ‹p 55, l 18›
theorem Class_commutes_with_inverse:
"a ∈ G ⟹ quotient.inverse (Class a) = Class (inverse a)"
by (rule quotient.inverse_equality) (auto simp: Class_right_inverse Class_left_inverse)

text ‹p 55, l 17›
sublocale quotient: group "G / E" "([⋅])" "Class 𝟭"
by unfold_locales (metis Block_self Class_invertible element_exists)

end (* group_congruence *)

text ‹Def 1.5›
text ‹p 55, ll 22--25›
locale normal_subgroup =
subgroup_of_group K G "(⋅)" 𝟭 for K and G and composition (infixl "⋅" 70) and unit ("𝟭") +
assumes normal: "⟦ g ∈ G; k ∈ K ⟧ ⟹ inverse g ⋅ k ⋅ g ∈ K"

text ‹Lemmas from the proof of Thm 1.6›

context subgroup_of_group begin

text ‹We use @{term H} for @{term K}.›
text ‹p 56, ll 14--16›
theorem Left_equals_Right_coset_implies_normality:
assumes [simp]: "⋀g. g ∈ G ⟹ g ⋅| H = H |⋅ g"
shows "normal_subgroup H G (⋅) 𝟭"
proof
fix g k
assume [simp]: "g ∈ G" "k ∈ H"
have "k ⋅ g ∈ g ⋅| H" by auto
then obtain k' where "k ⋅ g = g ⋅ k'" and "k' ∈ H" by blast
then show "inverse g ⋅ k ⋅ g ∈ H" by (simp add: associative invertible_left_inverse2)
qed

end (* subgroup_of_group *)

text ‹Thm 1.6, first part›

context group_congruence begin

text ‹Jacobson's $K$›
text ‹p 56, l 29›
definition "Normal = Class 𝟭"

text ‹p 56, ll 3--6›
interpretation subgroup "Normal" G "(⋅)" 𝟭
unfolding Normal_def
proof (rule subgroupI)
fix k1 and k2
assume K: "k1 ∈ Class 𝟭" "k2 ∈ Class 𝟭"
then have "k1 ⋅ k2 ∈ Class (k1 ⋅ k2)" by blast
also have "… = Class k1 [⋅] Class k2" using K by (auto simp add: Class_commutes_with_composition Class_closed)
also have "… = Class 𝟭 [⋅] Class 𝟭" using K by (metis ClassD Class_eq unit_closed)
also have "… = Class 𝟭" by simp
finally show "k1 ⋅ k2 ∈ Class 𝟭" .
next
fix k
assume K: "k ∈ Class 𝟭"
then have "inverse k ∈ Class (inverse k)" by blast
also have "… = quotient.inverse (Class k)" using Class_commutes_with_inverse K by blast
also have "… = quotient.inverse (Class 𝟭)" using Block_self K by auto
also have "… = Class 𝟭" using quotient.inverse_unit by blast
finally show "inverse k ∈ Class 𝟭" .
qed auto

text ‹Coset notation›
text ‹p 56, ll 5--6›
interpretation subgroup_of_group "Normal" G "(⋅)" 𝟭 ..

text ‹Equation 25 for right cosets›
text ‹p 55, ll 29--30; p 56, ll 6--11›
theorem Right_Coset_Class_unit:
assumes g: "g ∈ G" shows "Normal |⋅ g = Class g"
unfolding Normal_def
proof auto
fix a  ― ‹ll 6--8›
assume a: "a ∈ Class g"
from a g have "a ⋅ inverse g ∈ Class (a ⋅ inverse g)" by blast
also from a g have "… = Class a [⋅] Class (inverse g)"
also from a g have "… = Class g [⋅] quotient.inverse (Class g)"
using Block_self Class_commutes_with_inverse by auto
also from g have "… = Class 𝟭" by simp
finally show "a ∈ Class 𝟭 |⋅ g"
unfolding Right_Coset_def
by simp (metis Class_closed a associative g inverse_equality invertible invertible_def right_unit)
next
fix a  ― ‹ll 8--9›
assume a: "a ∈ Class 𝟭 |⋅ g"
then obtain k where eq: "a = k ⋅ g" and k: "k ∈ Class 𝟭" by blast
with g have "Class a = Class k [⋅] Class g" using Class_commutes_with_composition by auto
also from k have "… = Class 𝟭 [⋅] Class g" using Block_self by auto
also from g have "… = Class g" by simp
finally show "a ∈ Class g" using g eq k composition_closed quotient.unit_closed by blast
qed

text ‹Equation 25 for left cosets›
text ‹p 55, ll 29--30; p 56, ll 6--11›
theorem Left_Coset_Class_unit:
assumes g: "g ∈ G" shows "g ⋅| Normal = Class g"
unfolding Normal_def
proof auto
fix a  ― ‹ll 6--8›
assume a: "a ∈ Class g"
from a g have "inverse g ⋅ a ∈ Class (inverse g ⋅ a)" by blast
also from a g have "… = Class (inverse g) [⋅] Class a"
also from a g have "… = quotient.inverse (Class g) [⋅] Class g"
using Block_self Class_commutes_with_inverse by auto
also from g have "… = Class 𝟭" by simp
finally show "a ∈ g ⋅| Class 𝟭"
unfolding Left_Coset_def
by simp (metis Class_closed a associative g inverse_equality invertible invertible_def right_unit)
next
fix a  ― ‹ll 8--9, the same thing holds''›
assume a: "a ∈ g ⋅| Class 𝟭"
then obtain k where eq: "a = g ⋅ k" and k: "k ∈ Class 𝟭" by blast
with g have "Class a = Class g [⋅] Class k" using Class_commutes_with_composition by auto
also from k have "… = Class g [⋅] Class 𝟭" using Block_self by auto
also from g have "… = Class g" by simp
finally show "a ∈ Class g" using g eq k composition_closed quotient.unit_closed by blast
qed

text ‹Thm 1.6, statement of first part›
text ‹p 55, ll 28--29; p 56, ll 12--16›
theorem Class_unit_is_normal:
"normal_subgroup Normal G (⋅) 𝟭"
proof -
{
fix g
assume "g ∈ G"
then have "g ⋅| Normal = Normal |⋅ g" by (simp add: Right_Coset_Class_unit Left_Coset_Class_unit)
}
then show ?thesis by (rule Left_equals_Right_coset_implies_normality)
qed

sublocale normal: normal_subgroup Normal G "(⋅)" 𝟭
by (fact Class_unit_is_normal)

end (* group_congruence *)

context normal_subgroup begin

text ‹p 56, ll 16--19›
theorem Left_equals_Right_coset:
"g ∈ G ⟹ g ⋅| K = K |⋅ g"
proof
assume [simp]: "g ∈ G"
show "K |⋅ g ⊆ g ⋅| K"
proof
fix x
assume x: "x ∈ K |⋅ g"
then obtain k where "x = k ⋅ g" and [simp]: "k ∈ K" by (auto simp add: Right_Coset_def)
then have "x = g ⋅ (inverse g ⋅ k ⋅ g)" by (simp add: associative invertible_right_inverse2)
also from normal have "… ∈ g ⋅| K" by (auto simp add: Left_Coset_def)
finally show "x ∈ g ⋅| K" .
qed
next
assume [simp]: "g ∈ G"
show "g ⋅| K ⊆ K |⋅ g"
proof
fix x
assume x: "x ∈ g ⋅| K"
then obtain k where "x = g ⋅ k" and [simp]: "k ∈ K" by (auto simp add: Left_Coset_def)
then have "x = (inverse (inverse g) ⋅ k ⋅ inverse g) ⋅ g" by (simp add: associative del: invertible_right_inverse)
also from normal [where g = "inverse g"] have "… ∈ K |⋅ g" by (auto simp add: Right_Coset_def)
finally show "x ∈ K |⋅ g" .
qed
qed

text ‹Thm 1.6, second part›

text ‹p 55, ll 31--32; p 56, ll 20--21›
definition "Congruence = {(a, b). a ∈ G ∧ b ∈ G ∧ inverse a ⋅ b ∈ K}"

text ‹p 56, ll 21--22›
interpretation right_translations_of_group ..

text ‹p 56, ll 21--22›
interpretation transformation_group "translation  K" G rewrites "Orbit_Relation = Congruence"
proof -
interpret transformation_group "translation  K" G ..
show "Orbit_Relation = Congruence"
unfolding Orbit_Relation_def Congruence_def
by (force simp: invertible_left_inverse2 invertible_right_inverse2 translation_apply simp del: restrict_apply)
qed rule

text ‹p 56, ll 20--21›
lemma CongruenceI: "⟦ a = b ⋅ k; a ∈ G; b ∈ G; k ∈ K ⟧ ⟹ (a, b) ∈ Congruence"
by (clarsimp simp: Congruence_def associative inverse_composition_commute)

text ‹p 56, ll 20--21›
lemma CongruenceD: "(a, b) ∈ Congruence ⟹ ∃k∈K. a = b ⋅ k"
by (drule orbit.symmetric) (force simp: Congruence_def invertible_right_inverse2)

text ‹
We showed in the last section that the relation we are considering is an equivalence relation in
@{term G} for any subgroup @{term K} of @{term G}.  We now proceed to show that normality of @{term K}
ensures that [...] $a \equiv b \pmod{K}$ is a congruence.''
›
text ‹p 55, ll 30--32; p 56, ll 1, 22--28›
sublocale group_congruence where E = Congruence rewrites "Normal = K"
proof -
show "group_congruence G (⋅) 𝟭 Congruence"
proof unfold_locales
note CongruenceI [intro] CongruenceD [dest]
fix a g b h
assume 1: "(a, g) ∈ Congruence" and 2: "(b, h) ∈ Congruence"
then have G: "a ∈ G" "g ∈ G" "b ∈ G" "h ∈ G" unfolding Congruence_def by clarify+
from 1 obtain k1 where a: "a = g ⋅ k1" and k1: "k1 ∈ K" by blast
from 2 obtain k2 where b: "b = h ⋅ k2" and k2: "k2 ∈ K" by blast
from G Left_equals_Right_coset have "K |⋅ h = h ⋅| K" by blast
with k1 obtain k3 where c: "k1 ⋅ h = h ⋅ k3" and k3: "k3 ∈ K"
unfolding Left_Coset_def Right_Coset_def by blast
from G k1 k2 a b have "a ⋅ b = g ⋅ k1 ⋅ h ⋅ k2" by (simp add: associative)
also from G k1 k3 c have "… = g ⋅ h ⋅ k3 ⋅ k2" by (simp add: associative)
also have "… = (g ⋅ h) ⋅ (k3 ⋅ k2)" using G k2 k3 by (simp add: associative)
finally show "(a ⋅ b, g ⋅ h) ∈ Congruence" using G k2 k3 by blast
qed
then interpret group_congruence where E = Congruence .
show "Normal = K"
unfolding Normal_def orbit.Class_def unfolding Congruence_def
using invertible_inverse_inverse submonoid_inverse_closed by fastforce
qed

end (* normal_subgroup *)  (* deletes translations and orbits, recovers Class for congruence class *)

context group begin

text ‹Pulled out of @{locale normal_subgroup} to achieve standard notation.›
text ‹p 56, ll 31--32›
abbreviation Factor_Group (infixl "'/'/" 75)
where "S // K ≡ S / (normal_subgroup.Congruence K G (⋅) 𝟭)"

end (* group *)

context normal_subgroup begin

text ‹p 56, ll 28--29›
theorem Class_unit_normal_subgroup: "Class 𝟭 = K"
unfolding Class_def unfolding Congruence_def
using invertible_inverse_inverse submonoid_inverse_closed by fastforce

text ‹p 56, ll 1--2; p 56, l 29›
theorem Class_is_Left_Coset:
"g ∈ G ⟹ Class g = g ⋅| K"
using Left_Coset_Class_unit Class_unit_normal_subgroup by simp

text ‹p 56, l 29›
lemma Left_CosetE: "⟦ A ∈ G // K; ⋀a. a ∈ G ⟹ P (a ⋅| K) ⟧ ⟹ P A"
by (metis Class_is_Left_Coset quotient_ClassE)

text ‹Equation 26›
text ‹p 56, ll 32--34›
theorem factor_composition [simp]:
"⟦ g ∈ G; h ∈ G ⟧ ⟹ (g ⋅| K) [⋅] (h ⋅| K) = g ⋅ h ⋅| K"
using Class_commutes_with_composition Class_is_Left_Coset by auto

text ‹p 56, l 35›
theorem factor_unit:
"K = 𝟭 ⋅| K"
using Class_is_Left_Coset Class_unit_normal_subgroup by blast

text ‹p 56, l 35›
theorem factor_inverse [simp]:
"g ∈ G ⟹ quotient.inverse (g ⋅| K) = (inverse g ⋅| K)"
using Class_commutes_with_inverse Class_is_Left_Coset by auto

end (* normal_subgroup *)

text ‹p 57, ll 4--5›
locale subgroup_of_abelian_group = subgroup_of_group H G "(⋅)" 𝟭 + abelian_group G "(⋅)" 𝟭
for H and G and composition (infixl "⋅" 70) and unit ("𝟭")

text ‹p 57, ll 4--5›
sublocale subgroup_of_abelian_group ⊆ normal_subgroup H G "(⋅)" 𝟭
using commutative invertible_right_inverse2 by unfold_locales auto

subsection ‹Homomorphims›

text ‹Def 1.6›
text ‹p 58, l 33; p 59, ll 1--2›
locale monoid_homomorphism =
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"
and commutes_with_unit: "η 𝟭 = 𝟭'"
begin

text ‹Jacobson notes that @{thm [source] commutes_with_unit} is not necessary for groups, but doesn't make use of that later.›

text ‹p 58, l 33; p 59, ll 1--2›
notation source.invertible ("invertible _"  100)
notation source.inverse ("inverse _"  100)
notation target.invertible ("invertible'' _"  100)
notation target.inverse ("inverse'' _"  100)

end (* monoid_homomorphism *)

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'

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)

context monoid_homomorphism begin

text ‹p 59, ll 33--34›
theorem invertible_image_lemma:
assumes "invertible a" "a ∈ M"
shows "η a ⋅' η (inverse a) = 𝟭'" and "η (inverse a) ⋅' η a = 𝟭'"
using assms commutes_with_composition commutes_with_unit source.inverse_equality
by auto (metis source.invertible_inverse_closed source.invertible_left_inverse)

text ‹p 59, l 34; p 60, l 1›
theorem invertible_target_invertible [intro, simp]:
"⟦ invertible a; a ∈ M ⟧ ⟹ invertible' (η a)"
using invertible_image_lemma by blast

text ‹p 60, l 1›
theorem invertible_commutes_with_inverse:
"⟦ invertible a; a ∈ M ⟧ ⟹ η (inverse a) = inverse' (η a)"
using invertible_image_lemma target.inverse_equality by fastforce

end (* monoid_homomorphism *)

text ‹p 60, ll 32--34; p 61, l 1›
sublocale monoid_congruence ⊆ natural: monoid_homomorphism Class M "(⋅)" 𝟭 "M / E" "([⋅])" "Class 𝟭"
by unfold_locales (auto simp: PiE_I Class_commutes_with_composition)

text ‹Fundamental Theorem of Homomorphisms of Monoids›

text ‹p 61, ll 5, 14--16›
sublocale monoid_homomorphism ⊆ image: submonoid "η  M" M' "(⋅')" "𝟭'"
by unfold_locales (auto simp: commutes_with_composition [symmetric] commutes_with_unit [symmetric])

text ‹p 61, l 4›
locale monoid_homomorphism_fundamental = monoid_homomorphism begin

text ‹p 61, ll 17--18›
sublocale fiber_relation η M M' ..
notation Fiber_Relation ("E'(_')")

text ‹p 61, ll 6--7, 18--20›
sublocale monoid_congruence where E = "E(η)"
using Class_eq
by unfold_locales (rule Class_equivalence [THEN iffD1],
auto simp: left_closed right_closed commutes_with_composition Fiber_equality)

text ‹p 61, ll 7--9›
text ‹
@{term induced} denotes Jacobson's $\bar{\eta}$.  We have the commutativity of the diagram, where
@{term induced} is unique: @{thm [display] factorization} @{thm [display] uniqueness}.
›

text ‹p 61, l 20›
notation quotient_composition (infixl "[⋅]" 70)

text ‹p 61, ll 7--8, 22--25›
sublocale induced: monoid_homomorphism induced "M / E(η)" "([⋅])" "Class 𝟭" "M'" "(⋅')" "𝟭'"
apply unfold_locales
apply (auto simp: commutes_with_unit)
apply (fastforce simp: commutes_with_composition commutes_with_unit Class_commutes_with_composition)
done

text ‹p 61, ll 9, 26›
sublocale natural: monoid_epimorphism Class M "(⋅)" 𝟭 "M / E(η)" "([⋅])" "Class 𝟭" ..

text ‹p 61, ll 9, 26--27›
sublocale induced: monoid_monomorphism induced "M / E(η)" "([⋅])" "Class 𝟭" "M'" "(⋅')" "𝟭'" ..

end (* monoid_homomorphism_fundamental *)

text ‹p 62, ll 12--13›
locale group_homomorphism =
monoid_homomorphism η G "(⋅)" 𝟭 G' "(⋅')" "𝟭'" +
source: group G "(⋅)" 𝟭 + target: group G' "(⋅')" "𝟭'"
for η and G and composition (infixl "⋅" 70) and unit ("𝟭")
and G' and composition' (infixl "⋅''" 70) and unit' ("𝟭''")
begin

text ‹p 62, l 13›
sublocale image: subgroup "η  G" G' "(⋅')" "𝟭'"
using invertible_image_lemma by unfold_locales auto

text ‹p 62, ll 13--14›
definition "Ker = η - {𝟭'} ∩ G"

text ‹p 62, ll 13--14›
lemma Ker_equality:
"Ker = {a | a. a ∈ G ∧ η a = 𝟭'}"
unfolding Ker_def by auto

text ‹p 62, ll 13--14›
lemma Ker_closed [intro, simp]:
"a ∈ Ker ⟹ a ∈ G"
unfolding Ker_def by simp

text ‹p 62, ll 13--14›
lemma Ker_image [intro]: (* loops as a simprule *)
"a ∈ Ker ⟹ η a = 𝟭'"
unfolding Ker_def by simp

text ‹p 62, ll 13--14›
lemma Ker_memI [intro]: (* loops as a simprule *)
"⟦ η a = 𝟭'; a ∈ G ⟧ ⟹ a ∈ Ker"
unfolding Ker_def by simp

text ‹p 62, ll 15--16›
sublocale kernel: normal_subgroup Ker G
proof -
interpret kernel: submonoid Ker G
unfolding Ker_def by unfold_locales (auto simp: commutes_with_composition commutes_with_unit)
interpret kernel: subgroup Ker G
by unfold_locales (force intro: source.invertible_right_inverse simp: Ker_image invertible_commutes_with_inverse)
show "normal_subgroup Ker G (⋅) 𝟭"
apply unfold_locales
unfolding Ker_def
by (auto simp: commutes_with_composition invertible_image_lemma(2))
qed

text ‹p 62, ll 17--20›
theorem injective_iff_kernel_unit:
"inj_on η G ⟷ Ker = {𝟭}"
proof (rule Not_eq_iff [THEN iffD1, OF iffI])
assume "Ker ≠ {𝟭}"
then obtain b where b: "b ∈ Ker" "b ≠ 𝟭" by blast
then have "η b = η 𝟭" by (simp add: Ker_image)
with b show "¬ inj_on η G"  by (meson inj_onD kernel.sub source.unit_closed)
next
assume "¬ inj_on η G"
then obtain a b where "a ≠ b" and ab: "a ∈ G" "b ∈ G" "η a = η b" by (meson inj_onI)
then have "inverse a ⋅ b ≠ 𝟭" "η (inverse a ⋅ b) = 𝟭'"
using ab source.invertible_right_inverse2
by force (metis ab commutes_with_composition invertible_image_lemma(2) source.invertible source.invertible_inverse_closed)
then have "inverse a ⋅ b ∈ Ker" using Ker_memI ab by blast
then show "Ker ≠ {𝟭}" using ‹inverse a ⋅ b ≠ 𝟭› by blast
qed

end (* group_homomorphism *)

text ‹p 62, l 24›
locale group_epimorphism = group_homomorphism + monoid_epimorphism η G "(⋅)" 𝟭 G' "(⋅')" "𝟭'"

text ‹p 62, l 21›
locale normal_subgroup_in_kernel =
group_homomorphism + contained: normal_subgroup L G "(⋅)" 𝟭 for L +
assumes subset: "L ⊆ Ker"
begin

text ‹p 62, l 21›
notation contained.quotient_composition (infixl "[⋅]" 70)

text ‹"homomorphism onto @{term "G // L"}"›
text ‹p 62, ll 23--24›
sublocale natural: group_epimorphism contained.Class G "(⋅)" 𝟭 "G // L" "([⋅])" "contained.Class 𝟭" ..

text ‹p 62, ll 25--26›
theorem left_coset_equality:
assumes eq: "a ⋅| L = b ⋅| L" and [simp]: "a ∈ G" and b: "b ∈ G"
shows "η a = η b"
proof -
obtain l where l: "b = a ⋅ l" "l ∈ L"
by (metis b contained.Class_is_Left_Coset contained.Class_self eq kernel.Left_Coset_memE)
then have "η a = η a ⋅' η l" using Ker_image monoid_homomorphism.commutes_with_composition subset by auto
also have "… = η b" by (simp add: commutes_with_composition l)
finally show ?thesis .
qed

text ‹$\bar{\eta}$›
text ‹p 62, ll 26--27›
definition "induced = (λA ∈ G // L. THE b. ∃a ∈ G. a ⋅| L = A ∧ b = η a)"

text ‹p 62, ll 26--27›
lemma induced_closed [intro, simp]:
assumes [simp]: "A ∈ G // L" shows "induced A ∈ G'"
proof -
obtain a where a: "a ∈ G" "a ⋅| L = A" using contained.Class_is_Left_Coset contained.Partition_def assms by auto
have "(THE b. ∃a ∈ G. a ⋅| L = A ∧ b = η a) ∈ G'"
apply (rule theI2)
using a by (auto intro: left_coset_equality)
then show ?thesis unfolding induced_def by simp
qed

text ‹p 62, ll 26--27›
lemma induced_undefined [intro, simp]:
"A ∉ G // L ⟹ induced A = undefined"
unfolding induced_def by simp

text ‹p 62, ll 26--27›
theorem induced_left_coset_closed [intro, simp]:
"a ∈ G ⟹ induced (a ⋅| L) ∈ G'"
using contained.Class_is_Left_Coset contained.Class_in_Partition by auto

text ‹p 62, ll 26--27›
theorem induced_left_coset_equality [simp]:
assumes [simp]: "a ∈ G" shows "induced (a ⋅| L) = η a"
proof -
have "(THE b. ∃a' ∈ G. a' ⋅| L = a ⋅| L ∧ b = η a') = η a"
by (rule the_equality) (auto intro: left_coset_equality)
then show ?thesis unfolding induced_def
using contained.Class_is_Left_Coset contained.Class_in_Partition by auto
qed

text ‹p 62, l 27›
theorem induced_Left_Coset_commutes_with_composition [simp]:
"⟦ a ∈ G; b ∈ G ⟧ ⟹ induced ((a ⋅| L) [⋅] (b ⋅| L)) = induced (a ⋅| L) ⋅' induced (b ⋅| L)"

text ‹p 62, ll 27--28›
theorem induced_group_homomorphism:
"group_homomorphism induced (G // L) ([⋅]) (contained.Class 𝟭) G' (⋅') 𝟭'"
apply unfold_locales
apply (auto elim!: contained.Left_CosetE simp: commutes_with_composition commutes_with_unit)
using contained.factor_unit induced_left_coset_equality apply (fastforce simp: contained.Class_unit_normal_subgroup)
done

text ‹p 62, l 28›
sublocale induced: group_homomorphism induced "G // L" "([⋅])" "contained.Class 𝟭" G' "(⋅')" "𝟭'"
by (fact induced_group_homomorphism)

text ‹p 62, ll 28--29›
theorem factorization_lemma: "a ∈ G ⟹ compose G induced contained.Class a = η a"
unfolding compose_def by (simp add: contained.Class_is_Left_Coset)

text ‹p 62, ll 29--30›
theorem factorization [simp]: "compose G induced contained.Class = η"
by rule (simp add: compose_def contained.Class_is_Left_Coset map_undefined)

text ‹
Jacobson does not state the uniqueness of @{term induced} explicitly but he uses it later,
for rings, on p 107.
›
text ‹p 62, l 30›
theorem uniqueness:
assumes map: "β ∈ G // L →⇩E G'"
and factorization: "compose G β contained.Class = η"
shows "β = induced"
proof
fix A
show "β A = induced A"
proof (cases "A ∈ G // L")
case True
then obtain a where [simp]: "A = contained.Class a" "a ∈ G" by fast
then have "β (contained.Class a) = η a" by (metis compose_eq factorization)
also have "… = induced (contained.Class a)" by (simp add: contained.Class_is_Left_Coset)
finally show ?thesis by simp
qed (simp add: induced_def PiE_arb [OF map])
qed

text ‹p 62, l 31›
theorem induced_image:
"induced  (G // L) = η  G"
by (metis factorization contained.natural.surjective surj_compose)

text ‹p 62, l 33›
interpretation L: normal_subgroup L Ker
by unfold_locales (auto simp: subset, metis kernel.sub kernel.subgroup_inverse_equality contained.normal)

text ‹p 62, ll 31--33›
theorem induced_kernel:
"induced.Ker = Ker / L.Congruence" (* Ker // L is apparently not the right thing *)
proof -
have "induced.Ker = { a ⋅| L | a. a ∈ G ∧ a ∈ Ker }"
unfolding induced.Ker_equality
by simp (metis (hide_lams) contained.Class_is_Left_Coset Ker_image Ker_memI
induced_left_coset_equality contained.Class_in_Partition contained.representant_exists)
also have "… = Ker / L.Congruence"
using L.Class_is_Left_Coset L.Class_in_Partition
by auto (metis L.Class_is_Left_Coset L.representant_exists kernel.sub)
finally show ?thesis .
qed

text ‹p 62, ll 34--35›
theorem induced_inj_on:
"inj_on induced (G // L) ⟷ L = Ker"
apply (simp add: induced.injective_iff_kernel_unit induced_kernel contained.Class_unit_normal_subgroup)
apply rule
using L.block_exists apply auto 
using L.Block_self L.Class_unit_normal_subgroup L.quotient.unit_closed L.representant_exists
apply auto
done

end (* normal_subgroup_in_kernel *)

text ‹Fundamental Theorem of Homomorphisms of Groups›

text ‹p 63, l 1›
locale group_homomorphism_fundamental = group_homomorphism begin

text ‹p 63, l 1›
notation kernel.quotient_composition (infixl "[⋅]" 70)

text ‹p 63, l 1›
sublocale normal_subgroup_in_kernel where L = Ker by unfold_locales rule

text ‹p 62, ll 36--37; p 63, l 1›
text ‹
@{term induced} denotes Jacobson's $\bar{\eta}$.  We have the commutativity of the diagram, where
@{term induced} is unique: @{thm [display] factorization} @{thm [display] uniqueness}
›

end (* group_homomorphism_fundamental *)

text ‹p 63, l 5›
locale group_isomorphism = group_homomorphism + bijective_map η G G' begin

text ‹p 63, l 5›
sublocale monoid_isomorphism η G "(⋅)" 𝟭 G' "(⋅')" "𝟭'"
by unfold_locales (auto simp: commutes_with_composition)

text ‹p 63, l 6›
lemma inverse_group_isomorphism:
"group_isomorphism (restrict (inv_into G η) G') G' (⋅') 𝟭' G (⋅) 𝟭"
using commutes_with_composition commutes_with_unit surjective by unfold_locales auto

end (* group_isomorphism *)

text ‹p 63, l 6›
definition isomorphic_as_groups (infixl "≅⇩G" 50)
where "𝒢 ≅⇩G 𝒢' ⟷ (let (G, composition, unit) = 𝒢; (G', composition', unit') = 𝒢' in
(∃η. group_isomorphism η G composition unit G' composition' unit'))"

text ‹p 63, l 6›
lemma isomorphic_as_groups_symmetric:
"(G, composition, unit) ≅⇩G (G', composition', unit') ⟹ (G', composition', unit') ≅⇩G (G, composition, unit)"
by (simp add: isomorphic_as_groups_def) (meson group_isomorphism.inverse_group_isomorphism)

text ‹p 63, l 1›
sublocale group_isomorphism ⊆ group_epimorphism ..

text ‹p 63, l 1›
locale group_epimorphism_fundamental = group_homomorphism_fundamental + group_epimorphism begin

text ‹p 63, ll 1--2›
interpretation image: group_homomorphism induced "G // Ker" "([⋅])" "kernel.Class 𝟭" "(η  G)" "(⋅')" "𝟭'"
by (simp add: surjective group_homomorphism_fundamental.intro induced_group_homomorphism)

text ‹p 63, ll 1--2›
sublocale image: group_isomorphism induced "G // Ker" "([⋅])" "kernel.Class 𝟭" "(η  G)" "(⋅')" "𝟭'"
using induced_group_homomorphism
by unfold_locales (auto simp: bij_betw_def induced_image induced_inj_on induced.commutes_with_composition)

end (* group_epimorphism_fundamental *)

context group_homomorphism begin

text ‹p 63, ll 5--7›
theorem image_isomorphic_to_factor_group:
"∃K composition unit. normal_subgroup K G (⋅) 𝟭 ∧ (η  G, (⋅'), 𝟭') ≅⇩G (G // K, composition, unit)"
proof -
interpret image: group_epimorphism_fundamental where G' = "η  G"
by unfold_locales (auto simp: commutes_with_composition)
have "group_isomorphism image.induced (G // Ker) ([⋅]) (kernel.Class 𝟭) (η  G) (⋅') 𝟭'" ..
then have "(η  G, (⋅'), 𝟭') ≅⇩G (G // Ker, ([⋅]), kernel.Class 𝟭)"
by (simp add: isomorphic_as_groups_def) (meson group_isomorphism.inverse_group_isomorphism)
moreover have "normal_subgroup Ker G (⋅) 𝟭" ..
ultimately show ?thesis by blast
qed

end (* group_homomorphism *)

end


# Theory Ring_Theory

(*
Copyright (c) 2015--2019 by Clemens Ballarin
*)

theory Ring_Theory imports Group_Theory begin

no_notation plus (infixl "+" 65)
no_notation minus (infixl "-" 65)
no_notation uminus ("- _"  80)
no_notation quotient (infixl "'/'/" 90)

section ‹Rings›

subsection ‹Definition and Elementary Properties›

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 ("- _"  65)
abbreviation subtraction (infixl "-" 65) where "a - b ≡ a + (- b)"  (* or, alternatively, a definition *)

end (* ring *)

text ‹p 87, ll 10--12›
locale subring =
additive: subgroup S R "(+)" 𝟬 + multiplicative: submonoid S R "(⋅)" 𝟭
for S and R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭")

context ring begin

text ‹p 88, ll 26--28›
lemma right_zero [simp]:
assumes [simp]: "a ∈ R" shows "a ⋅ 𝟬 = 𝟬"
proof -
have "a ⋅ 𝟬 = a ⋅ (𝟬 + 𝟬)" by simp
also have "… = a ⋅ 𝟬 + a ⋅ 𝟬" by (simp add: distributive del: additive.left_unit additive.right_unit)
finally have "a ⋅ 𝟬 - a ⋅ 𝟬 = a ⋅ 𝟬 + a ⋅ 𝟬 - a ⋅ 𝟬" by simp
qed

text ‹p 88, l 29›
lemma left_zero [simp]:
assumes [simp]: "a ∈ R" shows "𝟬 ⋅ a = 𝟬"
proof -
have "𝟬 ⋅ a = (𝟬 + 𝟬) ⋅ a" by simp
also have "… = 𝟬 ⋅ a + 𝟬 ⋅ a" by (simp add: distributive del: additive.left_unit additive.right_unit)
finally have "𝟬 ⋅ a - 𝟬 ⋅ a = 𝟬 ⋅ a + 𝟬 ⋅ a - 𝟬 ⋅ a" by simp
qed

text ‹p 88, ll 29--30; p 89, ll 1--2›
lemma left_minus:
assumes [simp]: "a ∈ R" "b ∈ R" shows "(- a) ⋅ b = - a ⋅ b"
proof -
have "𝟬 = 𝟬 ⋅ b" by simp
also have "… = (a - a) ⋅ b" by simp
also have "… = a ⋅ b + (- a) ⋅ b" by (simp add: distributive del: additive.invertible_right_inverse)
finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + (- a) ⋅ b" by (simp add: additive.associative del: additive.invertible_left_inverse)
then show ?thesis by simp
qed

text ‹p 89, l 3›
lemma right_minus:
assumes [simp]: "a ∈ R" "b ∈ R" shows "a ⋅ (- b) = - a ⋅ b"
proof -
have "𝟬 = a ⋅ 𝟬" by simp
also have "… = a ⋅ (b - b)" by simp
also have "… = a ⋅ b + a ⋅ (- b)" by (simp add: distributive del: additive.invertible_right_inverse)
finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + a ⋅ (- b)" by (simp add: additive.associative del: additive.invertible_left_inverse)
then show ?thesis by simp
qed

end (* ring *)

subsection ‹Ideals, Quotient Rings›

text ‹p 101, ll 2--5›
locale ring_congruence = ring +
additive: group_congruence R "(+)" 𝟬 E +
multiplicative: monoid_congruence R "(⋅)" 𝟭 E
for E
begin

text ‹p 101, ll 2--5›
notation additive.quotient.inverse ("[-] _"  65)
notation multiplicative.quotient_composition (infixl "[⋅]" 70)

text ‹p 101, ll 5--11›
sublocale quotient: ring "R / E" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭"
by unfold_locales

end (* ring_congruence *)

text ‹p 101, ll 12--13›
additive: subgroup I R "(+)" 𝟬 + ring R "(+)" "(⋅)" 𝟬 𝟭
for I and R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭")
begin

text ‹p 101, ll 13--14›
definition "Ring_Congruence = {(a, b). a ∈ R ∧ b ∈ R ∧ a - b ∈ I}"

text ‹p 101, ll 13--14›
lemma Ring_CongruenceI: "⟦ a - b ∈ I; a ∈ R; b ∈ R ⟧ ⟹ (a, b) ∈ Ring_Congruence"
using Ring_Congruence_def by blast

text ‹p 101, ll 13--14›
lemma Ring_CongruenceD: "(a, b) ∈ Ring_Congruence ⟹ a - b ∈ I"
using Ring_Congruence_def by blast

text ‹
Jacobson's definition of ring congruence deviates from that of group congruence; this complicates
the proof.
›
text ‹p 101, ll 12--14›
sublocale additive: subgroup_of_abelian_group I R "(+)" 𝟬  (* implies normal_subgroup *)
proof -
show "subgroup_of_abelian_group I R (+) 𝟬"
then interpret additive: subgroup_of_abelian_group I R "(+)" 𝟬 .
{
fix a b
assume [simp]: "a ∈ R" "b ∈ R"
have "a - b ∈ I ⟷ - (a - b) ∈ I" by auto
finally have "a - b ∈ I ⟷ - a + b ∈ I" .
}
qed

text ‹p 101, l 14›

text ‹Def 2.2›
text ‹p 101, ll 21--22›
assumes ideal: "⟦ a ∈ R; b ∈ I ⟧ ⟹ a ⋅ b ∈ I" "⟦ a ∈ R; b ∈ I ⟧ ⟹ b ⋅ a ∈ I"

text ‹p 101, ll 14--17›
theorem multiplicative_congruence_implies_ideal:
assumes "monoid_congruence R (⋅) 𝟭 Ring_Congruence"
shows "ideal I R (+) (⋅) 𝟬 𝟭"
proof -
interpret multiplicative: monoid_congruence R "(⋅)" 𝟭 Ring_Congruence by fact
show ?thesis
proof
fix a b
assume [simp]: "a ∈ R" "b ∈ I"
have congs: "(a, a) ∈ Ring_Congruence" "(b, 𝟬) ∈ Ring_Congruence"
from congs have "(a ⋅ b, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce
then show "a ⋅ b ∈ I" using additive.Class_unit_normal_subgroup by blast
from congs have "(b ⋅ a, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce
then show "b ⋅ a ∈ I"  using additive.Class_unit_normal_subgroup by blast
qed
qed

context ideal begin

text ‹p 101, ll 17--20›
theorem multiplicative_congruence [intro]:
assumes a: "(a, a') ∈ Ring_Congruence" and b: "(b, b') ∈ Ring_Congruence"
shows "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence"
proof -
note Ring_CongruenceI [intro] Ring_CongruenceD [dest]
from a b have [simp]: "a ∈ R" "a' ∈ R" "b ∈ R" "b' ∈ R" by auto
from a have [simp]: "a - a' ∈ I" ..
have "a ⋅ b - a' ⋅ b = (a - a') ⋅ b" by (simp add: distributive left_minus)
also have "… ∈ I" by (simp add: ideal)
finally have ab: "a ⋅ b - a' ⋅ b ∈ I" .  ― ‹ll 18--19›
from b have [simp]: "b - b' ∈ I" ..
have "a' ⋅ b - a' ⋅ b' = a' ⋅ (b - b')" by (simp add: distributive right_minus)
also have "… ∈ I" by (simp add: ideal)
finally have a'b': "a' ⋅ b - a' ⋅ b' ∈ I" .  ― ‹l 19›
have "a ⋅ b - a' ⋅ b' = (a ⋅ b - a' ⋅ b) + (a' ⋅ b - a' ⋅ b')"
also have "… ∈ I" using ab a'b' by simp
finally show "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence" by auto  ― ‹ll 19--20›
qed

text ‹p 101, ll 23--24›
sublocale ring_congruence where E = Ring_Congruence by unfold_locales rule

end (* ideal *)

context ring begin

text ‹Pulled out of @{locale ideal} to achieve standard notation.›
text ‹p 101, ll 24--26›
abbreviation Quotient_Ring (infixl "'/'/" 75)
where "S // I ≡ S / (subgroup_of_additive_group_of_ring.Ring_Congruence I R (+) 𝟬)"

end (* ring *)

text ‹p 101, ll 24--26›
locale quotient_ring = ideal begin

text ‹p 101, ll 24--26›
sublocale quotient: ring "R // I" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭" ..

text ‹p 101, l 26›

text ‹Equation 17 (1)›
text ‹p 101, l 28›

text ‹Equation 17 (2)›
text ‹p 101, l 29›
theorem quotient_multiplication [simp]:
"⟦ a ∈ R; b ∈ R ⟧ ⟹ (a +| I) [⋅] (b +| I) = a ⋅ b +| I"

text ‹p 101, l 30›

end (* quotient_ring *)

subsection ‹Homomorphisms of Rings.  Basic Theorems›

text ‹Def 2.3›
text ‹p 106, ll 7--9›
locale ring_homomorphism =
map η R R' + source: ring R "(+)" "(⋅)" 𝟬 𝟭 + target: ring R' "(+')" "(⋅')" "𝟬'" "𝟭'" +
additive: group_homomorphism η R "(+)" 𝟬 R' "(+')" "𝟬'" +
multiplicative: monoid_homomorphism η R "(⋅)" 𝟭 R' "(⋅')" "𝟭'"
for η
and R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭")
and R' and addition' (infixl "+''" 65) and multiplication' (infixl "⋅''" 70) and zero' ("𝟬''") and unit' ("𝟭''")

text ‹p 106, l 17›
locale ring_epimorphism = ring_homomorphism + surjective_map η R R'

text ‹p 106, ll 14--18›
sublocale quotient_ring ⊆ natural: ring_epimorphism
where η = additive.Class and R' = "R // I" and addition' = "([+])" and multiplication' =  "([⋅])"
..

context ring_homomorphism begin

text ‹
Jacobson reasons via @{term "a - b ∈ additive.Ker"} being a congruence; we prefer the direct proof,
since it is very simple.
›
text ‹p 106, ll 19--21›
sublocale kernel: ideal where I = additive.Ker
by unfold_locales (auto simp: additive.Ker_image multiplicative.commutes_with_composition)

end (* ring_homomorphism *)

text ‹p 106, l 22›
locale ring_monomorphism = ring_homomorphism + injective_map η R R'

context ring_homomorphism begin

text ‹p 106, ll 21--23›
theorem ring_monomorphism_iff_kernel_unit:
"ring_monomorphism η R (+) (⋅) 𝟬 𝟭 R' (+') (⋅') 𝟬' 𝟭' ⟷ additive.Ker = {𝟬}" (is "?monom ⟷ ?ker")
proof
assume ?monom then interpret ring_monomorphism . show ?ker by (simp add: additive.injective_iff_kernel_unit [symmetric])
next
qed

end (* ring_homomorphism *)

text ‹p 106, ll 23--25›
sublocale ring_homomorphism ⊆ image: subring "η  R" R' "(+')" "(⋅')" "𝟬'" "𝟭'" ..

text ‹p 106, ll 26--27›
locale ideal_in_kernel =
ring_homomorphism + contained: ideal I R "(+)" "(⋅)" 𝟬 𝟭 for I +
begin

text ‹p 106, ll 26--27›
notation contained.multiplicative.quotient_composition (infixl "[⋅]" 70)

text ‹Provides @{text additive.induced}, which Jacobson calls $\bar{\eta}$.›
text ‹p 106, l 30›
sublocale additive: normal_subgroup_in_kernel η R "(+)" 𝟬 R' "(+')" "𝟬'" I
rewrites "normal_subgroup.Congruence I R addition zero = contained.Ring_Congruence"

text ‹Only the multiplicative part needs some work.›
text ‹p 106, ll 27--30›
using contained.multiplicative.Class_commutes_with_composition
by unfold_locales

text ‹p 106, l 30; p 107, ll 1--3›
text ‹
@{term additive.induced} denotes Jacobson's $\bar{\eta}$.  We have the commutativity of the diagram, where
›

end (* ideal_in_kernel *)

text ‹Fundamental Theorem of Homomorphisms of Rings›

text ‹p 107, l 6›
locale ring_homomorphism_fundamental = ring_homomorphism begin

text ‹p 107, l 6›
notation kernel.multiplicative.quotient_composition (infixl "[⋅]" 70)

text ‹p 107, l 6›
sublocale ideal_in_kernel where I = additive.Ker by unfold_locales rule

text ‹p 107, ll 8--9›
sublocale natural: ring_epimorphism
and multiplication' = "kernel.multiplicative.quotient_composition"
..

text ‹p 107, l 9›
sublocale induced: ring_monomorphism
and multiplication = "kernel.multiplicative.quotient_composition"

end (* ring_homomorphism_fundamental *)

text ‹p 107, l 11›
locale ring_isomorphism = ring_homomorphism + bijective_map η R R' begin

text ‹p 107, l 11›
sublocale ring_monomorphism ..
sublocale ring_epimorphism ..

text ‹p 107, l 11›
lemma inverse_ring_isomorphism:
"ring_isomorphism (restrict (inv_into R η) R') R' (+') (⋅') 𝟬' 𝟭' R (+) (⋅) 𝟬 𝟭"
multiplicative.commutes_with_composition [symmetric] multiplicative.commutes_with_unit surjective
by unfold_locales auto

end (* ring_isomorphsim *)

text ‹p 107, l 11›
definition isomorphic_as_rings (infixl "≅⇩R" 50)
where "ℛ ≅⇩R ℛ' ⟷ (let (R, addition, multiplication, zero, unit) = ℛ; (R', addition', multiplication', zero', unit') = ℛ' in
(∃η. ring_isomorphism η R addition multiplication zero unit R' addition' multiplication' zero' unit'))"

text ‹p 107, l 11›
lemma isomorphic_as_rings_symmetric:
"(R, addition, multiplication, zero, unit) ≅⇩R (R', addition', multiplication', zero', unit') ⟹
by (simp add: isomorphic_as_rings_def) (meson ring_isomorphism.inverse_ring_isomorphism)

context ring_homomorphism begin

text ‹Corollary›
text ‹p 107, ll 11--12›
theorem image_is_isomorphic_to_quotient_ring:
"∃K add mult zero one. ideal K R (+) (⋅) 𝟬 𝟭 ∧ (η  R, (+'), (⋅'), 𝟬', 𝟭') ≅⇩R (R // K, add, mult, zero, one)"
proof -
interpret image: ring_homomorphism_fundamental where R' = "η  R"
have "ring_isomorphism image.additive.induced (R // additive.Ker) ([+]) ([⋅]) (kernel.additive.Class 𝟬) (kernel.additive.Class 𝟭) (η  R) (+') (⋅') 𝟬' 𝟭'"
`