Theory Jacobson_Basic_Algebra.Group_Theory

(*
  Copyright (c) 2014-2019 by Clemens Ballarin
  This file is licensed under the 3-clause BSD license.
*)

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"
  by (simp add: inverse_def)

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"
  by (simp add: inverse_equality)

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


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)"
  by (simp add: invertible_left_inverse2 associative)
  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"
  by (simp add: Units_bijective)

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'
  by unfold_locales (simp add: commutes_with_composition)

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
qed (simp add: commutes_with_composition)

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"
  by (simp add: image_subsetI)

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"
  by unfold_locales (simp add: translation_def)

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)"
    by (simp add: inj_on_imp_bij_betw)
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
  by unfold_locales (simp add: translation_def)

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"
  by (simp add: image_subsetI)

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 (λaG. 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
  "λaG. 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 "HL(G)"} and
  @{term "left.translation ` G"} denotes Jacobson's @{text "GL"}.
›

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:
  "(xG. H |⋅ x) = G"
  by (simp add: Right_Coset_is_orbit)

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"
  by (force simp add: Right_Coset_def)

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 "HR(G)"} and
  @{term "Translations"} denotes Jacobson's @{text "GR"}.
›

text ‹p 53, ll 6--7›
theorem right_translations_of_subgroup_are_transformation_group [intro]:
  "transformation_group (translation ` H) G"
proof -
  have "subgroup ((λaG. 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')"
  by (simp add: Class_equivalence cong)

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 𝟭"
  by (simp add: Class_commutes_with_composition)

text ‹p 55, l 18›
theorem Class_left_inverse:
  "a  G  Class (inverse a) [⋅] Class a = Class 𝟭"
  by (simp add: Class_commutes_with_composition)

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)"
    by (simp add: Class_commutes_with_composition block_closed)
  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"
    by (simp add: Class_commutes_with_composition block_closed)
  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  kK. 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] 100)
notation source.inverse ("inverse _" [100] 100)
notation target.invertible ("invertible'' _" [100] 100)
notation target.inverse ("inverse'' _" [100] 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)"
  by (simp add: commutes_with_composition)

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 (opaque_lifting) 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 [1]
  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