Theory Group_Theory

(*
  Derived from the AFP entry Jacobson_Basic_Algebra, by Clemens Ballarin
*)

theory Group_Theory 
  imports Set_Theory 

begin

section ‹Monoids and Groups›

subsection ‹Monoids of Transformations and Abstract Monoids›

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 "(⋅)" 𝟭
proof qed (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 "invertible u ≡ (∃v ∈ M. u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭)"

text ‹p 31, ll 3--5›
lemma invertibleI [intro]:
  "⟦ u ⋅ v = 𝟭; v ⋅ u = 𝟭; 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 ⟧ ⟹ 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"
  using inverse_def local.inverse_unique by auto

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 (metis (lifting) inverse_def restrict_apply)

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 ‹A self-contained introduction rule for groups: the monoid laws together with the
  existence of a two-sided inverse for every element (stated directly, without reference
  to the @{const Monoid.invertible} predicate, which would otherwise require a separate
  monoid interpretation).›
lemma GroupI:
  fixes G and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
  assumes "⋀a b. ⟦ a ∈ G; b ∈ G ⟧ ⟹ a ⋅ b ∈ G"
    and "𝟭 ∈ G"
    and "⋀a b c. ⟦ a ∈ G; b ∈ G; c ∈ G ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)"
    and "⋀a. a ∈ G ⟹ 𝟭 ⋅ a = a"
    and "⋀a. a ∈ G ⟹ a ⋅ 𝟭 = a"
    and inv: "⋀u. u ∈ G ⟹ ∃v ∈ G. u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭"
  shows "Group G (⋅) 𝟭"
proof -
  interpret Monoid G "(⋅)" 𝟭
    using assms(1-5) by unfold_locales blast+
  show ?thesis
  proof 
    fix u assume "u ∈ G"
    then obtain v where "v ∈ G" "u ⋅ v = 𝟭" "v ⋅ u = 𝟭" using inv by blast
    then show "invertible u" using invertibleI by blast
  qed
qed

text ‹p 31, ll 11--12›
text ‹The first parameter @{term H} is the ∗‹subgroup› and @{term G} the ambient
  group, mirroring the parameter order of @{locale Submonoid}.  At all use sites one
  writes ‹subgroup H G› (subgroup then ambient); the later locales
  ‹subgroup_of_group› and ‹normal_subgroup› take their parameters in the same order.›
locale Subgroup = Submonoid H G "(⋅)" 𝟭 + sub: Group H "(⋅)" 𝟭
  for H and G 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 ∈ H ⟹ inverse u = sub.inverse u"
  by (simp add: inverse_equality)

text ‹p 31, ll 11--12›
lemma subgroup_inverse_iff [simp]:
  "⟦ invertible x; x ∈ G ⟧ ⟹ inverse x ∈ H ⟷ x ∈ H"
  using invertible_inverse_inverse sub.invertible_inverse_closed by fastforce

end (* subgroup *)

text ‹A subgroup is in particular a group in its own right.›
lemma subgroup_imp_Group:
  assumes "Subgroup H M composition unit"
  shows "Group H composition unit"
  using assms Subgroup.axioms(2) by fastforce


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

lemma subgroup_restrict:
  assumes I: "Subgroup I G composition unit"
    and H: "Subgroup H G composition unit"
    and "I ⊆ H"
  shows "Subgroup I H composition unit"
proof -
  interpret I: Subgroup I G composition unit by fact
  interpret H: Subgroup H G composition unit by fact
  have "Submonoid I H composition unit"
  proof (rule Submonoid.intro[OF H.sub.Monoid_axioms], rule Submonoid_axioms.intro)
    show "I ⊆ H" by fact
    show "⋀a b. ⟦a ∈ I; b ∈ I⟧ ⟹ composition a b ∈ I"
      by (rule I.sub_composition_closed)
    show "unit ∈ I" by (rule I.sub_unit_closed)
  qed
  then show ?thesis
    by (rule Subgroup.intro) (rule I.sub.Group_axioms)
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

lemma conjugate_composition:
  assumes "invertible g" "g ∈ M" "a ∈ M" "b ∈ M"
  shows "inverse g ⋅ (a ⋅ b) ⋅ g =
         (inverse g ⋅ a ⋅ g) ⋅ (inverse g ⋅ b ⋅ g)"
proof -
  have invg: "inverse g ∈ M"
    by (rule invertible_inverse_closed[OF assms(1,2)])
  have ab: "a ⋅ b ∈ M" by (rule composition_closed[OF assms(3,4)])
  have bg: "b ⋅ g ∈ M" by (rule composition_closed[OF assms(4,2)])
  have ia: "inverse g ⋅ a ∈ M" by (rule composition_closed[OF invg assms(3)])
  have ib: "inverse g ⋅ b ∈ M" by (rule composition_closed[OF invg assms(4)])
  have ibg: "inverse g ⋅ b ⋅ g ∈ M"
    by (rule composition_closed[OF ib assms(2)])
  have cancel: "g ⋅ (inverse g ⋅ (b ⋅ g)) = b ⋅ g"
    by (rule invertible_right_inverse2[OF assms(1,2) bg])
  have left:
    "inverse g ⋅ (a ⋅ b) ⋅ g = inverse g ⋅ (a ⋅ (b ⋅ g))"
  proof -
    have "inverse g ⋅ (a ⋅ b) ⋅ g = inverse g ⋅ ((a ⋅ b) ⋅ g)"
      by (rule associative[OF invg ab assms(2)])
    also have "… = inverse g ⋅ (a ⋅ (b ⋅ g))"
      by (simp only: associative[OF assms(3,4,2)])
    finally show ?thesis .
  qed
  have right:
    "(inverse g ⋅ a ⋅ g) ⋅ (inverse g ⋅ b ⋅ g) =
     inverse g ⋅ (a ⋅ (b ⋅ g))"
  proof -
    have "(inverse g ⋅ a ⋅ g) ⋅ (inverse g ⋅ b ⋅ g) =
          (inverse g ⋅ a) ⋅ (g ⋅ (inverse g ⋅ b ⋅ g))"
      by (rule associative[OF ia assms(2) ibg])
    also have "… = (inverse g ⋅ a) ⋅ (g ⋅ (inverse g ⋅ (b ⋅ g)))"
      by (simp only: associative[OF invg assms(4,2)])
    also have "… = (inverse g ⋅ a) ⋅ (b ⋅ g)"
      by (simp only: cancel)
    also have "… = inverse g ⋅ (a ⋅ (b ⋅ g))"
      by (rule associative[OF invg assms(3) bg])
    finally show ?thesis .
  qed
  show ?thesis by (rule trans[OF left right[symmetric]])
qed

end (* Monoid *)

context Group begin

text ‹The whole group is a subgroup of itself.›
lemma group_self_subgroup: "Subgroup G G (⋅) 𝟭"
  by (rule subgroupI) auto

text ‹The trivial subgroup, consisting of the unit alone.›
lemma trivial_subgroup: "Subgroup {𝟭} G (⋅) 𝟭"
  by (rule subgroupI) auto


subsection ‹The subgroup generated by a set›

text ‹
  The subgroup generated by a set @{term S} of elements of a group, defined
  inductively as the smallest set containing @{term "S ∩ G"} and closed under the
  group operations.  This basic construction underlies commutators, the derived
  series, and solvability.
›

inductive_set generate :: "'a set ⇒ 'a set" for S :: "'a set"
  where
    unit:  "𝟭 ∈ generate S"
  | incl:  "x ∈ S ∩ G ⟹ x ∈ generate S"
  | comp:  "⟦ x ∈ generate S; y ∈ generate S ⟧ ⟹ x ⋅ y ∈ generate S"
  | inv:   "x ∈ generate S ⟹ inverse x ∈ generate S"

definition Gen :: "'a set ⇒ 'a set" (‹⟨_⟩›)
  where "⟨S⟩ ≡ generate (S ∩ G)"

text ‹Everything generated lies in the carrier.›
lemma generate_subset_carrier: "generate S ⊆ G"
proof
  fix x assume "x ∈ generate S"
  then show "x ∈ G"
  proof induction
    case unit then show ?case by simp
  next
    case (incl x) then show ?case by simp
  next
    case (comp x y) then show ?case by simp
  next
    case (inv x) then show ?case by simp
  qed
qed

lemma Gen_subset_carrier: "⟨S⟩ ⊆ G"
  unfolding Gen_def by (rule generate_subset_carrier)

text ‹The generated set is a subgroup.›
lemma generate_is_subgroup: "Subgroup (generate S) G (⋅) 𝟭"
proof (rule subgroupI)
  show "generate S ⊆ G" by (rule generate_subset_carrier)
next
  show "𝟭 ∈ generate S" by (rule generate.unit)
next
  fix g h assume "g ∈ generate S" "h ∈ generate S"
  then show "g ⋅ h ∈ generate S" by (rule generate.comp)
next
  fix g assume "g ∈ generate S"
  then have "g ∈ G" using generate_subset_carrier by auto
  then show "invertible g" by simp
next
  fix g assume "g ∈ generate S"
  then show "inverse g ∈ generate S" by (rule generate.inv)
qed

lemma Gen_is_subgroup: "Subgroup ⟨S⟩ G (⋅) 𝟭"
  unfolding Gen_def by (rule generate_is_subgroup)

text ‹The generating set is included (intersected with the carrier).›
lemma generate_incl: "S ∩ G ⊆ generate S"
  using generate.incl by auto

lemma Gen_incl: "S ∩ G ⊆ ⟨S⟩"
  unfolding Gen_def using generate.incl by auto

text ‹@{term "generate S"} is the smallest subgroup containing @{term "S ∩ G"}.›
lemma generate_minimal:
  assumes "Subgroup H G (⋅) 𝟭" and "S ∩ G ⊆ H"
  shows "generate S ⊆ H"
proof
  interpret H: Subgroup H G "(⋅)" 𝟭 by (rule assms(1))
  fix x assume "x ∈ generate S"
  then show "x ∈ H"
  proof induction
    case unit then show ?case by (rule H.sub_unit_closed)
  next
    case (incl x) then show ?case using assms(2) by auto
  next
    case (comp x y)
    then show ?case using H.sub_composition_closed by blast
  next
    case (inv x)
    then show ?case using H.submonoid_inverse_closed H.sub.invertible by auto
  qed
qed

lemma Gen_minimal:
  assumes "Subgroup H G (⋅) 𝟭" and "S ∩ G ⊆ H"
  shows "⟨S⟩ ⊆ H"
  unfolding Gen_def using assms by (intro generate_minimal) auto

text ‹Monotonicity.›
lemma generate_mono:
  assumes "S ⊆ T"
  shows "generate S ⊆ generate T"
proof (rule generate_minimal)
  show "Subgroup (generate T) G (⋅) 𝟭" by (rule generate_is_subgroup)
  show "S ∩ G ⊆ generate T" using assms generate_incl by auto
qed

lemma Gen_mono:
  assumes "S ⊆ T"
  shows "⟨S⟩ ⊆ ⟨T⟩"
  unfolding Gen_def using assms by (intro generate_mono) (auto)

text ‹A subgroup generates itself.›
lemma generate_subgroup_eq:
  assumes "Subgroup H G (⋅) 𝟭" and "H ⊆ G"
  shows "generate H = H"
proof
  show "generate H ⊆ H" using assms by (intro generate_minimal) auto
  show "H ⊆ generate H" using assms generate_incl by auto
qed

lemma Gen_subgroup_eq:
  assumes "Subgroup H G (⋅) 𝟭"
  shows "⟨H⟩ = H"
proof -
  interpret H: Subgroup H G "(⋅)" 𝟭 by (rule assms)
  have "H ⊆ G" by auto
  then show ?thesis unfolding Gen_def using assms
    by (simp add: Int_absorb2 generate_subgroup_eq)
qed

text ‹Idempotence.›
lemma Gen_idem: "⟨⟨S⟩⟩ = ⟨S⟩"
  using Gen_is_subgroup by (rule Gen_subgroup_eq)

text ‹The intersection characterisation: @{term "⟨S⟩"} is the intersection of all
  subgroups containing @{term "S ∩ G"}.›
lemma Gen_eq_Inter:
  "⟨S⟩ = ⋂{H. Subgroup H G (⋅) 𝟭 ∧ S ∩ G ⊆ H}"
proof
  show "⟨S⟩ ⊆ ⋂{H. Subgroup H G (⋅) 𝟭 ∧ S ∩ G ⊆ H}"
    using Gen_minimal by auto
next
  have "⟨S⟩ ∈ {H. Subgroup H G (⋅) 𝟭 ∧ S ∩ G ⊆ H}"
    using Gen_is_subgroup Gen_incl by auto
  then show "⋂{H. Subgroup H G (⋅) 𝟭 ∧ S ∩ G ⊆ H} ⊆ ⟨S⟩"
    by (rule Inter_lower)
qed

text ‹The set generated inside a subgroup (with the restricted operation) is contained
  in the set generated in the ambient group.  A locality property of @{const generate}.›
lemma generate_subgroup_subset:
  assumes H: "Subgroup H G (⋅) 𝟭"
  shows "Group.generate H (⋅) 𝟭 S ⊆ generate S"
proof
  interpret S: Subgroup H G "(⋅)" 𝟭 by (rule H)
  fix x assume "x ∈ Group.generate H (⋅) 𝟭 S"
  then show "x ∈ generate S"
  proof induction
    case unit
    then show ?case by (rule generate.unit)
  next
    case (incl x)
    then have "x ∈ S ∩ G" using S.sub by auto
    then show ?case by (rule generate.incl)
  next
    case (comp x y)
    then show ?case using generate.comp by blast
  next
    case (inv x)
    have "x ∈ H" using inv.hyps S.sub.generate_subset_carrier by auto
    then have "S.sub.inverse x = inverse x" by (simp add: S.subgroup_inverse_equality)
    then show ?case using inv.IH generate.inv by simp
  qed
qed

end (* Group *)

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"
  using bij_betw_iff_has_inverse dom invertible_def by auto

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 (use commutes_with_composition in auto)

text ‹Both definitions are equivalent.›
text ‹p 37, ll 12--15›
sublocale Monoid_isomorphism' ⊆ Monoid_isomorphism
proof 
  {
    fix y assume "y ∈ M'"
    then obtain x where "η x = y" "x ∈ M"
      using bij_betw_imp_surj_on by blast
    then have "y ⋅' η 𝟭 = y" using commutes_with_composition by auto
  }
  then show "η 𝟭 = 𝟭'"
    using bij_betwE by fastforce
qed (auto simp: 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 (⋅) 𝟭"
proof -
  have "⋀x y. ⟦x ∈ M'; y ∈ M'⟧
           ⟹ inv_into M η x ⋅ inv_into M η y = inv_into M η (x ⋅' y)"
    using commutes_with_composition surjective by fastforce
  with bij_betw_inv_into bij_betw_inv_into_left commutes_with_unit target.unit_closed 
  show ?thesis
  proof unfold_locales qed fastforce+
qed

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 ‹Reflexivity and transitivity complete the picture: isomorphism is an equivalence relation
  on monoid triples, which is what lets isomorphism classes be formed as a quotient.›

lemma isomorphic_as_monoids_refl:
  assumes "Monoid M composition unit"
  shows "(M, composition, unit) ≅⇩M (M, composition, unit)"
proof -
  interpret M: Monoid M composition unit by fact
  have "Monoid_isomorphism (restrict id M) M composition unit M composition unit"
    by unfold_locales
      (auto simp: PiE_def extensional_def restrict_def bij_betw_def inj_on_def
        M.composition_closed)
  then show ?thesis unfolding isomorphic_as_monoids_def by auto
qed

lemma isomorphic_as_monoids_transitive:
  assumes "(M, composition, unit) ≅⇩M (M', composition', unit')"
    and "(M', composition', unit') ≅⇩M (M'', composition'', unit'')"
  shows "(M, composition, unit) ≅⇩M (M'', composition'', unit'')"
proof -
  obtain η where first: "Monoid_isomorphism η M composition unit M' composition' unit'"
    using assms(1) unfolding isomorphic_as_monoids_def by auto
  obtain θ where second: "Monoid_isomorphism θ M' composition' unit' M'' composition'' unit''"
    using assms(2) unfolding isomorphic_as_monoids_def by auto
  interpret first: Monoid_isomorphism η M composition unit M' composition' unit' by fact
  interpret second: Monoid_isomorphism θ M' composition' unit' M'' composition'' unit'' by fact
  have "Monoid_isomorphism (restrict (θ ∘ η) M) M composition unit M'' composition'' unit''"
  proof
    show "restrict (θ ∘ η) M ∈ M →⇩E M''"
      using first.graph second.graph by auto
    show "composition'' (restrict (θ ∘ η) M x) (restrict (θ ∘ η) M y)
            = restrict (θ ∘ η) M (composition x y)"
      if "x ∈ M" "y ∈ M" for x y
      using that first.commutes_with_composition second.commutes_with_composition
        first.source.composition_closed first.map_closed by auto
    show "restrict (θ ∘ η) M unit = unit''"
      using first.commutes_with_unit second.commutes_with_unit first.source.unit_closed by simp
    have "bij_betw (θ ∘ η) M M''"
      using first.bijective second.bijective by (rule bij_betw_trans)
    then show "bij_betw (restrict (θ ∘ η) M) M M''"
      by (simp add: bij_betw_restrict_eq)
  qed
  then show ?thesis unfolding isomorphic_as_monoids_def by auto
qed

text ‹Being a group is a property of the isomorphism class, not of the presentation: invertibility
  transports along a monoid isomorphism, because the isomorphism carries a two-sided inverse to a
  two-sided inverse and reaches every element of the target.  This is what allows isomorphism
  classes to be formed once, at the level of monoids, with group-ness imposed as a constraint.›
lemma (in Monoid_isomorphism) target_Group:
  assumes "Group M (⋅) 𝟭"
  shows "Group M' (⋅') 𝟭'"
proof (rule GroupI)
  interpret source: Group M "(⋅)" 𝟭 by (rule assms)
  fix u assume u: "u ∈ M'"
  then obtain a where a: "a ∈ M" and ηa: "η a = u"
    using bijective by (metis bij_betw_imp_surj_on imageE)
  obtain b where b: "b ∈ M" and ab: "a ⋅ b = 𝟭" and ba: "b ⋅ a = 𝟭"
    using source.invertible[OF a] unfolding source.invertible_def by blast
  have "η b ∈ M'" using b by (rule map_closed)
  moreover have "u ⋅' η b = 𝟭'"
    using ηa commutes_with_composition[OF a b] ab commutes_with_unit by simp
  moreover have "η b ⋅' u = 𝟭'"
    using ηa commutes_with_composition[OF b a] ba commutes_with_unit by simp
  ultimately show "∃v ∈ M'. u ⋅' v = 𝟭' ∧ v ⋅' u = 𝟭'" by blast
qed (use target.composition_closed target.unit_closed target.associative
       target.left_unit target.right_unit in blast)+

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 (metis left_unit restrict_apply' restrict_ext unit_closed)

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"
  by (auto simp: associative compose_def translation_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›
lemma translation_is_map: "translation ∈ M →⇩E (translation ` M)"
  using translation_def by force

text ‹p 38, ll 12--16›
theorem translation_isomorphism [intro]:
  "Monoid_isomorphism translation M (⋅) 𝟭 (translation ` M) (compose M) (identity M)"
proof 
  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)
  show "translation ∈ M →⇩E translation ` M"
    using translation_is_map by auto
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›
lemma "translation ∈ G →⇩E Translations"
  by (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 (λa∈G. transformation.symmetric.inverse (a)⇩R) G (⋅) 𝟭 Translations (compose G) (identity G)"
  (is "Monoid_isomorphism ?inv _ _ _ _ _ _")
proof 
  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)
  show "?inv 𝟭 = identity G"
    using transformation.symmetric.inverse_unit by auto
  show "?inv ∈ G →⇩E Translations"
    using transformation.symmetric.submonoid_inverse_closed
      transformation.symmetric.sub.invertible by auto
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)
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"
begin

text ‹The left-commutativity law: together with @{thm associative} and @{thm commutative} it forms a
  confluent rewrite system for normalising products.  We bundle the three as @{text ac} so a proof
  can request full associative-commutative normalisation on demand via @{text "simp add: ac"}, rather
  than making them global @{attribute simp} rules (which would change the simplifier's normal form
  throughout the development).›
lemma left_commutative:
  assumes "x ∈ M" "y ∈ M" "z ∈ M"
  shows "x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
proof -
  have "x ⋅ (y ⋅ z) = (x ⋅ y) ⋅ z" using assms by (simp add: associative)
  also have "… = (y ⋅ x) ⋅ z" using assms by (simp add: commutative)
  also have "… = y ⋅ (x ⋅ z)" using assms by (simp add: associative)
  finally show ?thesis .
qed

lemmas ac = associative commutative left_commutative

end

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]:
  "⟦ y = α x; α ∈ G; 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 (intro equivalenceI)
  show "Orbit_Relation ⊆ S × S"
    by (auto simp: Orbit_Relation_def)
next
  fix a
  assume "a ∈ S"
  then show "(a, a) ∈ Orbit_Relation"
    using Orbit_Relation_memI by fastforce
next
  fix a b
  assume "(a, b) ∈ Orbit_Relation"
  then show "(b, a) ∈ Orbit_Relation"
    by (metis Orbit_Relation_memE Orbit_Relation_memI compose_eq restrict_apply' symmetric.sub.invertible
        symmetric.sub.invertible_def transformation_group_closed)
next
  fix a b c
  assume "(a, b) ∈ Orbit_Relation" and "(b, c) ∈ Orbit_Relation"
  then have "∃α∈G. c = α a"
    by (metis Orbit_Relation_memE compose_eq symmetric.sub_composition_closed)
  then show "(a, c) ∈ Orbit_Relation"
    using ‹(a, b) ∈ Orbit_Relation› by blast
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: commutes_with_composition sub.associative simp flip: commutes_with_unit)
  show ?thesis
  proof
    show "η ` G ⊆ M'"
      using bij_betw_imp_surj_on by blast
  next
    fix u :: 'b
    assume "u ∈ η ` G"
    then show "image.invertible u"
      using commutes_with_composition commutes_with_unit sub.invertible_def image.invertible_def by fastforce
  qed auto
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. h ⋅ x) ` H"

text ‹p 53, ll 8--9›
definition Left_Coset (infixl ‹⋅|› 70) where "x ⋅| H ≡ (λh. x ⋅ 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"
  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)"
    unfolding inj_on_def
    by (smt (verit) Right_Coset_memE assms  associative composition_closed in_mono invertible
        invertible_inverse_closed invertible_right_inverse right.translation_apply right_unit subset)
next
  show "(inverse x ⋅ y)⇩R ` (H |⋅ x) = H |⋅ y"
    by (force simp: 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:
  assumes "finite G"
  shows "card G = card H * index"
  unfolding index_def
proof (subst card_partition)
  fix c :: "'a set"
  assume "c ∈ orbit.Partition"
  then show "card c = card H"
    using Right_Coset_cardinality Right_Coset_is_orbit orbit.Partition_def
    by auto
next
  fix c1 c2
  assume "c1 ∈ orbit.Partition" and "c2 ∈ orbit.Partition"
    and "c1 ≠ c2"
  then show "c1 ∩ c2 = {}"
    using orbit.not_disjoint_implies_equal
    by (auto simp: image_iff orbit.Partition_def)
qed (use assms in ‹auto simp: orbit.Partition_def›)

end (* subgroup_of_group *)

lemma subgroup_of_groupI:
  assumes "Subgroup H G composition unit" and "Group G composition unit"
  shows "subgroup_of_group H G composition unit"
proof -
  interpret H: Subgroup H G composition unit by fact
  interpret G: Group G composition unit by fact
  show ?thesis by unfold_locales
qed

text ‹Left cosets›

context Subgroup begin

text ‹p 31, ll 11--12›

lemma image_of_inverse [intro, simp]:
  "x ∈ H ⟹ x ∈ inverse ` H"
  by (smt (verit) imageI inverse_equality sub sub.invertible sub.invertibleE)

lemma image_of_inverse_iff:
  "x ∈ inverse ` H ⟷ x ∈ H"
  by blast

end (* subgroup *)

context Group begin

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

text ‹Intersections are the basic way of restricting subgroups and normal
  subgroups to a smaller ambient group.›

lemma subgroup_intersection:
  assumes "Subgroup H G (⋅) 𝟭" "Subgroup K G (⋅) 𝟭"
  shows "Subgroup (H ∩ K) G (⋅) 𝟭"
proof -
  interpret H: Subgroup H G "(⋅)" 𝟭 by fact
  interpret K: Subgroup K G "(⋅)" 𝟭 by fact
  interpret HK: Monoid "H ∩ K" "(⋅)" 𝟭
    by unfold_locales auto
  show ?thesis
  proof
    fix u
    assume u: "u ∈ H ∩ K"
    have inv_H: "local.inverse u ∈ H"
      by (rule H.submonoid_inverse_closed) (use u in auto)
    have inv_K: "local.inverse u ∈ K"
      by (rule K.submonoid_inverse_closed) (use u in auto)
    have right: "u ⋅ local.inverse u = 𝟭"
      using u by simp
    have left: "local.inverse u ⋅ u = 𝟭"
      using u by simp
    show "HK.invertible u"
      unfolding HK.invertible_def
      using inv_H inv_K left right by blast
  qed auto
qed

lemma commute_iff_inverse:
  assumes "g ∈ G" "h ∈ G"
  shows "(g ⋅ h = h ⋅ g) ⟷ (g ⋅ h ⋅ local.inverse g = h)"
proof -
  have "g ⋅ h ∈ G"
    using assms by simp
  then have "g ⋅ h ⋅ local.inverse g ⋅ g = g ⋅ h ⋅ (local.inverse g ⋅ g)"
    using assms by blast
  then show ?thesis
    using assms by auto
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')"
  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"
  using Class_commutes_with_composition Partition_def by auto

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 Class_invertible quotient_ClassE)

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"

context Group begin

text ‹The trivial subgroup is normal in every group.›
lemma trivial_normal_subgroup:
  "normal_subgroup {𝟭} G (⋅) 𝟭"
proof (intro normal_subgroup.intro subgroup_of_group.intro)
  show "Subgroup {𝟭} G (⋅) 𝟭" by (rule trivial_subgroup)
  show "Group G (⋅) 𝟭" by (rule Group_axioms)
  show "normal_subgroup_axioms {𝟭} G (⋅) 𝟭"
  proof
    fix g k
    assume "g ∈ G" "k ∈ {𝟭}"
    then show "inverse g ⋅ k ⋅ g ∈ {𝟭}" by simp
  qed
qed

end

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 𝟭)"
    by (metis Class_eq K Equivalence.ClassD Equivalence_axioms unit_closed)
  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"
  then have §: "a ⋅ inverse g ∈ Class 𝟭 ⟹ ∃h. a = h ⋅ g ∧ h ∈ Class 𝟭"
    by (metis Class_closed associative g inverse_equality invertible invertible_def right_unit)
  from a g have "a ⋅ inverse g ∈ Class (a ⋅ inverse g)" by blast
  also from a g have "… = Class a [⋅] Class (inverse g)"
    using Class_closed Class_commutes_with_composition invertible
      invertible_inverse_closed by presburger
  also from a g have "… = Class g [⋅] quotient.inverse (Class g)"
    by (metis Class_commutes_with_inverse Class_eq ClassD)
  also from g have "… = Class 𝟭" by simp
  finally show "a ∈ Class 𝟭 |⋅ g"
    using § by (auto simp: Right_Coset_def)
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"
    by (metis ClassD Class_eq unit_closed)
  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"
  then have §: "inverse g ⋅ a ∈ Class 𝟭 ⟹ ∃h. a = g ⋅ h ∧ h ∈ Class 𝟭"
    by (metis Class_closed associative g inverse_equality invertible invertible_def right_unit)
  from a g have "inverse g ⋅ a ∈ Class (inverse g ⋅ a)" by blast
  also from a g have "… = Class (inverse g) [⋅] Class a"
    using Class_closed Class_commutes_with_composition invertible
      invertible_inverse_closed by presburger
  also from a g have "… = quotient.inverse (Class g) [⋅] Class g"
    by (metis ClassD Class_commutes_with_inverse Class_eq)
  also from g have "… = Class 𝟭" by simp
  finally show "a ∈ g ⋅| Class 𝟭"
    using § by (auto simp: Left_Coset_def)
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 𝟭"
    by (metis ClassD Class_eq unit_closed)
  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

lemma set_prod_commute:
  assumes "S ⊆ G"
  shows "(case_prod(⋅)) ` (S × K) = (case_prod(⋅)) ` (K × S)"
proof -
  have "∃x∈K. ∃y∈S. a ⋅ b = x ⋅ y" if "a ∈ S" "b ∈ K" for a b
    using that assms
    by (metis Left_equals_Right_coset Right_Coset_memE coset_notation.Left_Coset_memI
        subsetD)
  moreover have "∃x∈S. ∃y∈K. a ⋅ b = x ⋅ y" if "a ∈ K" "b ∈ S" for a b
    using that
    by (metis Left_Coset_memE Left_equals_Right_coset assms coset_notation.Right_Coset_memI
        subsetD)
  ultimately show ?thesis
    by (auto simp add: image_iff subset_iff)
qed

text ‹p 56, ll 31--32; no infix syntax because it leads to many problems›
abbreviation Factor_Group (* == Partition!*)
  where "Factor_Group ≡ G / (normal_subgroup.Congruence K G (⋅) 𝟭)"

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

context Group begin

lemma normal_subgroup_intersection:
  assumes K: "normal_subgroup K G (⋅) 𝟭"
    and H: "Subgroup H G (⋅) 𝟭"
  shows "normal_subgroup (H ∩ K) H (⋅) 𝟭"
proof -
  interpret H: Subgroup H G "(⋅)" 𝟭 by fact
  interpret K: normal_subgroup K G "(⋅)" 𝟭 by fact
  have HK_G: "Subgroup (H ∩ K) G (⋅) 𝟭"
    by (rule subgroup_intersection[OF H K.Subgroup_axioms])
  interpret HK: Subgroup "H ∩ K" H "(⋅)" 𝟭
    by (rule subgroup_restrict[OF HK_G H]) auto
  show ?thesis
  proof
    fix h k
    assume h: "h ∈ H" and k: "k ∈ H ∩ K"
    then show "H.sub.inverse h ⋅ k ⋅ h ∈ H ∩ K"
      by (metis H.sub H.sub.invertible H.sub_composition_closed
          H.subgroup_inverse_equality H.submonoid_inverse_closed Int_iff K.normal)
  qed
qed

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 ‹The quotient by a normal subgroup is trivial exactly when that
  subgroup is the whole carrier.  Keeping the representative argument here
  avoids repeating it for each client that packages a quotient group.›
lemma Factor_Group_eq_singleton_iff:
  "Factor_Group = {Class 𝟭} ⟷ K = G"
proof
  assume factor_group: "Factor_Group = {Class 𝟭}"
  show "K = G"
  proof (rule equalityI)
    show "K ⊆ G" by (rule subset)
    show "G ⊆ K"
    proof
      fix x
      assume x: "x ∈ G"
      have class_mem: "Class x ∈ Factor_Group"
        by (rule Class_in_Partition[OF x])
      have class_eq: "Class x = Class 𝟭"
        using class_mem factor_group by simp
      have "x ∈ Class x" by (rule Class_self[OF x])
      then have "x ∈ Class 𝟭" using class_eq by simp
      then show "x ∈ K" using Class_unit_normal_subgroup by simp
    qed
  qed
next
  assume KG: "K = G"
  show "Factor_Group = {Class 𝟭}"
  proof (rule equalityI)
    show "Factor_Group ⊆ {Class 𝟭}"
    proof
      fix A
      assume A: "A ∈ Factor_Group"
      then obtain x where x: "x ∈ G" and A_eq: "A = Class x"
        using representant_exists by auto
      have xK: "x ∈ K" using KG x by simp
      have class_eq: "Class x = Class 𝟭"
      proof (rule Class_eq)
        show "(x, 𝟭) ∈ Congruence"
        proof (rule CongruenceI)
          show "x = 𝟭 ⋅ x" by (rule left_unit[OF x, symmetric])
          show "x ∈ G" by fact
          show "𝟭 ∈ G" by (rule unit_closed)
          show "x ∈ K" by fact
        qed
      qed
      show "A ∈ {Class 𝟭}" using A_eq class_eq by simp
    qed
    show "{Class 𝟭} ⊆ Factor_Group"
      using Class_in_Partition[OF unit_closed] by simp
  qed
qed

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 ∈ Factor_Group; ⋀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

lemma Factor_Group_eq_Left_Cosets:
  "Factor_Group = (λg. g ⋅| K) ` G"
proof (rule set_eqI)
  fix A
  show "A ∈ Factor_Group ⟷ A ∈ (λg. g ⋅| K) ` G"
  proof
    assume "A ∈ Factor_Group"
    then obtain g where "g ∈ G" "A = Class g"
      using quotient_ClassE by (metis representant_exists)
    then show "A ∈ (λg. g ⋅| K) ` G"
      using Class_is_Left_Coset by blast
  next
    assume "A ∈ (λg. g ⋅| K) ` G"
    then obtain g where "g ∈ G" "A = g ⋅| K" by blast
    then have "A = Class g" using Class_is_Left_Coset by simp
    then show "A ∈ Factor_Group"
      using Class_in_Partition ‹g ∈ G› by simp
  qed
qed

lemma Factor_Group_eq_Right_Cosets:
  "Factor_Group = (λg. K |⋅ g) ` G"
  by (simp add: Right_Coset_Class_unit natural.surjective)

lemma Class_cardinality:
  assumes "g ∈ G"
  shows "card (Class g) = card K"
proof -
  have "Class g = g ⋅| K" using Class_is_Left_Coset assms by simp
  also have "… = K |⋅ g" using Left_equals_Right_coset assms by simp
  finally show ?thesis using Right_Coset_cardinality assms by simp
qed

lemma card_Factor_Group:
  assumes "finite G"
  shows "card (Factor_Group) = index"
proof -
  have fin_class: "finite p" if "p ∈ Partition" for p
    by (metis Class_closed2 assms finite_subset representant_exists that)
  have card_class: "card p = card K" if "p ∈ Partition" for p
    using Class_cardinality representant_exists that by blast
  have "card G = (∑p∈Partition. card p)"
    using product_partition [OF partition fin_class] by simp
  also have "… = (∑p∈Partition. card K)"
    using card_class by simp
  also have "… = card K * card Partition"
    by simp
  finally have "card G = card K * card Partition" .
  moreover have "card G = card K * index"
    using lagrange assms by simp
  moreover have "card K > 0"
    by (metis Normal_def card_eq_0_iff emptyE fin_class gr0I natural.map_closed sub
        sub_unit_closed)
  ultimately have "card K * card Partition = card K * index" by simp
  with ‹card K > 0› have "card Partition = index"
    using nat_mult_eq_cancel1 by simp
  then show ?thesis by simp
qed

lemma quotient_composition_PiE:
  "quotient_composition ∈ Factor_Group →⇩E Factor_Group →⇩E Factor_Group"
proof -
  have "quotient_composition A B ∈ Factor_Group" if "A ∈ Factor_Group" "B ∈ Factor_Group" for A B
    using that by simp
  then show ?thesis
    unfolding quotient_composition_def by (auto simp: restrict_PiE_iff)
qed

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

context subgroup_of_abelian_group begin

lemma quotient_abelian: "Abelian_Group Factor_Group quotient_composition (Class 𝟭)"
proof -
  have comm: "quotient_composition X Y = quotient_composition Y X"
    if XF: "X ∈ Factor_Group" and YF: "Y ∈ Factor_Group" for X Y
  proof -
    obtain a where aG: "a ∈ G" and Xa: "X = Class a"
      using representant_exists XF by blast
    obtain b where bG: "b ∈ G" and Yb: "Y = Class b"
      using representant_exists YF by blast
    have "X [⋅] Y = Class (a ⋅ b)"
      using aG bG by (simp add: Xa Yb Class_commutes_with_composition)
    also have "… = Class (b ⋅ a)"
      using commutative aG bG by presburger
    also have "… = Y [⋅] X"
      using aG bG by (simp add: Xa Yb Class_commutes_with_composition)
    finally show ?thesis .
  qed
  show ?thesis
    unfolding Abelian_Group_def commutative_monoid_def commutative_monoid_axioms_def
    using quotient.Group_axioms quotient.Monoid_axioms comm by auto
qed

end

subsection ‹Homomorphisms›

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)"
  by (metis invertible_image_lemma map_closed
      source.invertible_inverse_closed target.inverse_equality)

end (* Monoid_homomorphism *)

text ‹p 60, ll 32--34; p 61, l 1›
sublocale Monoid_congruence 
  ⊆ natural: Monoid_homomorphism "Class" M "(⋅)" 𝟭 "M / E" "([⋅])" "Class 𝟭"
proof
qed (auto simp add: 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'" "(⋅')" "𝟭'"
proof
  fix x y
  assume "x ∈ Partition" and "y ∈ Partition"
  then show "induced (x [⋅] y) = induced x ⋅' induced y"
    by (metis commutes_with_composition induced_Fiber_simp
        natural.commutes_with_composition representant_exists
        source.composition_closed)
next
  show "induced (Class 𝟭) = 𝟭'"
    by (simp add: commutes_with_unit)
qed

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 $G/L$"›
text ‹p 62, ll 23--24›
sublocale natural: group_epimorphism contained.Class G "(⋅)" 𝟭 "contained.Factor_Group" "([⋅])" "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 ∈ contained.Factor_Group. THE b. ∃a ∈ G. a ⋅| L = A ∧ b = η a)"

text ‹p 62, ll 26--27›
lemma induced_closed [intro, simp]:
  assumes [simp]: "A ∈ contained.Factor_Group" 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 ∉ contained.Factor_Group ⟹ 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 contained.Factor_Group ([⋅]) (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 "contained.Factor_Group" "([⋅])" "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: "β ∈ contained.Factor_Group →⇩E G'"
    and factorization: "compose G β contained.Class = η"
  shows "β = induced"
proof
  fix A
  show "β A = induced A"
  proof (cases "A ∈ contained.Factor_Group")
    case True
    then obtain a where [simp]: "A = contained.Class a" "a ∈ G"
      by (meson contained.representant_exists)
    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 ` contained.Factor_Group = η ` 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 contained.Factor_Group ⟷ L = Ker"
proof -
  have "L = Ker"
    if "L.Partition = {L}"
    using that L.Class_Union L.natural.map_closed by auto
  moreover have "L.Partition ⊆ {Ker}" if "L = Ker"
    by (metis L.ClassD L.Class_eq L.Normal_def L.representant_exists
        contained.sub_unit_closed insert_iff subsetI that)
  moreover have "{Ker} ⊆ L.Partition" if "L = Ker"
    using that L.Normal_def L.quotient.unit_closed by auto
  ultimately show ?thesis
    by (auto simp add: induced.injective_iff_kernel_unit induced_kernel contained.Class_unit_normal_subgroup)
qed

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 (⋅) 𝟭"
proof
qed (use commutes_with_composition commutes_with_unit bij_betw_inverse surjective in 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)

lemma isomorphic_as_groups_transitive:
  assumes "(G, composition, unit) ≅⇩G (G', composition', unit')"
    and "(G', composition', unit') ≅⇩G (G'', composition'', unit'')"
  shows "(G, composition, unit) ≅⇩G (G'', composition'', unit'')"
proof -
  obtain η where first:
    "group_isomorphism η G composition unit G' composition' unit'"
    using assms(1) unfolding isomorphic_as_groups_def by auto
  obtain θ where second:
    "group_isomorphism θ G' composition' unit' G'' composition'' unit''"
    using assms(2) unfolding isomorphic_as_groups_def by auto
  interpret first: group_isomorphism η G composition unit G' composition' unit' by fact
  interpret second: group_isomorphism θ G' composition' unit' G'' composition'' unit'' by fact
  have composite:
    "group_isomorphism (restrict (θ ∘ η) G)
      G composition unit G'' composition'' unit''"
  proof
    show "restrict (θ ∘ η) G ∈ G →⇩E G''"
      using first.graph second.graph by auto
    show "restrict (θ ∘ η) G (composition x y) =
          composition'' (restrict (θ ∘ η) G x)
            (restrict (θ ∘ η) G y)"
      if "x ∈ G" "y ∈ G" for x y
      using that first.commutes_with_composition second.commutes_with_composition
        first.source.composition_closed by auto
    show "restrict (θ ∘ η) G unit = unit''"
      using first.commutes_with_unit second.commutes_with_unit first.source.unit_closed by simp
    have "bij_betw (θ ∘ η) G G''"
      using first.bijective second.bijective by (rule bij_betw_trans)
    then show "bij_betw (restrict (θ ∘ η) G) G G''"
      by (simp add: bij_betw_restrict_eq)
  qed
  show ?thesis unfolding isomorphic_as_groups_def using composite by auto
qed

text ‹On groups the two notions of isomorphism coincide: a bijective monoid isomorphism between
  groups is already a group isomorphism, since @{locale group_homomorphism} adds nothing to
  @{locale Monoid_homomorphism} beyond the two structures being groups.  So isomorphism classes may
  be formed once at the level of monoids without losing the group-level statement.›
lemma isomorphic_as_monoids_iff_groups:
  assumes G: "Group G composition unit" and G': "Group G' composition' unit'"
  shows "(G, composition, unit) ≅⇩M (G', composition', unit')
     ⟷ (G, composition, unit) ≅⇩G (G', composition', unit')"
proof
  assume "(G, composition, unit) ≅⇩M (G', composition', unit')"
  then obtain η where η: "Monoid_isomorphism η G composition unit G' composition' unit'"
    unfolding isomorphic_as_monoids_def by auto
  interpret η: Monoid_isomorphism η G composition unit G' composition' unit' by fact
  interpret source: Group G composition unit by (rule G)
  interpret target: Group G' composition' unit' by (rule G')
  ― ‹The @{locale Monoid_isomorphism} interpretation already supplies the map and bijectivity
    components; only the homomorphism equation is left, and it differs merely in orientation.›
  have "group_isomorphism η G composition unit G' composition' unit'"
    by unfold_locales (simp_all add: η.commutes_with_composition η.commutes_with_unit)
  then show "(G, composition, unit) ≅⇩G (G', composition', unit')"
    unfolding isomorphic_as_groups_def by auto
next
  assume "(G, composition, unit) ≅⇩G (G', composition', unit')"
  then obtain η where "group_isomorphism η G composition unit G' composition' unit'"
    unfolding isomorphic_as_groups_def by auto
  then interpret η: group_isomorphism η G composition unit G' composition' unit' .
  show "(G, composition, unit) ≅⇩M (G', composition', unit')"
    unfolding isomorphic_as_monoids_def
    using η.Monoid_isomorphism_axioms by auto
qed

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 "kernel.Factor_Group" "([⋅])" "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 "kernel.Factor_Group" "([⋅])" "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 / (normal_subgroup.Congruence K G (⋅) 𝟭), composition, unit)"
proof -
  interpret image: group_epimorphism_fundamental where G' = "η ` G"
    by unfold_locales (auto simp: commutes_with_composition)
  have "group_isomorphism image.induced kernel.Factor_Group ([⋅]) (kernel.Class 𝟭) (η ` G) (⋅') 𝟭'" ..
  then have "(η ` G, (⋅'), 𝟭') ≅⇩G (kernel.Factor_Group, ([⋅]), 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

text ‹p 65›
text ‹The First Isomorphism Theorem states that for any group homomorphism @{text "η : G → G'"},
  the quotient @{text "G/ker(η)"} is isomorphic to the image @{text "im(η)"}. The isomorphism is
  given by the induced map @{text "gK ↦ η(g)"}, which is well-defined because elements in the same
  coset of @{text "ker(η)"} have the same image under @{text "η"}.›

theorem first_isomorphism:
  "(kernel.Factor_Group, kernel.quotient_composition, kernel.Class 𝟭) ≅⇩G (η ` G, (⋅'), 𝟭')"
proof -
  ― ‹Restrict the codomain to the image to obtain a surjection.›
  interpret image: group_epimorphism_fundamental η G "(⋅)" 𝟭 "η ` G" "(⋅')" "𝟭'"
    by unfold_locales (auto simp: commutes_with_composition)
  ― ‹The induced map is an isomorphism from @{text "G/ker(η)"} to @{text "im(η)"}.›
  have "group_isomorphism image.induced kernel.Factor_Group kernel.quotient_composition
    (kernel.Class 𝟭) (η ` G) (⋅') 𝟭'" ..
  then show ?thesis
    by (auto simp: isomorphic_as_groups_def)
qed

end (* group_homomorphism *)

subsection ‹Correspondence Theorem and Third Isomorphism Theorem›
text ‹p 65›

text ‹The proofs in this section, in their initial form, were generated by Claude Opus 4.6
through Dominic Mulligan's Isabelle Assistant. Then simplified and tidied by LCP.›

text ‹
  Let @{term K} be a normal subgroup of @{term G} and @{term H} a subgroup of @{term G} containing
  @{term K}. Then @{text "H/K"} is a subgroup of @{text "G/K"}, the map @{text "H ↦ H/K"} is a
  bijection between subgroups of @{term G} containing @{term K} and subgroups of @{text "G/K"},
  @{term H} is normal in @{term G} if and only if @{text "H/K"} is normal in @{text "G/K"}, and
  @{text "G/H ≅ (G/K)/(H/K)"}.
›

locale normal_subgroup_in_subgroup =
  K: normal_subgroup K G "(⋅)" 𝟭 +
  H: subgroup_of_group H G "(⋅)" 𝟭
  for K and H and G and composition (infixl ‹⋅› 70) and unit (‹𝟭›) +
  assumes K_contained: "K ⊆ H"
begin

interpretation K_subgroup_H: Subgroup K H "(⋅)" 𝟭
proof qed (use K_contained in auto)

text ‹@{term K} is a normal subgroup of @{term H}.›
interpretation K_in_H: normal_subgroup K H "(⋅)" 𝟭
proof
  show "⋀g k. ⟦g ∈ H; k ∈ K⟧ ⟹ H.sub.inverse g ⋅ k ⋅ g ∈ K"
    by (metis K.normal H.sub H.subgroup_inverse_equality)
qed

notation K.quotient_composition (infixl ‹[⋅]› 70)

text ‹@{text "H/K"} as a subset of @{text "G/K"}, defined as the image of @{term H} under the
  canonical projection.›

definition "Fract_H_K = K.Class ` H"

text ‹One might expect the quotient $H/K$ to be @{term "K.Factor_Group"} with @{term H} in place of
  @{term G}. However, @{term K.Factor_Group} always forms the congruence of @{term K}
  relative to @{term G} (not @{term H}), so substituting @{term H} for the carrier would give
  @{term "Equivalence.Partition H K.Congruence"}. Since @{term K.Congruence} is an equivalence on
  @{term G} rather than @{term H}, the conditional defining equation of @{const Equivalence.Partition}
  cannot be applied, leaving the term opaque.

  The correct formalisation of $H/K$ is @{term K_in_H.Partition}, the partition of @{term H} under
  @{term K_in_H.Congruence}---the congruence of @{term K} viewed as a normal subgroup of @{term H}.
  The proof that @{term Fract_H_K} equals @{term K_in_H.Partition} follows from the fact that @{term K.Class}
  and @{term K_in_H.Class} agree on elements of @{term H}: both map $h \in H$ to the left coset
  $hK$, by @{thm [source] K.Class_is_Left_Coset} and @{thm [source] K_in_H.Class_is_Left_Coset}.›

lemma H_Class_eq: "h ∈ H ⟹ K_in_H.Class h = K.Class h"
  using K.Left_Coset_Class_unit K_in_H.Left_Coset_Class_unit by force

lemma Fract_H_K_is_quotient: "Fract_H_K = K_in_H.Partition"
  by (auto simp: Fract_H_K_def K_in_H.Partition_def H_Class_eq)

lemma Fract_H_K_subset: "Fract_H_K ⊆ K.Factor_Group"
  unfolding Fract_H_K_def by blast

lemma Class_H_closed [intro, simp]:
  "h ∈ H ⟹ K.Class h ∈ Fract_H_K"
  unfolding Fract_H_K_def by auto

lemma Fract_H_K_unit_closed [intro, simp]:
  "K.Class 𝟭 ∈ Fract_H_K"
  using H.sub_unit_closed by auto

lemma Fract_H_K_memE [elim]:
  "⟦ A ∈ Fract_H_K; ⋀h. ⟦ h ∈ H; A = K.Class h ⟧ ⟹ P ⟧ ⟹ P"
  unfolding Fract_H_K_def by auto

text ‹@{text "H/K"} is a subgroup of @{text "G/K"}.›

lemma Fract_H_K_into_subset_H: "h ∈ Fract_H_K ⟹ h ⊆ H"
  using Fract_H_K_is_quotient K_in_H.natural.surjective by blast

theorem Fract_H_K_subgroup: "Subgroup Fract_H_K K.Factor_Group ([⋅]) (K.Class 𝟭)"
proof (rule K.quotient.subgroupI)
  show "Fract_H_K ⊆ K.Factor_Group" by (rule Fract_H_K_subset)
next
  fix A
  assume "A ∈ Fract_H_K"
  then obtain a where a: "a ∈ H" "A = K.Class a" by auto
  then show "K.quotient.invertible A"
    using K.Class_invertible H.sub by auto
  show "K.quotient.inverse A ∈ Fract_H_K"
    using a by (simp add: K.Class_commutes_with_inverse)
qed (use K.Class_commutes_with_composition in fastforce)+

sublocale Fract_H_K: subgroup_of_group Fract_H_K "K.Factor_Group" "([⋅])" "K.Class 𝟭"
  by (simp add: Fract_H_K_subgroup K.quotient.Group_axioms subgroup_of_group_def)

text ‹@{term H} is normal in @{term G} if and only if $H/K$ is normal in $G/K$.›
theorem normal_iff:
  "normal_subgroup H G (⋅) 𝟭 ⟷ normal_subgroup Fract_H_K K.Factor_Group ([⋅]) (K.Class 𝟭)"
proof
  assume "normal_subgroup H G (⋅) 𝟭"
  then interpret H_normal: normal_subgroup H G "(⋅)" 𝟭 .
  show "normal_subgroup Fract_H_K K.Factor_Group ([⋅]) (K.Class 𝟭)"
  proof 
    fix A B
    assume A: "A ∈ K.Factor_Group" and B: "B ∈ Fract_H_K"
    then obtain g h where g: "g ∈ G" "A = K.Class g"
                      and h: "h ∈ H" "B = K.Class h" 
         by (meson K.representant_exists Fract_H_K_memE)
    have "K.quotient.inverse A = K.Class (K.inverse g)"
      using g K.Class_commutes_with_inverse by auto
    then have eq: "K.quotient.inverse A [⋅] B [⋅] A = K.Class (K.inverse g ⋅ h ⋅ g)"
      using g h K.Class_commutes_with_composition by force
    have "K.inverse g ⋅ h ⋅ g ∈ H" using H_normal.normal g h by auto
    then show "K.quotient.inverse A [⋅] B [⋅] A ∈ Fract_H_K"
      unfolding eq by auto
  qed
next
  assume Fract_H_K_normal: "normal_subgroup Fract_H_K K.Factor_Group ([⋅]) (K.Class 𝟭)"
  then interpret Fract_H_K_normal: normal_subgroup Fract_H_K "K.Factor_Group" "([⋅])" "K.Class 𝟭" .
  show "normal_subgroup H G (⋅) 𝟭"
  proof 
    fix g h
    assume g: "g ∈ G" and h: "h ∈ H"
    then have A: "K.Class g ∈ K.Factor_Group" and B: "K.Class h ∈ Fract_H_K" by auto
    have "K.quotient.inverse (K.Class g) [⋅] K.Class h [⋅] K.Class g
        = K.Class (K.inverse g ⋅ h ⋅ g)"
      using K.Class_commutes_with_inverse K.natural.commutes_with_composition g h by auto
    with Fract_H_K_normal.normal [OF A B] 
    obtain h' where h': "h' ∈ H" "K.Class (K.inverse g ⋅ h ⋅ g) = K.Class h'"
      by (metis Fract_H_K_memE)
    then have "(K.inverse g ⋅ h ⋅ g, h') ∈ K.Congruence"
      using g h H.sub K.Class_equivalence by auto
    then obtain k where k: "k ∈ K" "K.inverse g ⋅ h ⋅ g = h' ⋅ k"
      using K.CongruenceD by auto
    show "K.inverse g ⋅ h ⋅ g ∈ H"
      using k h' K_contained H.sub_composition_closed by auto
  qed
qed

text ‹Third Isomorphism Theorem: @{text "G/H ≅ (G/K)/(H/K)"}›

text ‹We assume @{term H} is normal in @{term G} and construct a surjective group homomorphism
  from @{text "G/K"} to @{text "G/H"} whose kernel is @{text "H/K"}.›

theorem third_isomorphism:
  assumes H_normal: "normal_subgroup H G (⋅) 𝟭"
  defines "CongH ≡ normal_subgroup.Congruence H G (⋅) 𝟭"
    and "CongHK ≡ normal_subgroup.Congruence Fract_H_K K.Factor_Group K.quotient_composition (K.Class 𝟭)"
  shows "(G / CongH,
          Monoid_congruence.quotient_composition G (⋅) CongH,
          Equivalence.Class G CongH 𝟭) ≅⇩G
         (K.Factor_Group / CongHK,
          Monoid_congruence.quotient_composition K.Factor_Group K.quotient_composition CongHK,
          Equivalence.Class K.Factor_Group CongHK (K.Class 𝟭))"
proof -
  interpret Hn: normal_subgroup H G "(⋅)" 𝟭 
    by (rule H_normal)

  ― ‹The canonical map, sending ‹K.Class g› to ‹Hn.Class g›; the
      description operator is discharged by well-definedness below.›
  define φ where "φ = (λA ∈ K.Factor_Group. THE B. ∃g ∈ G. A = K.Class g ∧ B = Hn.Class g)"

  have φ_eq: "φ (K.Class g) = Hn.Class g" if g: "g ∈ G" for g
    proof -
    have unfold: "φ (K.Class g) = (THE B. ∃g'∈G. K.Class g = K.Class g' ∧ B = Hn.Class g')"
      unfolding φ_def using g by simp
    ― ‹Well defined because ‹K ⊆ H›: elements in one ‹K›-coset lie in one
        ‹H›-coset.›
    have well_def: "(THE B. ∃g'∈G. K.Class g = K.Class g' ∧ B = Hn.Class g') = Hn.Class g"
    proof (rule the_equality)
      fix B assume "∃g'∈G. K.Class g = K.Class g' ∧ B = Hn.Class g'"
      with g obtain g' k where g': "g' ∈ G" and eq: "K.Class g = K.Class g'" and B: "B = Hn.Class g'"
        and "(g, g') ∈ K.Congruence" and "g = g' ⋅ k" and "k ∈ K"
        by (meson K.CongruenceD K.Class_equivalence)
      then have "(g, g') ∈ Hn.Congruence"
        using g g' K_contained by (auto intro: Hn.CongruenceI)
      with B show "B = Hn.Class g"
        using Hn.Class_eq by presburger
    qed (use g in blast)
    show "φ (K.Class g) = Hn.Class g"
      by (simp add: unfold well_def)
  qed

  interpret gh: group_homomorphism φ "K.Factor_Group" "([⋅])" "K.Class 𝟭" "Hn.Factor_Group" "Hn.quotient_composition" "Hn.Class 𝟭"
  proof 
    show "φ ∈ K.Partition →⇩E Hn.Partition"
    proof (rule PiE_I)
      fix A assume "A ∈ K.Partition"
      then show "φ A ∈ Hn.Partition"
        by (metis Hn.natural.map_closed φ_eq K.representant_exists)
    qed (auto simp: φ_def)
  next
    fix A B assume A: "A ∈ K.Partition" and B: "B ∈ K.Partition"
    then obtain a b where a: "a ∈ G" and A_eq: "A = K.Class a" 
      and b: "b ∈ G" and B_eq: "B = K.Class b"
        using K.representant_exists by meson
      have "φ (A [⋅] B) = φ (K.Class (a ⋅ b))"
        by (simp add: A_eq B_eq a b K.Class_commutes_with_composition)
      also have "… = Hn.Class (a ⋅ b)"
        using a b by (simp add: φ_eq)
      also have "… = Hn.quotient_composition (φ A) (φ B)"
        using A_eq B_eq Hn.natural.commutes_with_composition φ_eq a b by presburger
      finally show "φ (A [⋅] B) = Hn.quotient_composition (φ A) (φ B)" .
  next
    show "φ (K.Class 𝟭) = Hn.Class 𝟭"
      by (simp add: φ_eq)
  qed

  have φ_surj: "φ ` K.Factor_Group = Hn.Factor_Group"
    using Hn.representant_exists φ_eq by blast

  have φ_ker: "gh.Ker = Fract_H_K"
  proof (intro equalityI subsetI)
    fix A assume A_ker: "A ∈ gh.Ker"
    then have "A ∈ K.Factor_Group" and φ_A: "φ A = Hn.Class 𝟭"
      by (auto simp: gh.Ker_def)
    then obtain g where g: "g ∈ G" and A_eq: "A = K.Class g"
      by (meson K.representant_exists)
    then have "(g, 𝟭) ∈ Hn.Congruence"
      using g Hn.Class_equivalence φ_A φ_eq by force
    then show "A ∈ Fract_H_K"
      using A_eq Hn.CongruenceD by blast
  next
    fix A assume "A ∈ Fract_H_K"
    then obtain h where h: "h ∈ H" and A_eq: "A = K.Class h"
      by auto
    then have "(h, 𝟭) ∈ Hn.Congruence"
      using Hn.Normal_def h by blast
    then have "φ A = Hn.Class 𝟭"
      by (simp add: A_eq Hn.Class_eq φ_eq h)
    then show "A ∈ gh.Ker"
      using ‹A ∈ Fract_H_K› by blast
  qed
  show ?thesis
    unfolding CongHK_def CongH_def
    by (metis φ_ker φ_surj gh.first_isomorphism isomorphic_as_groups_symmetric)
qed

end (* normal_subgroup_in_subgroup *)

text ‹
  The product of a subgroup and a normal subgroup is again a subgroup.  We keep
  the construction set-based, in keeping with the rest of this development,
  and package its closure facts in a locale so that later isomorphism theorems
  can use the product as an ambient group in its own right.
›
locale normal_subgroup_product =
  K: normal_subgroup K G "(⋅)" 𝟭 +
  H: subgroup_of_group H G "(⋅)" 𝟭
  for K and H and G and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
begin

definition HK where "HK ≡ (case_prod(⋅)) ` (H × K)"

lemma HK_memI:
  "⟦h ∈ H; k ∈ K⟧ ⟹ h ⋅ k ∈ HK"
  unfolding HK_def by blast

lemma HK_memE:
  assumes "x ∈ HK"
  obtains h k where "h ∈ H" "k ∈ K" "x = h ⋅ k"
proof -
  from assms obtain p where p: "p ∈ H × K" "x = case_prod (⋅) p"
    unfolding HK_def by blast
  obtain h k where "p = (h,k)" by (cases p)
  then have "h ∈ H" "k ∈ K" "x = h ⋅ k"
    using p by simp_all
  then show thesis by (rule that)
qed

lemma HK_eq_KH: "HK = (case_prod(⋅)) ` (K × H)"
  using H.subset HK_def K.set_prod_commute by presburger

interpretation HK_mon: Monoid HK
proof
  fix a b
  assume "a ∈ HK" and "b ∈ HK"
  then have "∃hb kb. h ⋅ k ⋅ (ha ⋅ ka) = hb ⋅ kb ∧ hb ∈ H ∧ kb ∈ K"
    if "h ∈ H" "k ∈ K" "ha ∈ H" "ka ∈ K" for h ha k ka
  proof -
    have hG: "h ∈ G" and haG: "ha ∈ G" using that H.sub by auto
    have kG: "k ∈ G" and kaG: "ka ∈ G" using that K.sub by auto
    have "k ⋅ ha ∈ (case_prod(⋅)) ` (K × H)"
      using that by auto
    then have "k ⋅ ha ∈ HK"
      using HK_eq_KH by simp
    then obtain h' k' where hk': "k ⋅ ha = h' ⋅ k'" "h' ∈ H" "k' ∈ K"
      by (auto simp: HK_def)
    have "h ⋅ k ⋅ (ha ⋅ ka) = h ⋅ (k ⋅ ha) ⋅ ka"
      by (simp add: K.associative hG haG kG kaG)
    also have "… = (h ⋅ h') ⋅ (k' ⋅ ka)"
      using ‹k ⋅ ha = h' ⋅ k'› by (simp add: K.associative hG hk' kaG)
    finally have eq: "h ⋅ k ⋅ (ha ⋅ ka) = (h ⋅ h') ⋅ (k' ⋅ ka)" .
    then show ?thesis
      using hk' ‹h ∈ H› ‹ka ∈ K› by blast
  qed
  then show "a ⋅ b ∈ HK"
    using HK_def ‹a ∈ HK› ‹b ∈ HK› by force
qed (force simp: HK_def)+

interpretation HK_sub: Subgroup HK G
proof
  fix a assume a: "a ∈ HK"
  then show "⋀b. b ∈ HK ⟹ a ⋅ b ∈ HK"
    by blast
  obtain h k where hk: "h ∈ H" "k ∈ K" "a = k⋅h"
    using HK_eq_KH a by auto
  define a' where "a' ≡ H.sub.inverse h ⋅ K.sub.inverse k"
  have "a' ∈ HK"
    using HK_def a'_def hk by auto
  have "a ⋅ a' = 𝟭"
    using hk unfolding a'_def
    by (metis H.sub H.subgroup_inverse_equality K.composition_closed K.inverse_composition_commute
        K.invertible K.invertible_right_inverse K.sub K.subgroup_inverse_equality)
  moreover have "a' ⋅ a = 𝟭"
    unfolding ‹a = k⋅h› a'_def
    by (metis H.sub H.subgroup_inverse_equality K.composition_closed K.inverse_composition_commute
        K.invertible K.invertible_left_inverse K.sub K.subgroup_inverse_equality hk)
  moreover have "a' ∈ HK"
    using hk by (auto simp: a'_def HK_def)
  ultimately show "Monoid.invertible HK (⋅) 𝟭 a"
    using HK_mon.invertibleI by blast
qed (force simp: HK_def)+

lemma HK_subgroup: "Subgroup HK G (⋅) 𝟭"
  ..

lemma H_subset_HK: "H ⊆ HK"
  unfolding HK_def
  using K.sub_unit_closed H.sub by force

lemma K_subset_HK: "K ⊆ HK"
  unfolding HK_def
  using H.sub_unit_closed K.sub by force

end (* normal_subgroup_product *)

locale second_iso_theorem = normal_subgroup_product K H G "(⋅)" 𝟭
  for K and H and G and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
begin

interpretation HIntK_Mon: Monoid "H ∩ K" 
proof qed auto

interpretation HIntKn: normal_subgroup "H ∩ K" H
proof
  fix u :: 'a
  assume "u ∈ H ∩ K"
  then have uH: "u ∈ H" and uK: "u ∈ K" by auto
  then have inv_H: "H.sub.inverse u ∈ H"
    using H.sub.invertible H.sub.invertible_inverse_closed by auto
  have "H.sub.inverse u = K.sub.inverse u"
    by (metis H.subgroup_inverse_equality K.subgroup_inverse_equality uH uK)
  then show "Monoid.invertible (H ∩ K) (⋅) 𝟭 u"
    using inv_H uK by force
  fix g 
  assume "g ∈ H" 
  then show "H.sub.inverse g ⋅ u ⋅ g ∈ H ∩ K"
    by (metis H.sub H.sub.invertible H.sub_composition_closed H.subgroup_inverse_equality
        H.submonoid_inverse_closed Int_iff K.normal uH uK)
qed auto

text ‹Defining the quotient groups as sets of equivalence classes›
definition "Fract_HK_K ≡ K.Class ` HK"
definition "Fract_H_HIntK ≡ HIntKn.Class ` H"
definition φ where "φ ≡ (λA ∈ Fract_HK_K. THE B. ∃g ∈ HK. A = K.Class g ∧ B = HIntKn.Class g)"


theorem second_isomorphism: 
  shows "(Fract_HK_K, K.quotient_composition, K.Class 𝟭) ≅⇩G
         (Fract_H_HIntK, HIntKn.quotient_composition, HIntKn.Class 𝟭)"
proof -
  define η where "η = (λh ∈ H. K.Class h)"

  interpret gh: group_homomorphism η H "(⋅)" 𝟭 "K.Factor_Group" K.quotient_composition "K.Class 𝟭"
  proof
    show "η ∈ H →⇩E K.Partition"
      by (simp add: η_def)
  next
    fix x y assume xy: "x ∈ H" "y ∈ H"
    then show "η (x ⋅ y) = K.quotient_composition (η x) (η y)"
      by (simp add: K.natural.commutes_with_composition η_def)
  next
    show "η 𝟭 = K.Class 𝟭"
      unfolding η_def using H.sub_unit_closed by simp
  qed

  have image_eq: "η ` H = Fract_HK_K"
  proof (intro equalityI subsetI)
    fix A assume "A ∈ η ` H"
    then obtain h where h: "h ∈ H" "A = η h" by auto
    then have "A = K.Class h" unfolding η_def by simp
    moreover have "h ∈ HK"
      unfolding HK_def using h(1) K.sub_unit_closed H.sub
      by (force intro: image_eqI[where x="(h, 𝟭)"])
    ultimately show "A ∈ Fract_HK_K"
      unfolding Fract_HK_K_def by auto
  next
    fix A assume "A ∈ Fract_HK_K"
    then obtain a where a: "a ∈ HK" "A = K.Class a"
      unfolding Fract_HK_K_def by auto
    then obtain h k where hk: "h ∈ H" "k ∈ K" "a = h ⋅ k"
      unfolding HK_def by auto
    have "K.Class a = K.Class h"
      using hk H.sub K.sub
      by (meson K.Class_eq K.CongruenceI K.composition_closed)
    then have "A = η h" using a hk unfolding η_def by simp
    then show "A ∈ η ` H" using hk(1) by auto
  qed

  have ker_eq: "gh.Ker = H ∩ K"
  proof (intro equalityI subsetI)
    fix h assume "h ∈ gh.Ker"
    then have hH: "h ∈ H" and "η h = K.Class 𝟭"
      using ‹h ∈ gh.Ker› gh.Ker_image by blast+
    then have "K.Class h = K.Class 𝟭"
      unfolding η_def by simp
    then have "(h, 𝟭) ∈ K.Congruence"
      using hH H.sub K.Class_equivalence by simp
    then have "h ∈ K"
      using K.CongruenceD by blast
    with hH show "h ∈ H ∩ K" by auto
  next
    fix h assume "h ∈ H ∩ K"
    then have hH: "h ∈ H" and hK: "h ∈ K" by auto
    have "η h = K.Class h" unfolding η_def using hH by simp
    also have "… = K.Class 𝟭"
      by (metis K.Class_eq K.CongruenceI K.left_unit K.sub K.unit_closed hK)
    finally show "h ∈ gh.Ker" 
      using hH by blast
  qed

  ― ‹The kernel's congruence and quotient agree with HIntKn's.›
  ― ‹Apply the first isomorphism theorem.›
  have "(gh.kernel.Partition, gh.kernel.quotient_composition, gh.kernel.Class 𝟭) ≅⇩G
        (η ` H, K.quotient_composition, K.Class 𝟭)"
    using gh.first_isomorphism by simp
  then have "(Fract_H_HIntK, HIntKn.quotient_composition, HIntKn.Class 𝟭) ≅⇩G
             (Fract_HK_K, K.quotient_composition, K.Class 𝟭)"
    unfolding image_eq Fract_H_HIntK_def ker_eq by (simp add: HIntKn.Partition_def)
  then show ?thesis
    by (rule isomorphic_as_groups_symmetric)
qed


end (*first_iso_theorem*)

subsection ‹Dropping from elements of a partition to representatives›

text ‹This prevents a change of type for inductive proofs that involve quotienting.›

locale class_representatives =
  fixes A:: "'a set" and P and composition (infixl ‹⋅› 70) and unit (‹𝟭›)
  assumes P: "partition_on A P"
  assumes comp: "(⋅) ∈ P →⇩E P →⇩E P"
  assumes unit: "𝟭 ∈ P "
begin

definition the_part :: "'a ⇒ 'a set" where
  "the_part x ≡ THE X. X ∈ P ∧ x ∈ X"

definition rep_comp :: "'a ⇒ 'a ⇒ 'a" where
  "rep_comp ≡ λx∈A. λy∈A. some_elem ((the_part x) ⋅ (the_part y))"

lemma some_elem_typing: "X ∈ P ⟹ some_elem X ∈ A"
  by (metis P UnionI partition_on_def some_elem_nonempty)

lemma the_part_works:
  assumes "x ∈ A" shows "x ∈ the_part x" "the_part x ∈ P"
proof -
  obtain X where X: "x ∈ X" "X ∈ P"
    using P assms by (metis UnionE partition_on_def)
  moreover have "Y = X" if "x ∈ Y" "Y ∈ P" for Y
    using P X
    by (metis (no_types, lifting) IntI disjoint_def emptyE partition_on_def that)
  ultimately have "x ∈ the_part x ∧ the_part x ∈ P"
    by (metis (mono_tags, lifting) theI_unique the_part_def)
  then show "x ∈ the_part x" "the_part x ∈ P"
    by auto
qed

lemma typing: "⟦x ∈ A; y ∈ A⟧ ⟹ some_elem (the_part x ⋅ the_part y) ∈ A"
  by (metis some_elem_typing PiE_E comp the_part_works(2))

lemma unit_typing: "some_elem 𝟭 ∈ A"
  by (simp add: some_elem_typing unit)

lemma rep_comp_typing: "rep_comp ∈ A →⇩E (A →⇩E A)"
  by (simp add: rep_comp_def typing)

lemma the_part_some_elem [simp]:
  assumes "X ∈ P"
  shows "the_part (some_elem X) = X"
proof -
  have "disjoint P"
    using P partition_on_def by blast
  moreover
  have "X ≠ {}"
    using assms P partition_on_def by blast
  ultimately show ?thesis
    using assms by (simp add: pairwise_disjnt_iff some_elem_nonempty the1_equality' the_part_def)
qed

lemma rep_comp: "⟦X ∈ P; Y ∈ P⟧ ⟹ rep_comp (some_elem X) (some_elem Y) = some_elem (X ⋅ Y)"
  by (simp add: rep_comp_def some_elem_typing)

lemma Monoid_class_reps:
  assumes "Monoid P (⋅) 𝟭"
  shows "Monoid (some_elem ` P) rep_comp (some_elem 𝟭)"
proof -
  interpret Monoid P
    by (simp add: assms)
  show ?thesis
  proof  qed (use rep_comp associative in auto)
qed

lemma Group_class_reps:
  assumes "Group P (⋅) 𝟭"
  shows "Group (some_elem ` P) rep_comp (some_elem 𝟭)"
proof -
  interpret Group P
    by (simp add: assms)
  interpret Mr: Monoid "some_elem ` P" rep_comp "some_elem 𝟭"
    by (simp add: Monoid_axioms Monoid_class_reps)
  have "⋀x. x ∈ P ⟹ Mr.invertible (some_elem x)"
    by (metis Mr.invertible_def image_eqI invertible invertible_def
        rep_comp)
  then show ?thesis
  proof unfold_locales qed auto
qed

lemma some_elem_inj_on: "inj_on some_elem P"
  by (rule inj_on_inverseI [where g = the_part]) simp

lemma some_elem_bij_betw: "bij_betw some_elem P (some_elem ` P)"
  using some_elem_inj_on by (simp add: bij_betw_def)

lemma Monoid_iso_class_reps:
  assumes "Monoid P (⋅) 𝟭"
  shows "Monoid_isomorphism (restrict some_elem P) P (⋅) 𝟭 (some_elem ` P) rep_comp (some_elem 𝟭)"
proof -
  interpret Monoid P
    by (simp add: assms)
  show ?thesis
    by unfold_locales
      (auto simp: Monoid_class_reps assms some_elem_bij_betw some_elem_typing rep_comp associative
        bij_betw_restrict_eq)
qed

lemma group_iso_class_reps:
  assumes "Group P (⋅) 𝟭"
  shows "group_isomorphism (restrict some_elem P) P (⋅) 𝟭 (some_elem ` P) rep_comp (some_elem 𝟭)"
proof -
  interpret Monoid_isomorphism "restrict some_elem P" P "(⋅)" 𝟭 "some_elem ` P" rep_comp "some_elem 𝟭"
    by (rule Monoid_iso_class_reps) (simp add: assms Group.axioms)
  show ?thesis
  proof
    show "⋀u. u ∈ P ⟹ invertible u"
      by (simp add: Group.invertible assms)
    show "⋀u. u ∈ some_elem ` P ⟹ invertible' u"
      by (meson Group.invertible Group_class_reps assms)
  qed
qed

lemma abelian_group_class_reps:
  assumes "Abelian_Group P (⋅) 𝟭"
  shows "Abelian_Group (some_elem ` P) rep_comp (some_elem 𝟭)"
proof -
  interpret Abelian_Group P "(⋅)" 𝟭 by (rule assms)
  have comm: "rep_comp (some_elem X) (some_elem Y) = rep_comp (some_elem Y) (some_elem X)"
    if "X ∈ P" "Y ∈ P" for X Y
    using that by (simp add: rep_comp commutative)
  show ?thesis
    unfolding Abelian_Group_def commutative_monoid_def commutative_monoid_axioms_def
    using Group_class_reps[OF Group_axioms] Group.axioms comm by auto
qed

end



context normal_subgroup begin

interpretation reps: class_representatives G Factor_Group quotient_composition "Class 𝟭"
proof 
  show "partition_on G Factor_Group"
    by (rule partition)
  show "quotient_composition ∈ Factor_Group →⇩E Factor_Group →⇩E Factor_Group"
    by (rule quotient_composition_PiE)
  show "Class 𝟭 ∈ Factor_Group"
    by simp
qed

theorem group_isomorphism_Factor_Group_class_reps:
  "group_isomorphism
    (restrict some_elem Factor_Group) Factor_Group quotient_composition (Class 𝟭)
    (some_elem ` Factor_Group) reps.rep_comp (some_elem (Class 𝟭))"
  by (rule reps.group_iso_class_reps) (rule quotient.Group_axioms)

lemma card_class_reps:
  "card (some_elem ` Factor_Group) = card Factor_Group"
  using reps.some_elem_inj_on card_image by blast

lemma class_reps_subset: "some_elem ` Factor_Group ⊆ G"
  using reps.some_elem_typing by auto

lemma abelian_class_reps:
  assumes "Abelian_Group Factor_Group quotient_composition (Class 𝟭)"
  shows "Abelian_Group (some_elem ` Factor_Group) reps.rep_comp (some_elem (Class 𝟭))"
  using reps.abelian_group_class_reps[OF assms] .


end (* normal_subgroup *)



subsection ‹Abstract type of monoids›

lemma trivial_Monoid: "Monoid {undefined} (λx y. undefined) undefined"
  by (auto simp: Monoid_def)

lemma trivial_Monoid_invertible: 
  "Monoid.invertible {undefined} (λx y. undefined) undefined undefined"
  by (simp add: Monoid.unit_invertible trivial_Monoid)

lemma trivial_Group: "Group {undefined} (λx y. undefined) undefined"
  by (simp add: Group_axioms_def Group_def trivial_Monoid
      trivial_Monoid_invertible)

typedef 'a monoid = "{(M::'a set,f,e). Monoid M f e}"
  morphisms "dest_monoid" "monoid"
  using trivial_Monoid  by blast

declare dest_monoid_inverse [simp]

definition "trivial_monoid ≡ monoid ({undefined}, (λx y. undefined), undefined)"

definition mcarrier where "mcarrier m ≡ fst (dest_monoid m)"

definition mmult where "mmult m ≡ fst (snd (dest_monoid m))"

definition munit where "munit m ≡ snd (snd (dest_monoid m))"

lemma monoid_is_Monoid [iff]: "Monoid (mcarrier m) (mmult m) (munit m)"
  by (metis Product_Type.Collect_case_prodD dest_monoid mcarrier_def
      mem_Collect_eq munit_def mmult_def)

lemma mmult_assoc [simp]:
  "⟦ a ∈ mcarrier m; b ∈ mcarrier m; c ∈ mcarrier m ⟧ ⟹ mmult m (mmult m a b) c = mmult m a (mmult m b c)"
  by (meson Monoid.associative monoid_is_Monoid)

lemma m_left_unit: "a ∈ mcarrier m ⟹ mmult m (munit m) a = a"
  by (meson Monoid.left_unit monoid_is_Monoid)

lemma m_right_unit: "a ∈ mcarrier m ⟹ mmult m a (munit m) = a"
  by (meson Monoid.right_unit monoid_is_Monoid)

lemma (in Monoid) mcarrier_monoid[simp]: 
  "mcarrier (monoid (M, (⋅), 𝟭)) = M"
  by (simp add: mcarrier_def Monoid_axioms monoid_inverse)

lemma (in Monoid) mmult_monoid[simp]: 
  "mmult (monoid (M, (⋅), 𝟭)) = (⋅)"
  by (simp add: mmult_def Monoid_axioms monoid_inverse)

lemma (in Monoid) munit_monoid[simp]: 
  "munit (monoid (M, (⋅), 𝟭)) = 𝟭"
  by (simp add: munit_def Monoid_axioms monoid_inverse)

lemma monoid_collapse [simp]: "monoid (mcarrier m, mmult m, munit m) = m"
  by (simp add: mcarrier_def mmult_def munit_def)

text ‹Allows reference to the current monoid space within the locale as a value›
definition (in Monoid) "Self ≡ monoid (M, (⋅), 𝟭)"

lemma (in Monoid) mcarrier_Self [simp]: "mcarrier Self = M"
  by (simp add: Self_def)

lemma (in Monoid) mmult_Self [simp]: "mmult Self = (⋅)"
  by (simp add: Self_def)

lemma (in Monoid) munit_Self [simp]: "munit Self = 𝟭"
  by (simp add: Self_def)


end