# Theory Set_Theory

(* Copyright (c) 2014-2019 by Clemens Ballarin This file is licensed under the 3-clause BSD license. *) theory Set_Theory imports "HOL-Library.FuncSet" begin hide_const map hide_const partition no_notation divide (infixl "'/" 70) no_notation inverse_divide (infixl "'/" 70) text ‹ Each statement in the formal text is annotated with the location of the originating statement in Jacobson's text @{cite Jacobson1985}. Each fact that Jacobson states explicitly is marked as @{command theorem} unless it is translated to a @{command sublocale} declaration. Literal quotations from Jacobson's text are reproduced in double quotes. Auxiliary results needed for the formalisation that cannot be found in Jacobson's text are marked as @{command lemma} or are @{command interpretation}s. Such results are annotated with the location of a related statement. For example, the introduction rule of a constant is annotated with the location of the definition of the corresponding operation. › section ‹Concepts from Set Theory. The Integers› subsection ‹The Cartesian Product Set. Maps› text ‹Maps as extensional HOL functions› text ‹p 5, ll 21--25› locale map = fixes α and S and T assumes graph [intro, simp]: "α ∈ S →⇩_{E}T" begin text ‹p 5, ll 21--25› lemma map_closed [intro, simp]: "a ∈ S ⟹ α a ∈ T" using graph by fast text ‹p 5, ll 21--25› lemma map_undefined [intro]: "a ∉ S ⟹ α a = undefined" using graph by fast end (* map *) text ‹p 7, ll 7--8› locale surjective_map = map + assumes surjective [intro]: "α ` S = T" text ‹p 7, ll 8--9› locale injective_map = map + assumes injective [intro, simp]: "inj_on α S" text ‹Enables locale reasoning about the inverse @{term "restrict (inv_into S α) T"} of @{term α}.› text ‹p 7, ll 9--10› locale bijective = fixes α and S and T assumes bijective [intro, simp]: "bij_betw α S T" text ‹ Exploit existing knowledge about @{term bij_betw} rather than extending @{locale surjective_map} and @{locale injective_map}. › text ‹p 7, ll 9--10› locale bijective_map = map + bijective begin text ‹p 7, ll 9--10› sublocale surjective_map by unfold_locales (simp add: bij_betw_imp_surj_on) text ‹p 7, ll 9--10› sublocale injective_map using bij_betw_def by unfold_locales fast text ‹p 9, ll 12--13› sublocale inverse: map "restrict (inv_into S α) T" T S by unfold_locales (simp add: inv_into_into surjective) text ‹p 9, ll 12--13› sublocale inverse: bijective "restrict (inv_into S α) T" T S by unfold_locales (simp add: bij_betw_inv_into surjective) end (* bijective_map *) text ‹p 8, ll 14--15› abbreviation "identity S ≡ (λx ∈ S. x)" context map begin text ‹p 8, ll 18--20; p 9, ll 1--8› theorem bij_betw_iff_has_inverse: "bij_betw α S T ⟷ (∃β ∈ T →⇩_{E}S. compose S β α = identity S ∧ compose T α β = identity T)" (is "_ ⟷ (∃β ∈ T →⇩_{E}S. ?INV β)") proof let ?inv = "restrict (inv_into S α) T" assume "bij_betw α S T" then have "?INV ?inv" and "?inv ∈ T →⇩_{E}S" by (simp_all add: compose_inv_into_id bij_betw_imp_surj_on compose_id_inv_into bij_betw_imp_funcset bij_betw_inv_into) then show "∃β ∈ T →⇩_{E}S. ?INV β" .. next assume "∃β ∈ T →⇩_{E}S. ?INV β" then obtain β where "α ∈ S → T" "β ∈ T → S" "⋀x. x ∈ S ⟹ β (α x) = x" "⋀y. y ∈ T ⟹ α (β y) = y" by (metis PiE_restrict compose_eq graph restrict_PiE restrict_apply) then show "bij_betw α S T" by (rule bij_betwI) qed end (* map *) subsection ‹Equivalence Relations. Factoring a Map Through an Equivalence Relation› text ‹p 11, ll 6--11› locale equivalence = fixes S and E assumes closed [intro, simp]: "E ⊆ S × S" and reflexive [intro, simp]: "a ∈ S ⟹ (a, a) ∈ E" and symmetric [sym]: "(a, b) ∈ E ⟹ (b, a) ∈ E" and transitive [trans]: "⟦ (a, b) ∈ E; (b, c) ∈ E ⟧ ⟹ (a, c) ∈ E" begin text ‹p 11, ll 6--11› lemma left_closed [intro]: (* inefficient as a simp rule *) "(a, b) ∈ E ⟹ a ∈ S" using closed by blast text ‹p 11, ll 6--11› lemma right_closed [intro]: (* inefficient as a simp rule *) "(a, b) ∈ E ⟹ b ∈ S" using closed by blast end (* equivalence *) text ‹p 11, ll 16--20› locale partition = fixes S and P assumes subset: "P ⊆ Pow S" and non_vacuous: "{} ∉ P" and complete: "⋃P = S" and disjoint: "⟦ A ∈ P; B ∈ P; A ≠ B ⟧ ⟹ A ∩ B = {}" context equivalence begin text ‹p 11, ll 24--26› definition "Class = (λa ∈ S. {b ∈ S. (b, a) ∈ E})" text ‹p 11, ll 24--26› lemma Class_closed [dest]: "⟦ a ∈ Class b; b ∈ S ⟧ ⟹ a ∈ S" unfolding Class_def by auto text ‹p 11, ll 24--26› lemma Class_closed2 [intro, simp]: "a ∈ S ⟹ Class a ⊆ S" unfolding Class_def by auto text ‹p 11, ll 24--26› lemma Class_undefined [intro, simp]: "a ∉ S ⟹ Class a = undefined" unfolding Class_def by simp text ‹p 11, ll 24--26› lemma ClassI [intro, simp]: "(a, b) ∈ E ⟹ a ∈ Class b" unfolding Class_def by (simp add: left_closed right_closed) text ‹p 11, ll 24--26› lemma Class_revI [intro, simp]: "(a, b) ∈ E ⟹ b ∈ Class a" by (blast intro: symmetric) text ‹p 11, ll 24--26› lemma ClassD [dest]: "⟦ b ∈ Class a; a ∈ S ⟧ ⟹ (b, a) ∈ E" unfolding Class_def by simp text ‹p 11, ll 30--31› theorem Class_self [intro, simp]: "a ∈ S ⟹ a ∈ Class a" unfolding Class_def by simp text ‹p 11, l 31; p 12, l 1› theorem Class_Union [simp]: "(⋃a∈S. Class a) = S" by blast text ‹p 11, ll 2--3› theorem Class_subset: "(a, b) ∈ E ⟹ Class a ⊆ Class b" proof fix a and b and c assume "(a, b) ∈ E" and "c ∈ Class a" then have "(c, a) ∈ E" by auto also note ‹(a, b) ∈ E› finally have "(c, b) ∈ E" by simp then show "c ∈ Class b" by auto qed text ‹p 11, ll 3--4› theorem Class_eq: "(a, b) ∈ E ⟹ Class a = Class b" by (auto intro!: Class_subset intro: symmetric) text ‹p 12, ll 1--5› theorem Class_equivalence: "⟦ a ∈ S; b ∈ S ⟧ ⟹ Class a = Class b ⟷ (a, b) ∈ E" proof fix a and b assume "a ∈ S" "b ∈ S" "Class a = Class b" then have "a ∈ Class a" by auto also note ‹Class a = Class b› finally show "(a, b) ∈ E" by (fast intro: ‹b ∈ S›) qed (rule Class_eq) text ‹p 12, ll 5--7› theorem not_disjoint_implies_equal: assumes not_disjoint: "Class a ∩ Class b ≠ {}" assumes closed: "a ∈ S" "b ∈ S" shows "Class a = Class b" proof - from not_disjoint and closed obtain c where witness: "c ∈ Class a ∩ Class b" by fast with closed have "(a, c) ∈ E" by (blast intro: symmetric) also from witness and closed have "(c, b) ∈ E" by fast finally show ?thesis by (rule Class_eq) qed text ‹p 12, ll 7--8› definition "Partition = Class ` S" text ‹p 12, ll 7--8› lemma Class_in_Partition [intro, simp]: "a ∈ S ⟹ Class a ∈ Partition" unfolding Partition_def by fast text ‹p 12, ll 7--8› theorem partition: "partition S Partition" proof fix A and B assume closed: "A ∈ Partition" "B ∈ Partition" then obtain a and b where eq: "A = Class a" "B = Class b" and ab: "a ∈ S" "b ∈ S" unfolding Partition_def by auto assume distinct: "A ≠ B" then show "A ∩ B = {}" proof (rule contrapos_np) assume not_disjoint: "A ∩ B ≠ {}" then show "A = B" by (simp add: eq) (metis not_disjoint_implies_equal ab) qed qed (auto simp: Partition_def) end (* equivalence *) context partition begin text ‹p 12, ll 9--10› theorem block_exists: "a ∈ S ⟹ ∃A. a ∈ A ∧ A ∈ P" using complete by blast text ‹p 12, ll 9--10› theorem block_unique: "⟦ a ∈ A; A ∈ P; a ∈ B; B ∈ P ⟧ ⟹ A = B" using disjoint by blast text ‹p 12, ll 9--10› lemma block_closed [intro]: (* inefficient as a simp rule *) "⟦ a ∈ A; A ∈ P ⟧ ⟹ a ∈ S" using complete by blast text ‹p 12, ll 9--10› lemma element_exists: "A ∈ P ⟹ ∃a ∈ S. a ∈ A" by (metis non_vacuous block_closed all_not_in_conv) text ‹p 12, ll 9--10› definition "Block = (λa ∈ S. THE A. a ∈ A ∧ A ∈ P)" text ‹p 12, ll 9--10› lemma Block_closed [intro, simp]: assumes [intro]: "a ∈ S" shows "Block a ∈ P" proof - obtain A where "a ∈ A" "A ∈ P" using block_exists by blast then show ?thesis apply (auto simp: Block_def) apply (rule theI2) apply (auto dest: block_unique) done qed text ‹p 12, ll 9--10› lemma Block_undefined [intro, simp]: "a ∉ S ⟹ Block a = undefined" unfolding Block_def by simp text ‹p 12, ll 9--10› lemma Block_self: "⟦ a ∈ A; A ∈ P ⟧ ⟹ Block a = A" apply (simp add: Block_def block_closed) apply (rule the_equality) apply (auto dest: block_unique) done text ‹p 12, ll 10--11› definition "Equivalence = {(a, b) . ∃A ∈ P. a ∈ A ∧ b ∈ A}" text ‹p 12, ll 11--12› theorem equivalence: "equivalence S Equivalence" proof show "Equivalence ⊆ S × S" unfolding Equivalence_def using subset by auto next fix a assume "a ∈ S" then show "(a, a) ∈ Equivalence" unfolding Equivalence_def using complete by auto next fix a and b assume "(a, b) ∈ Equivalence" then show "(b, a) ∈ Equivalence" unfolding Equivalence_def by auto next fix a and b and c assume "(a, b) ∈ Equivalence" "(b, c) ∈ Equivalence" then show "(a, c) ∈ Equivalence" unfolding Equivalence_def using disjoint by auto qed text ‹Temporarily introduce equivalence associated to partition.› text ‹p 12, ll 12--14› interpretation equivalence S Equivalence by (rule equivalence) text ‹p 12, ll 12--14› theorem Class_is_Block: assumes "a ∈ S" shows "Class a = Block a" proof - from ‹a ∈ S› and block_exists obtain A where block: "a ∈ A ∧ A ∈ P" by blast show ?thesis apply (simp add: Block_def Class_def) apply (rule theI2) apply (rule block) apply (metis block block_unique) apply (auto dest: block_unique simp: Equivalence_def) done qed text ‹p 12, l 14› lemma Class_equals_Block: "Class = Block" proof fix x show "Class x = Block x" by (cases "x ∈ S") (auto simp: Class_is_Block) qed text ‹p 12, l 14› theorem partition_of_equivalence: "Partition = P" by (auto simp add: Partition_def Class_equals_Block image_iff) (metis Block_self element_exists) end (* partition *) context equivalence begin text ‹p 12, ll 14--17› interpretation partition S Partition by (rule partition) text ‹p 12, ll 14--17› theorem equivalence_of_partition: "Equivalence = E" unfolding Equivalence_def unfolding Partition_def by auto (metis ClassD Class_closed Class_eq) end (* equivalence *) text ‹p 12, l 14› sublocale partition ⊆ equivalence S Equivalence rewrites "equivalence.Partition S Equivalence = P" and "equivalence.Class S Equivalence = Block" apply (rule equivalence) apply (rule partition_of_equivalence) apply (rule Class_equals_Block) done text ‹p 12, ll 14--17› sublocale equivalence ⊆ partition S Partition rewrites "partition.Equivalence Partition = E" and "partition.Block S Partition = Class" apply (rule partition) apply (rule equivalence_of_partition) apply (metis equivalence_of_partition partition partition.Class_equals_Block) done text ‹Unfortunately only effective on input› text ‹p 12, ll 18--20› notation equivalence.Partition (infixl "'/" 75) context equivalence begin text ‹p 12, ll 18--20› lemma representant_exists [dest]: "A ∈ S / E ⟹ ∃a∈S. a ∈ A ∧ A = Class a" by (metis Block_self element_exists) text ‹p 12, ll 18--20› lemma quotient_ClassE: "A ∈ S / E ⟹ (⋀a. a ∈ S ⟹ P (Class a)) ⟹ P A" using representant_exists by blast end (* equivalence *) text ‹p 12, ll 21--23› sublocale equivalence ⊆ natural: surjective_map Class S "S / E" by unfold_locales force+ text ‹Technical device to achieve Jacobson's syntax; context where @{text α} is not a parameter.› text ‹p 12, ll 25--26› locale fiber_relation_notation = fixes S :: "'a set" begin text ‹p 12, ll 25--26› definition Fiber_Relation ("E'(_')") where "Fiber_Relation α = {(x, y). x ∈ S ∧ y ∈ S ∧ α x = α y}" end (* fiber_relation_notation *) text ‹ Context where classes and the induced map are defined through the fiber relation. This will be the case for monoid homomorphisms but not group homomorphisms. › text ‹Avoids infinite interpretation chain.› text ‹p 12, ll 25--26› locale fiber_relation = map begin text ‹Install syntax› text ‹p 12, ll 25--26› sublocale fiber_relation_notation . text ‹p 12, ll 26--27› sublocale equivalence where E = "E(α)" unfolding Fiber_Relation_def by unfold_locales auto text ‹``define $\bar{\alpha}$ by $\bar{\alpha}(\bar{a}) = \alpha(a)$''› text ‹p 13, ll 8--9› definition "induced = (λA ∈ S / E(α). THE b. ∃a ∈ A. b = α a)" text ‹p 13, l 10› theorem Fiber_equality: "⟦ a ∈ S; b ∈ S ⟧ ⟹ Class a = Class b ⟷ α a = α b" unfolding Class_equivalence unfolding Fiber_Relation_def by simp text ‹p 13, ll 8--9› theorem induced_Fiber_simp [simp]: assumes [intro, simp]: "a ∈ S" shows "induced (Class a) = α a" proof - have "(THE b. ∃a∈Class a. b = α a) = α a" by (rule the_equality) (auto simp: Fiber_equality [symmetric] Block_self block_closed) then show ?thesis unfolding induced_def by simp qed text ‹p 13, ll 10--11› interpretation induced: map induced "S / E(α)" T proof (unfold_locales, rule) fix A assume [intro, simp]: "A ∈ S / E(α)" obtain a where a: "a ∈ S" "a ∈ A" using element_exists by auto have "(THE b. ∃a∈A. b = α a) ∈ T" apply (rule theI2) using a apply (auto simp: Fiber_equality [symmetric] Block_self block_closed) done then show "induced A ∈ T" unfolding induced_def by simp qed (simp add: induced_def) text ‹p 13, ll 12--13› sublocale induced: injective_map induced "S / E(α)" T proof show "inj_on induced Partition" unfolding inj_on_def by (metis Fiber_equality Block_self element_exists induced_Fiber_simp) qed text ‹p 13, ll 16--19› theorem factorization_lemma: "a ∈ S ⟹ compose S induced Class a = α a" by (simp add: compose_eq) text ‹p 13, ll 16--19› theorem factorization [simp]: "compose S induced Class = α" by (rule ext) (simp add: compose_def map_undefined) text ‹p 14, ll 2--4› theorem uniqueness: assumes map: "β ∈ S / E(α) →⇩_{E}T" and factorization: "compose S β Class = α" shows "β = induced" proof fix A show "β A = induced A" proof (cases "A ∈ S / E(α)") case True then obtain a where [simp]: "A = Class a" "a ∈ S" by fast then have "β (Class a) = α a" by (metis compose_eq factorization) also have "… = induced (Class a)" by simp finally show ?thesis by simp qed (simp add: induced_def PiE_arb [OF map]) qed end (* fiber_relation *) end

# Theory Group_Theory

(* Copyright (c) 2014-2019 by Clemens Ballarin This file is licensed under the 3-clause BSD license. *) theory Group_Theory imports Set_Theory begin hide_const monoid hide_const group hide_const inverse no_notation quotient (infixl "'/'/" 90) section ‹Monoids and Groups› subsection ‹Monoids of Transformations and Abstract Monoids› text ‹Def 1.1› text ‹p 28, ll 28--30› locale monoid = fixes M and composition (infixl "⋅" 70) and unit ("𝟭") assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M" and unit_closed [intro, simp]: "𝟭 ∈ M" and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)" and left_unit [intro, simp]: "a ∈ M ⟹ 𝟭 ⋅ a = a" and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ 𝟭 = a" text ‹p 29, ll 27--28› locale submonoid = monoid M "(⋅)" 𝟭 for N and M and composition (infixl "⋅" 70) and unit ("𝟭") + assumes subset: "N ⊆ M" and sub_composition_closed: "⟦ a ∈ N; b ∈ N ⟧ ⟹ a ⋅ b ∈ N" and sub_unit_closed: "𝟭 ∈ N" begin text ‹p 29, ll 27--28› lemma sub [intro, simp]: "a ∈ N ⟹ a ∈ M" using subset by blast text ‹p 29, ll 32--33› sublocale sub: monoid N "(⋅)" 𝟭 by unfold_locales (auto simp: sub_composition_closed sub_unit_closed) end (* submonoid *) text ‹p 29, ll 33--34› theorem submonoid_transitive: assumes "submonoid K N composition unit" and "submonoid N M composition unit" shows "submonoid K M composition unit" proof - interpret K: submonoid K N composition unit by fact interpret M: submonoid N M composition unit by fact show ?thesis by unfold_locales auto qed text ‹p 28, l 23› locale transformations = fixes S :: "'a set" (* assumes non_vacuous: "S ≠ {}" *) (* Jacobson requires this but we don't need it, strange. *) text ‹Monoid of all transformations› text ‹p 28, ll 23--24› sublocale transformations ⊆ monoid "S →⇩_{E}S" "compose S" "identity S" by unfold_locales (auto simp: PiE_def compose_eq compose_assoc Id_compose compose_Id) text ‹@{term N} is a monoid of transformations of the set @{term S}.› text ‹p 29, ll 34--36› locale transformation_monoid = transformations S + submonoid M "S →⇩_{E}S" "compose S" "identity S" for M and S begin text ‹p 29, ll 34--36› lemma transformation_closed [intro, simp]: "⟦ α ∈ M; x ∈ S ⟧ ⟹ α x ∈ S" by (metis PiE_iff sub) text ‹p 29, ll 34--36› lemma transformation_undefined [intro, simp]: "⟦ α ∈ M; x ∉ S ⟧ ⟹ α x = undefined" by (metis PiE_arb sub) end (* transformation_monoid *) subsection ‹Groups of Transformations and Abstract Groups› context monoid begin text ‹Invertible elements› text ‹p 31, ll 3--5› definition invertible where "u ∈ M ⟹ invertible u ⟷ (∃v ∈ M. u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭)" text ‹p 31, ll 3--5› lemma invertibleI [intro]: "⟦ u ⋅ v = 𝟭; v ⋅ u = 𝟭; u ∈ M; v ∈ M ⟧ ⟹ invertible u" unfolding invertible_def by fast text ‹p 31, ll 3--5› lemma invertibleE [elim]: "⟦ invertible u; ⋀v. ⟦ u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭; v ∈ M ⟧ ⟹ P; u ∈ M ⟧ ⟹ P" unfolding invertible_def by fast text ‹p 31, ll 6--7› theorem inverse_unique: "⟦ u ⋅ v' = 𝟭; v ⋅ u = 𝟭; u ∈ M; v ∈ M; v' ∈ M ⟧ ⟹ v = v'" by (metis associative left_unit right_unit) text ‹p 31, l 7› definition inverse where "inverse = (λu ∈ M. THE v. v ∈ M ∧ u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭)" text ‹p 31, l 7› theorem inverse_equality: "⟦ u ⋅ v = 𝟭; v ⋅ u = 𝟭; u ∈ M; v ∈ M ⟧ ⟹ inverse u = v" unfolding inverse_def using inverse_unique by simp blast text ‹p 31, l 7› lemma invertible_inverse_closed [intro, simp]: "⟦ invertible u; u ∈ M ⟧ ⟹ inverse u ∈ M" using inverse_equality by auto text ‹p 31, l 7› lemma inverse_undefined [intro, simp]: "u ∉ M ⟹ inverse u = undefined" by (simp add: inverse_def) text ‹p 31, l 7› lemma invertible_left_inverse [simp]: "⟦ invertible u; u ∈ M ⟧ ⟹ inverse u ⋅ u = 𝟭" using inverse_equality by auto text ‹p 31, l 7› lemma invertible_right_inverse [simp]: "⟦ invertible u; u ∈ M ⟧ ⟹ u ⋅ inverse u = 𝟭" using inverse_equality by auto text ‹p 31, l 7› lemma invertible_left_cancel [simp]: "⟦ invertible x; x ∈ M; y ∈ M; z ∈ M ⟧ ⟹ x ⋅ y = x ⋅ z ⟷ y = z" by (metis associative invertible_def left_unit) text ‹p 31, l 7› lemma invertible_right_cancel [simp]: "⟦ invertible x; x ∈ M; y ∈ M; z ∈ M ⟧ ⟹ y ⋅ x = z ⋅ x ⟷ y = z" by (metis associative invertible_def right_unit) text ‹p 31, l 7› lemma inverse_unit [simp]: "inverse 𝟭 = 𝟭" using inverse_equality by blast text ‹p 31, ll 7--8› theorem invertible_inverse_invertible [intro, simp]: "⟦ invertible u; u ∈ M ⟧ ⟹ invertible (inverse u)" using invertible_left_inverse invertible_right_inverse by blast text ‹p 31, l 8› theorem invertible_inverse_inverse [simp]: "⟦ invertible u; u ∈ M ⟧ ⟹ inverse (inverse u) = u" by (simp add: inverse_equality) end (* monoid *) context submonoid begin text ‹Reasoning about @{term invertible} and @{term inverse} in submonoids.› text ‹p 31, l 7› lemma submonoid_invertible [intro, simp]: "⟦ sub.invertible u; u ∈ N ⟧ ⟹ invertible u" using invertibleI by blast text ‹p 31, l 7› lemma submonoid_inverse_closed [intro, simp]: "⟦ sub.invertible u; u ∈ N ⟧ ⟹ inverse u ∈ N" using inverse_equality by auto end (* submonoid *) text ‹Def 1.2› text ‹p 31, ll 9--10› locale group = monoid G "(⋅)" 𝟭 for G and composition (infixl "⋅" 70) and unit ("𝟭") + assumes invertible [simp, intro]: "u ∈ G ⟹ invertible u" text ‹p 31, ll 11--12› locale subgroup = submonoid G M "(⋅)" 𝟭 + sub: group G "(⋅)" 𝟭 for G and M and composition (infixl "⋅" 70) and unit ("𝟭") begin text ‹Reasoning about @{term invertible} and @{term inverse} in subgroups.› text ‹p 31, ll 11--12› lemma subgroup_inverse_equality [simp]: "u ∈ G ⟹ inverse u = sub.inverse u" by (simp add: inverse_equality) text ‹p 31, ll 11--12› lemma subgroup_inverse_iff [simp]: "⟦ invertible x; x ∈ M ⟧ ⟹ inverse x ∈ G ⟷ x ∈ G" using invertible_inverse_inverse sub.invertible_inverse_closed by fastforce end (* subgroup *) text ‹p 31, ll 11--12› lemma subgroup_transitive [trans]: assumes "subgroup K H composition unit" and "subgroup H G composition unit" shows "subgroup K G composition unit" proof - interpret K: subgroup K H composition unit by fact interpret H: subgroup H G composition unit by fact show ?thesis by unfold_locales auto qed context monoid begin text ‹Jacobson states both directions, but the other one is trivial.› text ‹p 31, ll 12--15› theorem subgroupI: fixes G assumes subset [THEN subsetD, intro]: "G ⊆ M" and [intro]: "𝟭 ∈ G" and [intro]: "⋀g h. ⟦ g ∈ G; h ∈ G ⟧ ⟹ g ⋅ h ∈ G" and [intro]: "⋀g. g ∈ G ⟹ invertible g" and [intro]: "⋀g. g ∈ G ⟹ inverse g ∈ G" shows "subgroup G M (⋅) 𝟭" proof - interpret sub: monoid G "(⋅)" 𝟭 by unfold_locales auto show ?thesis proof unfold_locales fix u assume [intro]: "u ∈ G" show "sub.invertible u" using invertible_left_inverse invertible_right_inverse by blast qed auto qed text ‹p 31, l 16› definition "Units = {u ∈ M. invertible u}" text ‹p 31, l 16› lemma mem_UnitsI: "⟦ invertible u; u ∈ M ⟧ ⟹ u ∈ Units" unfolding Units_def by clarify text ‹p 31, l 16› lemma mem_UnitsD: "⟦ u ∈ Units ⟧ ⟹ invertible u ∧ u ∈ M" unfolding Units_def by clarify text ‹p 31, ll 16--21› interpretation units: subgroup Units M proof (rule subgroupI) fix u1 u2 assume Units [THEN mem_UnitsD, simp]: "u1 ∈ Units" "u2 ∈ Units" have "(u1 ⋅ u2) ⋅ (inverse u2 ⋅ inverse u1) = (u1 ⋅ (u2 ⋅ inverse u2)) ⋅ inverse u1" by (simp add: associative del: invertible_left_inverse invertible_right_inverse) also have "… = 𝟭" by simp finally have inv1: "(u1 ⋅ u2) ⋅ (inverse u2 ⋅ inverse u1) = 𝟭" by simp ― ‹ll 16--18› have "(inverse u2 ⋅ inverse u1) ⋅ (u1 ⋅ u2) = (inverse u2 ⋅ (inverse u1 ⋅ u1)) ⋅ u2" by (simp add: associative del: invertible_left_inverse invertible_right_inverse) also have "… = 𝟭" by simp finally have inv2: "(inverse u2 ⋅ inverse u1) ⋅ (u1 ⋅ u2) = 𝟭" by simp ― ‹l 9, “and similarly”› show "u1 ⋅ u2 ∈ Units" using inv1 inv2 invertibleI mem_UnitsI by auto qed (auto simp: Units_def) text ‹p 31, ll 21--22› theorem group_of_Units [intro, simp]: "group Units (⋅) 𝟭" .. text ‹p 31, l 19› lemma composition_invertible [simp, intro]: "⟦ invertible x; invertible y; x ∈ M; y ∈ M ⟧ ⟹ invertible (x ⋅ y)" using mem_UnitsD mem_UnitsI by blast text ‹p 31, l 20› lemma unit_invertible: "invertible 𝟭" by fast text ‹Useful simplification rules› text ‹p 31, l 22› lemma invertible_right_inverse2: "⟦ invertible u; u ∈ M; v ∈ M ⟧ ⟹ u ⋅ (inverse u ⋅ v) = v" by (simp add: associative [THEN sym]) text ‹p 31, l 22› lemma invertible_left_inverse2: "⟦ invertible u; u ∈ M; v ∈ M ⟧ ⟹ inverse u ⋅ (u ⋅ v) = v" by (simp add: associative [THEN sym]) text ‹p 31, l 22› lemma inverse_composition_commute: assumes [simp]: "invertible x" "invertible y" "x ∈ M" "y ∈ M" shows "inverse (x ⋅ y) = inverse y ⋅ inverse x" proof - have "inverse (x ⋅ y) ⋅ (x ⋅ y) = (inverse y ⋅ inverse x) ⋅ (x ⋅ y)" by (simp add: invertible_left_inverse2 associative) then show ?thesis by (simp del: invertible_left_inverse) qed end (* monoid *) text ‹p 31, l 24› context transformations begin text ‹p 31, ll 25--26› theorem invertible_is_bijective: assumes dom: "α ∈ S →⇩_{E}S" shows "invertible α ⟷ bij_betw α S S" proof - from dom interpret map α S S by unfold_locales show ?thesis by (auto simp add: bij_betw_iff_has_inverse invertible_def) qed text ‹p 31, ll 26--27› theorem Units_bijective: "Units = {α ∈ S →⇩_{E}S. bij_betw α S S}" unfolding Units_def by (auto simp add: invertible_is_bijective) text ‹p 31, ll 26--27› lemma Units_bij_betwI [intro, simp]: "α ∈ Units ⟹ bij_betw α S S" by (simp add: Units_bijective) text ‹p 31, ll 26--27› lemma Units_bij_betwD [dest, simp]: "⟦ α ∈ S →⇩_{E}S; bij_betw α S S ⟧ ⟹ α ∈ Units" unfolding Units_bijective by simp text ‹p 31, ll 28--29› abbreviation "Sym ≡ Units" text ‹p 31, ll 26--28› sublocale symmetric: group "Sym" "compose S" "identity S" by (fact group_of_Units) end (* transformations *) text ‹p 32, ll 18--19› locale transformation_group = transformations S + symmetric: subgroup G Sym "compose S" "identity S" for G and S begin text ‹p 32, ll 18--19› lemma transformation_group_closed [intro, simp]: "⟦ α ∈ G; x ∈ S ⟧ ⟹ α x ∈ S" using bij_betwE by blast text ‹p 32, ll 18--19› lemma transformation_group_undefined [intro, simp]: "⟦ α ∈ G; x ∉ S ⟧ ⟹ α x = undefined" by (metis compose_def symmetric.sub.right_unit restrict_apply) end (* transformation_group *) subsection ‹Isomorphisms. Cayley's Theorem› text ‹Def 1.3› text ‹p 37, ll 7--11› locale monoid_isomorphism = bijective_map η M M' + source: monoid M "(⋅)" 𝟭 + target: monoid M' "(⋅')" "𝟭'" for η and M and composition (infixl "⋅" 70) and unit ("𝟭") and M' and composition' (infixl "⋅''" 70) and unit' ("𝟭''") + assumes commutes_with_composition: "⟦ x ∈ M; y ∈ M ⟧ ⟹ η x ⋅' η y = η (x ⋅ y)" and commutes_with_unit: "η 𝟭 = 𝟭'" text ‹p 37, l 10› definition isomorphic_as_monoids (infixl "≅⇩_{M}" 50) where "ℳ ≅⇩_{M}ℳ' ⟷ (let (M, composition, unit) = ℳ; (M', composition', unit') = ℳ' in (∃η. monoid_isomorphism η M composition unit M' composition' unit'))" text ‹p 37, ll 11--12› locale monoid_isomorphism' = bijective_map η M M' + source: monoid M "(⋅)" 𝟭 + target: monoid M' "(⋅')" "𝟭'" for η and M and composition (infixl "⋅" 70) and unit ("𝟭") and M' and composition' (infixl "⋅''" 70) and unit' ("𝟭''") + assumes commutes_with_composition: "⟦ x ∈ M; y ∈ M ⟧ ⟹ η x ⋅' η y = η (x ⋅ y)" text ‹p 37, ll 11--12› sublocale monoid_isomorphism ⊆ monoid_isomorphism' by unfold_locales (simp add: commutes_with_composition) text ‹Both definitions are equivalent.› text ‹p 37, ll 12--15› sublocale monoid_isomorphism' ⊆ monoid_isomorphism proof unfold_locales { fix y assume "y ∈ M'" then obtain x where "η x = y" "x ∈ M" by (metis image_iff surjective) then have "y ⋅' η 𝟭 = y" using commutes_with_composition by auto } then show "η 𝟭 = 𝟭'" by fastforce qed (simp add: commutes_with_composition) context monoid_isomorphism begin text ‹p 37, ll 30--33› theorem inverse_monoid_isomorphism: "monoid_isomorphism (restrict (inv_into M η) M') M' (⋅') 𝟭' M (⋅) 𝟭" using commutes_with_composition commutes_with_unit surjective by unfold_locales auto end (* monoid_isomorphism *) text ‹We only need that @{term η} is symmetric.› text ‹p 37, ll 28--29› theorem isomorphic_as_monoids_symmetric: "(M, composition, unit) ≅⇩_{M}(M', composition', unit') ⟹ (M', composition', unit') ≅⇩_{M}(M, composition, unit)" by (simp add: isomorphic_as_monoids_def) (meson monoid_isomorphism.inverse_monoid_isomorphism) text ‹p 38, l 4› locale left_translations_of_monoid = monoid begin (* We take the liberty of omitting "left_" from the name of the translation operation. The derived transformation monoid and group won't be qualified with "left" either. This avoids qualifications such as "left.left_...". In contexts where left and right translations are used simultaneously, notably subgroup_of_group, qualifiers are needed. *) text ‹p 38, ll 5--7› definition translation ("'(_')⇩_{L}") where "translation = (λa ∈ M. λx ∈ M. a ⋅ x)" text ‹p 38, ll 5--7› lemma translation_map [intro, simp]: "a ∈ M ⟹ (a)⇩_{L}∈ M →⇩_{E}M" unfolding translation_def by simp text ‹p 38, ll 5--7› lemma Translations_maps [intro, simp]: "translation ` M ⊆ M →⇩_{E}M" by (simp add: image_subsetI) text ‹p 38, ll 5--7› lemma translation_apply: "⟦ a ∈ M; b ∈ M ⟧ ⟹ (a)⇩_{L}b = a ⋅ b" unfolding translation_def by auto text ‹p 38, ll 5--7› lemma translation_exist: "f ∈ translation ` M ⟹ ∃a ∈ M. f = (a)⇩_{L}" by auto text ‹p 38, ll 5--7› lemmas Translations_E [elim] = translation_exist [THEN bexE] text ‹p 38, l 10› theorem translation_unit_eq [simp]: "identity M = (𝟭)⇩_{L}" unfolding translation_def by auto text ‹p 38, ll 10--11› theorem translation_composition_eq [simp]: assumes [simp]: "a ∈ M" "b ∈ M" shows "compose M (a)⇩_{L}(b)⇩_{L}= (a ⋅ b)⇩_{L}" unfolding translation_def by rule (simp add: associative compose_def) (* Activate @{locale monoid} to simplify subsequent proof. *) text ‹p 38, ll 7--9› sublocale transformation: transformations M . text ‹p 38, ll 7--9› theorem Translations_transformation_monoid: "transformation_monoid (translation ` M) M" by unfold_locales auto text ‹p 38, ll 7--9› sublocale transformation: transformation_monoid "translation ` M" M by (fact Translations_transformation_monoid) text ‹p 38, l 12› sublocale map translation M "translation ` M" by unfold_locales (simp add: translation_def) text ‹p 38, ll 12--16› theorem translation_isomorphism [intro]: "monoid_isomorphism translation M (⋅) 𝟭 (translation ` M) (compose M) (identity M)" proof unfold_locales have "inj_on translation M" proof (rule inj_onI) fix a b assume [simp]: "a ∈ M" "b ∈ M" "(a)⇩_{L}= (b)⇩_{L}" have "(a)⇩_{L}𝟭 = (b)⇩_{L}𝟭" by simp then show "a = b" by (simp add: translation_def) qed then show "bij_betw translation M (translation ` M)" by (simp add: inj_on_imp_bij_betw) qed simp_all text ‹p 38, ll 12--16› sublocale monoid_isomorphism translation M "(⋅)" 𝟭 "translation ` M" "compose M" "identity M" .. end (* left_translations_of_monoid *) context monoid begin text ‹p 38, ll 1--2› interpretation left_translations_of_monoid .. text ‹p 38, ll 1--2› theorem cayley_monoid: "∃M' composition' unit'. transformation_monoid M' M ∧ (M, (⋅), 𝟭) ≅⇩_{M}(M', composition', unit')" by (simp add: isomorphic_as_monoids_def) (fast intro: Translations_transformation_monoid) end (* monoid *) text ‹p 38, l 17› locale left_translations_of_group = group begin text ‹p 38, ll 17--18› sublocale left_translations_of_monoid where M = G .. text ‹p 38, ll 17--18› notation translation ("'(_')⇩_{L}") text ‹ The group of left translations is a subgroup of the symmetric group, hence @{term transformation.sub.invertible}. › text ‹p 38, ll 20--22› theorem translation_invertible [intro, simp]: assumes [simp]: "a ∈ G" shows "transformation.sub.invertible (a)⇩_{L}" proof show "compose G (a)⇩_{L}(inverse a)⇩_{L}= identity G" by simp next show "compose G (inverse a)⇩_{L}(a)⇩_{L}= identity G" by simp qed auto text ‹p 38, ll 19--20› theorem translation_bijective [intro, simp]: "a ∈ G ⟹ bij_betw (a)⇩_{L}G G" by (blast intro: transformation.invertible_is_bijective [THEN iffD1]) text ‹p 38, ll 18--20› theorem Translations_transformation_group: "transformation_group (translation ` G) G" proof unfold_locales show "(translation ` G) ⊆ transformation.Sym" unfolding transformation.Units_bijective by auto next fix α assume α: "α ∈ translation ` G" then obtain a where a: "a ∈ G" and eq: "α = (a)⇩_{L}" .. with translation_invertible show "transformation.sub.invertible α" by simp qed auto text ‹p 38, ll 18--20› sublocale transformation: transformation_group "translation ` G" G by (fact Translations_transformation_group) end (* left_translations_of_group *) context group begin text ‹p 38, ll 2--3› interpretation left_translations_of_group .. text ‹p 38, ll 2--3› theorem cayley_group: "∃G' composition' unit'. transformation_group G' G ∧ (G, (⋅), 𝟭) ≅⇩_{M}(G', composition', unit')" by (simp add: isomorphic_as_monoids_def) (fast intro: Translations_transformation_group) end (* group *) text ‹Exercise 3› text ‹p 39, ll 9--10› locale right_translations_of_group = group begin text ‹p 39, ll 9--10› definition translation ("'(_')⇩_{R}") where "translation = (λa ∈ G. λx ∈ G. x ⋅ a)" text ‹p 39, ll 9--10› abbreviation "Translations ≡ translation ` G" text ‹The isomorphism that will be established is a map different from @{term translation}.› text ‹p 39, ll 9--10› interpretation aux: map translation G Translations by unfold_locales (simp add: translation_def) text ‹p 39, ll 9--10› lemma translation_map [intro, simp]: "a ∈ G ⟹ (a)⇩_{R}∈ G →⇩_{E}G" unfolding translation_def by simp text ‹p 39, ll 9--10› lemma Translation_maps [intro, simp]: "Translations ⊆ G →⇩_{E}G" by (simp add: image_subsetI) text ‹p 39, ll 9--10› lemma translation_apply: "⟦ a ∈ G; b ∈ G ⟧ ⟹ (a)⇩_{R}b = b ⋅ a" unfolding translation_def by auto text ‹p 39, ll 9--10› lemma translation_exist: "f ∈ Translations ⟹ ∃a ∈ G. f = (a)⇩_{R}" by auto text ‹p 39, ll 9--10› lemmas Translations_E [elim] = translation_exist [THEN bexE] text ‹p 39, ll 9--10› lemma translation_unit_eq [simp]: "identity G = (𝟭)⇩_{R}" unfolding translation_def by auto text ‹p 39, ll 10--11› lemma translation_composition_eq [simp]: assumes [simp]: "a ∈ G" "b ∈ G" shows "compose G (a)⇩_{R}(b)⇩_{R}= (b ⋅ a)⇩_{R}" unfolding translation_def by rule (simp add: associative compose_def) text ‹p 39, ll 10--11› sublocale transformation: transformations G . text ‹p 39, ll 10--11› lemma Translations_transformation_monoid: "transformation_monoid Translations G" by unfold_locales auto text ‹p 39, ll 10--11› sublocale transformation: transformation_monoid Translations G by (fact Translations_transformation_monoid) text ‹p 39, ll 10--11› lemma translation_invertible [intro, simp]: assumes [simp]: "a ∈ G" shows "transformation.sub.invertible (a)⇩_{R}" proof show "compose G (a)⇩_{R}(inverse a)⇩_{R}= identity G" by simp next show "compose G (inverse a)⇩_{R}(a)⇩_{R}= identity G" by simp qed auto text ‹p 39, ll 10--11› lemma translation_bijective [intro, simp]: "a ∈ G ⟹ bij_betw (a)⇩_{R}G G" by (blast intro: transformation.invertible_is_bijective [THEN iffD1]) text ‹p 39, ll 10--11› theorem Translations_transformation_group: "transformation_group Translations G" proof unfold_locales show "Translations ⊆ transformation.Sym" unfolding transformation.Units_bijective by auto next fix α assume α: "α ∈ Translations" then obtain a where a: "a ∈ G" and eq: "α = (a)⇩_{R}" .. with translation_invertible show "transformation.sub.invertible α" by simp qed auto text ‹p 39, ll 10--11› sublocale transformation: transformation_group Translations G by (rule Translations_transformation_group) text ‹p 39, ll 10--11› lemma translation_inverse_eq [simp]: assumes [simp]: "a ∈ G" shows "transformation.sub.inverse (a)⇩_{R}= (inverse a)⇩_{R}" proof (rule transformation.sub.inverse_equality) show "compose G (a)⇩_{R}(inverse a)⇩_{R}= identity G" by simp next show "compose G (inverse a)⇩_{R}(a)⇩_{R}= identity G" by simp qed auto text ‹p 39, ll 10--11› theorem translation_inverse_monoid_isomorphism [intro]: "monoid_isomorphism (λa∈G. transformation.symmetric.inverse (a)⇩_{R}) G (⋅) 𝟭 Translations (compose G) (identity G)" (is "monoid_isomorphism ?inv _ _ _ _ _ _") proof unfold_locales show "?inv ∈ G →⇩_{E}Translations" by (simp del: translation_unit_eq) next note bij_betw_compose [trans] have "bij_betw inverse G G" by (rule bij_betwI [where g = inverse]) auto also have "bij_betw translation G Translations" by (rule bij_betwI [where g = "λα∈Translations. α 𝟭"]) (auto simp: translation_apply) finally show "bij_betw ?inv G Translations" by (simp cong: bij_betw_cong add: compose_eq del: translation_unit_eq) next fix x and y assume [simp]: "x ∈ G" "y ∈ G" show "compose G (?inv x) (?inv y) = (?inv (x ⋅ y))" by (simp add: inverse_composition_commute del: translation_unit_eq) next show "?inv 𝟭 = identity G" by (simp del: translation_unit_eq) simp qed text ‹p 39, ll 10--11› sublocale monoid_isomorphism "λa∈G. transformation.symmetric.inverse (a)⇩_{R}" G "(⋅)" 𝟭 Translations "compose G" "identity G" .. end (* right_translations_of_group *) subsection ‹Generalized Associativity. Commutativity› text ‹p 40, l 27; p 41, ll 1--2› locale commutative_monoid = monoid + assumes commutative: "⟦ x ∈ M; y ∈ M ⟧ ⟹ x ⋅ y = y ⋅ x" text ‹p 41, l 2› locale abelian_group = group + commutative_monoid G "(⋅)" 𝟭 subsection ‹Orbits. Cosets of a Subgroup› context transformation_group begin text ‹p 51, ll 18--20› definition Orbit_Relation where "Orbit_Relation = {(x, y). x ∈ S ∧ y ∈ S ∧ (∃α ∈ G. y = α x)}" text ‹p 51, ll 18--20› lemma Orbit_Relation_memI [intro]: "⟦ ∃α ∈ G. y = α x; x ∈ S ⟧ ⟹ (x, y) ∈ Orbit_Relation" unfolding Orbit_Relation_def by auto text ‹p 51, ll 18--20› lemma Orbit_Relation_memE [elim]: "⟦ (x, y) ∈ Orbit_Relation; ⋀α. ⟦ α ∈ G; x ∈ S; y = α x ⟧ ⟹ Q ⟧ ⟹ Q" unfolding Orbit_Relation_def by auto text ‹p 51, ll 20--23, 26--27› sublocale orbit: equivalence S Orbit_Relation proof (unfold_locales, auto simp: Orbit_Relation_def) fix x assume x: "x ∈ S" then have id: "x = identity S x" by simp with x show "∃α ∈ G. x = α x" by fast fix α assume α: "α ∈ G" with x id have y: "x = compose S (symmetric.inverse α) α x" by auto with x α show "∃α' ∈ G. x = α' (α x)" by (metis compose_eq symmetric.sub.invertible symmetric.submonoid_inverse_closed) fix β assume β: "β ∈ G" with x have "β (α x) = compose S β α x" by (simp add: compose_eq) with α β show "∃γ ∈ G. β (α x) = γ x" by fast qed text ‹p 51, ll 23--24› theorem orbit_equality: "x ∈ S ⟹ orbit.Class x = {α x | α. α ∈ G}" by (simp add: orbit.Class_def) (blast intro: orbit.symmetric dest: orbit.symmetric) end (* transformation_group *) context monoid_isomorphism begin text ‹p 52, ll 16--17› theorem image_subgroup: assumes "subgroup G M (⋅) 𝟭" shows "subgroup (η ` G) M' (⋅') 𝟭'" proof - interpret subgroup G M "(⋅)" 𝟭 by fact interpret image: monoid "η ` G" "(⋅')" "𝟭'" by unfold_locales (auto simp add: commutes_with_composition commutes_with_unit [symmetric]) show ?thesis proof (unfold_locales, auto) fix x assume x: "x ∈ G" show "image.invertible (η x)" proof show "η (sub.inverse x) ∈ η ` G" using x by simp qed (auto simp: x commutes_with_composition commutes_with_unit) qed qed end (* monoid_isomorphism *) text ‹ Technical device to achieve Jacobson's notation for @{text Right_Coset} and @{text Left_Coset}. The definitions are pulled out of @{text subgroup_of_group} to a context where @{text H} is not a parameter. › text ‹p 52, l 20› locale coset_notation = fixes composition (infixl "⋅" 70) begin text ‹Equation 23› text ‹p 52, l 20› definition Right_Coset (infixl "|⋅" 70) where "H |⋅ x = {h ⋅ x | h. h ∈ H}" text ‹p 53, ll 8--9› definition Left_Coset (infixl "⋅|" 70) where "x ⋅| H = {x ⋅ h | h. h ∈ H}" text ‹p 52, l 20› lemma Right_Coset_memI [intro]: "h ∈ H ⟹ h ⋅ x ∈ H |⋅ x" unfolding Right_Coset_def by blast text ‹p 52, l 20› lemma Right_Coset_memE [elim]: "⟦ a ∈ H |⋅ x; ⋀h. ⟦ h ∈ H; a = h ⋅ x ⟧ ⟹ P ⟧ ⟹ P" unfolding Right_Coset_def by blast text ‹p 53, ll 8--9› lemma Left_Coset_memI [intro]: "h ∈ H ⟹ x ⋅ h ∈ x ⋅| H" unfolding Left_Coset_def by blast text ‹p 53, ll 8--9› lemma Left_Coset_memE [elim]: "⟦ a ∈ x ⋅| H; ⋀h. ⟦ h ∈ H; a = x ⋅ h ⟧ ⟹ P ⟧ ⟹ P" unfolding Left_Coset_def by blast end (* coset_notation *) text ‹p 52, l 12› locale subgroup_of_group = subgroup H G "(⋅)" 𝟭 + coset_notation "(⋅)" + group G "(⋅)" 𝟭 for H and G and composition (infixl "⋅" 70) and unit ("𝟭") begin text ‹p 52, ll 12--14› interpretation left: left_translations_of_group .. interpretation right: right_translations_of_group .. text ‹ @{term "left.translation ` H"} denotes Jacobson's @{text "H⇩_{L}(G)"} and @{term "left.translation ` G"} denotes Jacobson's @{text "G⇩_{L}"}. › text ‹p 52, ll 16--18› theorem left_translations_of_subgroup_are_transformation_group [intro]: "transformation_group (left.translation ` H) G" proof - have "subgroup (left.translation ` H) (left.translation ` G) (compose G) (identity G)" by (rule left.image_subgroup) unfold_locales also have "subgroup (left.translation ` G) left.transformation.Sym (compose G) (identity G)" .. finally interpret right_coset: subgroup "left.translation ` H" left.transformation.Sym "compose G" "identity G" . show ?thesis .. qed text ‹p 52, l 18› interpretation transformation_group "left.translation ` H" G .. text ‹p 52, ll 19--20› theorem Right_Coset_is_orbit: "x ∈ G ⟹ H |⋅ x = orbit.Class x" using left.translation_apply by (auto simp: orbit_equality Right_Coset_def) (metis imageI sub) text ‹p 52, ll 24--25› theorem Right_Coset_Union: "(⋃x∈G. H |⋅ x) = G" by (simp add: Right_Coset_is_orbit) text ‹p 52, l 26› theorem Right_Coset_bij: assumes G [simp]: "x ∈ G" "y ∈ G" shows "bij_betw (inverse x ⋅ y)⇩_{R}(H |⋅ x) (H |⋅ y)" proof (rule bij_betw_imageI) show "inj_on (inverse x ⋅ y)⇩_{R}(H |⋅ x)" by (fastforce intro: inj_onI simp add: Right_Coset_is_orbit right.translation_apply orbit.block_closed) next show "(inverse x ⋅ y)⇩_{R}` (H |⋅ x) = H |⋅ y" by (force simp add: right.translation_apply associative invertible_right_inverse2) qed text ‹p 52, ll 25--26› theorem Right_Cosets_cardinality: "⟦ x ∈ G; y ∈ G ⟧ ⟹ card (H |⋅ x) = card (H |⋅ y)" by (fast intro: bij_betw_same_card Right_Coset_bij) text ‹p 52, l 27› theorem Right_Coset_unit: "H |⋅ 𝟭 = H" by (force simp add: Right_Coset_def) text ‹p 52, l 27› theorem Right_Coset_cardinality: "x ∈ G ⟹ card (H |⋅ x) = card H" using Right_Coset_unit Right_Cosets_cardinality unit_closed by presburger text ‹p 52, ll 31--32› definition "index = card orbit.Partition" text ‹Theorem 1.5› text ‹p 52, ll 33--35; p 53, ll 1--2› theorem lagrange: "finite G ⟹ card G = card H * index" unfolding index_def apply (subst card_partition) apply (auto simp: finite_UnionD orbit.complete orbit.disjoint) apply (metis Right_Coset_cardinality Right_Coset_is_orbit orbit.Block_self orbit.element_exists) done end (* subgroup_of_group *) text ‹Left cosets› context subgroup begin text ‹p 31, ll 11--12› lemma image_of_inverse [intro, simp]: "x ∈ G ⟹ x ∈ inverse ` G" by (metis image_eqI sub.invertible sub.invertible_inverse_closed sub.invertible_inverse_inverse subgroup_inverse_equality) end (* subgroup *) context group begin (* Does Jacobson show this somewhere? *) text ‹p 53, ll 6--7› lemma inverse_subgroupI: assumes sub: "subgroup H G (⋅) 𝟭" shows "subgroup (inverse ` H) G (⋅) 𝟭" proof - from sub interpret subgroup H G "(⋅)" 𝟭 . interpret inv: monoid "inverse ` H" "(⋅)" 𝟭 by unfold_locales (auto simp del: subgroup_inverse_equality) interpret inv: group "inverse ` H" "(⋅)" 𝟭 by unfold_locales (force simp del: subgroup_inverse_equality) show ?thesis by unfold_locales (auto simp del: subgroup_inverse_equality) qed text ‹p 53, ll 6--7› lemma inverse_subgroupD: assumes sub: "subgroup (inverse ` H) G (⋅) 𝟭" and inv: "H ⊆ Units" shows "subgroup H G (⋅) 𝟭" proof - from sub have "subgroup (inverse ` inverse ` H) G (⋅) 𝟭" by (rule inverse_subgroupI) moreover from inv [THEN subsetD, simplified Units_def] have "inverse ` inverse ` H = H" by (simp cong: image_cong add: image_comp) ultimately show ?thesis by simp qed end (* group *) context subgroup_of_group begin text ‹p 53, l 6› interpretation right_translations_of_group .. text ‹ @{term "translation ` H"} denotes Jacobson's @{text "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" by (erule quotient_ClassE)+ (simp add: Class_commutes_with_composition) text ‹p 54, l 32; p 55, ll 1--3› sublocale quotient: monoid "M / E" "([⋅])" "Class 𝟭" by unfold_locales (auto simp: Class_commutes_with_composition associative elim!: quotient_ClassE) end (* monoid_congruence *) text ‹p 55, ll 16--17› locale group_congruence = group + monoid_congruence where M = G begin text ‹p 55, ll 16--17› notation quotient_composition (infixl "[⋅]" 70) text ‹p 55, l 18› theorem Class_right_inverse: "a ∈ G ⟹ Class a [⋅] Class (inverse a) = Class 𝟭" by (simp add: Class_commutes_with_composition) text ‹p 55, l 18› theorem Class_left_inverse: "a ∈ G ⟹ Class (inverse a) [⋅] Class a = Class 𝟭" by (simp add: Class_commutes_with_composition) text ‹p 55, l 18› theorem Class_invertible: "a ∈ G ⟹ quotient.invertible (Class a)" by (blast intro!: Class_right_inverse Class_left_inverse)+ text ‹p 55, l 18› theorem Class_commutes_with_inverse: "a ∈ G ⟹ quotient.inverse (Class a) = Class (inverse a)" by (rule quotient.inverse_equality) (auto simp: Class_right_inverse Class_left_inverse) text ‹p 55, l 17› sublocale quotient: group "G / E" "([⋅])" "Class 𝟭" by unfold_locales (metis Block_self Class_invertible element_exists) end (* group_congruence *) text ‹Def 1.5› text ‹p 55, ll 22--25› locale normal_subgroup = subgroup_of_group K G "(⋅)" 𝟭 for K and G and composition (infixl "⋅" 70) and unit ("𝟭") + assumes normal: "⟦ g ∈ G; k ∈ K ⟧ ⟹ inverse g ⋅ k ⋅ g ∈ K" text ‹Lemmas from the proof of Thm 1.6› context subgroup_of_group begin text ‹We use @{term H} for @{term K}.› text ‹p 56, ll 14--16› theorem Left_equals_Right_coset_implies_normality: assumes [simp]: "⋀g. g ∈ G ⟹ g ⋅| H = H |⋅ g" shows "normal_subgroup H G (⋅) 𝟭" proof fix g k assume [simp]: "g ∈ G" "k ∈ H" have "k ⋅ g ∈ g ⋅| H" by auto then obtain k' where "k ⋅ g = g ⋅ k'" and "k' ∈ H" by blast then show "inverse g ⋅ k ⋅ g ∈ H" by (simp add: associative invertible_left_inverse2) qed end (* subgroup_of_group *) text ‹Thm 1.6, first part› context group_congruence begin text ‹Jacobson's $K$› text ‹p 56, l 29› definition "Normal = Class 𝟭" text ‹p 56, ll 3--6› interpretation subgroup "Normal" G "(⋅)" 𝟭 unfolding Normal_def proof (rule subgroupI) fix k1 and k2 assume K: "k1 ∈ Class 𝟭" "k2 ∈ Class 𝟭" then have "k1 ⋅ k2 ∈ Class (k1 ⋅ k2)" by blast also have "… = Class k1 [⋅] Class k2" using K by (auto simp add: Class_commutes_with_composition Class_closed) also have "… = Class 𝟭 [⋅] Class 𝟭" using K by (metis ClassD Class_eq unit_closed) also have "… = Class 𝟭" by simp finally show "k1 ⋅ k2 ∈ Class 𝟭" . next fix k assume K: "k ∈ Class 𝟭" then have "inverse k ∈ Class (inverse k)" by blast also have "… = quotient.inverse (Class k)" using Class_commutes_with_inverse K by blast also have "… = quotient.inverse (Class 𝟭)" using Block_self K by auto also have "… = Class 𝟭" using quotient.inverse_unit by blast finally show "inverse k ∈ Class 𝟭" . qed auto text ‹Coset notation› text ‹p 56, ll 5--6› interpretation subgroup_of_group "Normal" G "(⋅)" 𝟭 .. text ‹Equation 25 for right cosets› text ‹p 55, ll 29--30; p 56, ll 6--11› theorem Right_Coset_Class_unit: assumes g: "g ∈ G" shows "Normal |⋅ g = Class g" unfolding Normal_def proof auto fix a ― ‹ll 6--8› assume a: "a ∈ Class g" from a g have "a ⋅ inverse g ∈ Class (a ⋅ inverse g)" by blast also from a g have "… = Class a [⋅] Class (inverse g)" by (simp add: Class_commutes_with_composition block_closed) also from a g have "… = Class g [⋅] quotient.inverse (Class g)" using Block_self Class_commutes_with_inverse by auto also from g have "… = Class 𝟭" by simp finally show "a ∈ Class 𝟭 |⋅ g" unfolding Right_Coset_def by simp (metis Class_closed a associative g inverse_equality invertible invertible_def right_unit) next fix a ― ‹ll 8--9› assume a: "a ∈ Class 𝟭 |⋅ g" then obtain k where eq: "a = k ⋅ g" and k: "k ∈ Class 𝟭" by blast with g have "Class a = Class k [⋅] Class g" using Class_commutes_with_composition by auto also from k have "… = Class 𝟭 [⋅] Class g" using Block_self by auto also from g have "… = Class g" by simp finally show "a ∈ Class g" using g eq k composition_closed quotient.unit_closed by blast qed text ‹Equation 25 for left cosets› text ‹p 55, ll 29--30; p 56, ll 6--11› theorem Left_Coset_Class_unit: assumes g: "g ∈ G" shows "g ⋅| Normal = Class g" unfolding Normal_def proof auto fix a ― ‹ll 6--8› assume a: "a ∈ Class g" from a g have "inverse g ⋅ a ∈ Class (inverse g ⋅ a)" by blast also from a g have "… = Class (inverse g) [⋅] Class a" by (simp add: Class_commutes_with_composition block_closed) also from a g have "… = quotient.inverse (Class g) [⋅] Class g" using Block_self Class_commutes_with_inverse by auto also from g have "… = Class 𝟭" by simp finally show "a ∈ g ⋅| Class 𝟭" unfolding Left_Coset_def by simp (metis Class_closed a associative g inverse_equality invertible invertible_def right_unit) next fix a ― ‹ll 8--9, ``the same thing holds''› assume a: "a ∈ g ⋅| Class 𝟭" then obtain k where eq: "a = g ⋅ k" and k: "k ∈ Class 𝟭" by blast with g have "Class a = Class g [⋅] Class k" using Class_commutes_with_composition by auto also from k have "… = Class g [⋅] Class 𝟭" using Block_self by auto also from g have "… = Class g" by simp finally show "a ∈ Class g" using g eq k composition_closed quotient.unit_closed by blast qed text ‹Thm 1.6, statement of first part› text ‹p 55, ll 28--29; p 56, ll 12--16› theorem Class_unit_is_normal: "normal_subgroup Normal G (⋅) 𝟭" proof - { fix g assume "g ∈ G" then have "g ⋅| Normal = Normal |⋅ g" by (simp add: Right_Coset_Class_unit Left_Coset_Class_unit) } then show ?thesis by (rule Left_equals_Right_coset_implies_normality) qed sublocale normal: normal_subgroup Normal G "(⋅)" 𝟭 by (fact Class_unit_is_normal) end (* group_congruence *) context normal_subgroup begin text ‹p 56, ll 16--19› theorem Left_equals_Right_coset: "g ∈ G ⟹ g ⋅| K = K |⋅ g" proof assume [simp]: "g ∈ G" show "K |⋅ g ⊆ g ⋅| K" proof fix x assume x: "x ∈ K |⋅ g" then obtain k where "x = k ⋅ g" and [simp]: "k ∈ K" by (auto simp add: Right_Coset_def) then have "x = g ⋅ (inverse g ⋅ k ⋅ g)" by (simp add: associative invertible_right_inverse2) also from normal have "… ∈ g ⋅| K" by (auto simp add: Left_Coset_def) finally show "x ∈ g ⋅| K" . qed next assume [simp]: "g ∈ G" show "g ⋅| K ⊆ K |⋅ g" proof fix x assume x: "x ∈ g ⋅| K" then obtain k where "x = g ⋅ k" and [simp]: "k ∈ K" by (auto simp add: Left_Coset_def) then have "x = (inverse (inverse g) ⋅ k ⋅ inverse g) ⋅ g" by (simp add: associative del: invertible_right_inverse) also from normal [where g = "inverse g"] have "… ∈ K |⋅ g" by (auto simp add: Right_Coset_def) finally show "x ∈ K |⋅ g" . qed qed text ‹Thm 1.6, second part› text ‹p 55, ll 31--32; p 56, ll 20--21› definition "Congruence = {(a, b). a ∈ G ∧ b ∈ G ∧ inverse a ⋅ b ∈ K}" text ‹p 56, ll 21--22› interpretation right_translations_of_group .. text ‹p 56, ll 21--22› interpretation transformation_group "translation ` K" G rewrites "Orbit_Relation = Congruence" proof - interpret transformation_group "translation ` K" G .. show "Orbit_Relation = Congruence" unfolding Orbit_Relation_def Congruence_def by (force simp: invertible_left_inverse2 invertible_right_inverse2 translation_apply simp del: restrict_apply) qed rule text ‹p 56, ll 20--21› lemma CongruenceI: "⟦ a = b ⋅ k; a ∈ G; b ∈ G; k ∈ K ⟧ ⟹ (a, b) ∈ Congruence" by (clarsimp simp: Congruence_def associative inverse_composition_commute) text ‹p 56, ll 20--21› lemma CongruenceD: "(a, b) ∈ Congruence ⟹ ∃k∈K. a = b ⋅ k" by (drule orbit.symmetric) (force simp: Congruence_def invertible_right_inverse2) text ‹ ``We showed in the last section that the relation we are considering is an equivalence relation in @{term G} for any subgroup @{term K} of @{term G}. We now proceed to show that normality of @{term K} ensures that [...] $a \equiv b \pmod{K}$ is a congruence.'' › text ‹p 55, ll 30--32; p 56, ll 1, 22--28› sublocale group_congruence where E = Congruence rewrites "Normal = K" proof - show "group_congruence G (⋅) 𝟭 Congruence" proof unfold_locales note CongruenceI [intro] CongruenceD [dest] fix a g b h assume 1: "(a, g) ∈ Congruence" and 2: "(b, h) ∈ Congruence" then have G: "a ∈ G" "g ∈ G" "b ∈ G" "h ∈ G" unfolding Congruence_def by clarify+ from 1 obtain k1 where a: "a = g ⋅ k1" and k1: "k1 ∈ K" by blast from 2 obtain k2 where b: "b = h ⋅ k2" and k2: "k2 ∈ K" by blast from G Left_equals_Right_coset have "K |⋅ h = h ⋅| K" by blast with k1 obtain k3 where c: "k1 ⋅ h = h ⋅ k3" and k3: "k3 ∈ K" unfolding Left_Coset_def Right_Coset_def by blast from G k1 k2 a b have "a ⋅ b = g ⋅ k1 ⋅ h ⋅ k2" by (simp add: associative) also from G k1 k3 c have "… = g ⋅ h ⋅ k3 ⋅ k2" by (simp add: associative) also have "… = (g ⋅ h) ⋅ (k3 ⋅ k2)" using G k2 k3 by (simp add: associative) finally show "(a ⋅ b, g ⋅ h) ∈ Congruence" using G k2 k3 by blast qed then interpret group_congruence where E = Congruence . show "Normal = K" unfolding Normal_def orbit.Class_def unfolding Congruence_def using invertible_inverse_inverse submonoid_inverse_closed by fastforce qed end (* normal_subgroup *) (* deletes translations and orbits, recovers Class for congruence class *) context group begin text ‹Pulled out of @{locale normal_subgroup} to achieve standard notation.› text ‹p 56, ll 31--32› abbreviation Factor_Group (infixl "'/'/" 75) where "S // K ≡ S / (normal_subgroup.Congruence K G (⋅) 𝟭)" end (* group *) context normal_subgroup begin text ‹p 56, ll 28--29› theorem Class_unit_normal_subgroup: "Class 𝟭 = K" unfolding Class_def unfolding Congruence_def using invertible_inverse_inverse submonoid_inverse_closed by fastforce text ‹p 56, ll 1--2; p 56, l 29› theorem Class_is_Left_Coset: "g ∈ G ⟹ Class g = g ⋅| K" using Left_Coset_Class_unit Class_unit_normal_subgroup by simp text ‹p 56, l 29› lemma Left_CosetE: "⟦ A ∈ G // K; ⋀a. a ∈ G ⟹ P (a ⋅| K) ⟧ ⟹ P A" by (metis Class_is_Left_Coset quotient_ClassE) text ‹Equation 26› text ‹p 56, ll 32--34› theorem factor_composition [simp]: "⟦ g ∈ G; h ∈ G ⟧ ⟹ (g ⋅| K) [⋅] (h ⋅| K) = g ⋅ h ⋅| K" using Class_commutes_with_composition Class_is_Left_Coset by auto text ‹p 56, l 35› theorem factor_unit: "K = 𝟭 ⋅| K" using Class_is_Left_Coset Class_unit_normal_subgroup by blast text ‹p 56, l 35› theorem factor_inverse [simp]: "g ∈ G ⟹ quotient.inverse (g ⋅| K) = (inverse g ⋅| K)" using Class_commutes_with_inverse Class_is_Left_Coset by auto end (* normal_subgroup *) text ‹p 57, ll 4--5› locale subgroup_of_abelian_group = subgroup_of_group H G "(⋅)" 𝟭 + abelian_group G "(⋅)" 𝟭 for H and G and composition (infixl "⋅" 70) and unit ("𝟭") text ‹p 57, ll 4--5› sublocale subgroup_of_abelian_group ⊆ normal_subgroup H G "(⋅)" 𝟭 using commutative invertible_right_inverse2 by unfold_locales auto subsection ‹Homomorphims› text ‹Def 1.6› text ‹p 58, l 33; p 59, ll 1--2› locale monoid_homomorphism = map η M M'+ source: monoid M "(⋅)" 𝟭 + target: monoid M' "(⋅')" "𝟭'" for η and M and composition (infixl "⋅" 70) and unit ("𝟭") and M' and composition' (infixl "⋅''" 70) and unit' ("𝟭''") + assumes commutes_with_composition: "⟦ x ∈ M; y ∈ M ⟧ ⟹ η (x ⋅ y) = η x ⋅' η y" and commutes_with_unit: "η 𝟭 = 𝟭'" begin text ‹Jacobson notes that @{thm [source] commutes_with_unit} is not necessary for groups, but doesn't make use of that later.› text ‹p 58, l 33; p 59, ll 1--2› notation source.invertible ("invertible _" [100] 100) notation source.inverse ("inverse _" [100] 100) notation target.invertible ("invertible'' _" [100] 100) notation target.inverse ("inverse'' _" [100] 100) end (* monoid_homomorphism *) text ‹p 59, ll 29--30› locale monoid_epimorphism = monoid_homomorphism + surjective_map η M M' text ‹p 59, l 30› locale monoid_monomorphism = monoid_homomorphism + injective_map η M M' text ‹p 59, ll 30--31› sublocale monoid_isomorphism ⊆ monoid_epimorphism by unfold_locales (auto simp: commutes_with_composition commutes_with_unit) text ‹p 59, ll 30--31› sublocale monoid_isomorphism ⊆ monoid_monomorphism by unfold_locales (auto simp: commutes_with_composition commutes_with_unit) context monoid_homomorphism begin text ‹p 59, ll 33--34› theorem invertible_image_lemma: assumes "invertible a" "a ∈ M" shows "η a ⋅' η (inverse a) = 𝟭'" and "η (inverse a) ⋅' η a = 𝟭'" using assms commutes_with_composition commutes_with_unit source.inverse_equality by auto (metis source.invertible_inverse_closed source.invertible_left_inverse) text ‹p 59, l 34; p 60, l 1› theorem invertible_target_invertible [intro, simp]: "⟦ invertible a; a ∈ M ⟧ ⟹ invertible' (η a)" using invertible_image_lemma by blast text ‹p 60, l 1› theorem invertible_commutes_with_inverse: "⟦ invertible a; a ∈ M ⟧ ⟹ η (inverse a) = inverse' (η a)" using invertible_image_lemma target.inverse_equality by fastforce end (* monoid_homomorphism *) text ‹p 60, ll 32--34; p 61, l 1› sublocale monoid_congruence ⊆ natural: monoid_homomorphism Class M "(⋅)" 𝟭 "M / E" "([⋅])" "Class 𝟭" by unfold_locales (auto simp: PiE_I Class_commutes_with_composition) text ‹Fundamental Theorem of Homomorphisms of Monoids› text ‹p 61, ll 5, 14--16› sublocale monoid_homomorphism ⊆ image: submonoid "η ` M" M' "(⋅')" "𝟭'" by unfold_locales (auto simp: commutes_with_composition [symmetric] commutes_with_unit [symmetric]) text ‹p 61, l 4› locale monoid_homomorphism_fundamental = monoid_homomorphism begin text ‹p 61, ll 17--18› sublocale fiber_relation η M M' .. notation Fiber_Relation ("E'(_')") text ‹p 61, ll 6--7, 18--20› sublocale monoid_congruence where E = "E(η)" using Class_eq by unfold_locales (rule Class_equivalence [THEN iffD1], auto simp: left_closed right_closed commutes_with_composition Fiber_equality) text ‹p 61, ll 7--9› text ‹ @{term induced} denotes Jacobson's $\bar{\eta}$. We have the commutativity of the diagram, where @{term induced} is unique: @{thm [display] factorization} @{thm [display] uniqueness}. › text ‹p 61, l 20› notation quotient_composition (infixl "[⋅]" 70) text ‹p 61, ll 7--8, 22--25› sublocale induced: monoid_homomorphism induced "M / E(η)" "([⋅])" "Class 𝟭" "M'" "(⋅')" "𝟭'" apply unfold_locales apply (auto simp: commutes_with_unit) apply (fastforce simp: commutes_with_composition commutes_with_unit Class_commutes_with_composition) done text ‹p 61, ll 9, 26› sublocale natural: monoid_epimorphism Class M "(⋅)" 𝟭 "M / E(η)" "([⋅])" "Class 𝟭" .. text ‹p 61, ll 9, 26--27› sublocale induced: monoid_monomorphism induced "M / E(η)" "([⋅])" "Class 𝟭" "M'" "(⋅')" "𝟭'" .. end (* monoid_homomorphism_fundamental *) text ‹p 62, ll 12--13› locale group_homomorphism = monoid_homomorphism η G "(⋅)" 𝟭 G' "(⋅')" "𝟭'" + source: group G "(⋅)" 𝟭 + target: group G' "(⋅')" "𝟭'" for η and G and composition (infixl "⋅" 70) and unit ("𝟭") and G' and composition' (infixl "⋅''" 70) and unit' ("𝟭''") begin text ‹p 62, l 13› sublocale image: subgroup "η ` G" G' "(⋅')" "𝟭'" using invertible_image_lemma by unfold_locales auto text ‹p 62, ll 13--14› definition "Ker = η -` {𝟭'} ∩ G" text ‹p 62, ll 13--14› lemma Ker_equality: "Ker = {a | a. a ∈ G ∧ η a = 𝟭'}" unfolding Ker_def by auto text ‹p 62, ll 13--14› lemma Ker_closed [intro, simp]: "a ∈ Ker ⟹ a ∈ G" unfolding Ker_def by simp text ‹p 62, ll 13--14› lemma Ker_image [intro]: (* loops as a simprule *) "a ∈ Ker ⟹ η a = 𝟭'" unfolding Ker_def by simp text ‹p 62, ll 13--14› lemma Ker_memI [intro]: (* loops as a simprule *) "⟦ η a = 𝟭'; a ∈ G ⟧ ⟹ a ∈ Ker" unfolding Ker_def by simp text ‹p 62, ll 15--16› sublocale kernel: normal_subgroup Ker G proof - interpret kernel: submonoid Ker G unfolding Ker_def by unfold_locales (auto simp: commutes_with_composition commutes_with_unit) interpret kernel: subgroup Ker G by unfold_locales (force intro: source.invertible_right_inverse simp: Ker_image invertible_commutes_with_inverse) show "normal_subgroup Ker G (⋅) 𝟭" apply unfold_locales unfolding Ker_def by (auto simp: commutes_with_composition invertible_image_lemma(2)) qed text ‹p 62, ll 17--20› theorem injective_iff_kernel_unit: "inj_on η G ⟷ Ker = {𝟭}" proof (rule Not_eq_iff [THEN iffD1, OF iffI]) assume "Ker ≠ {𝟭}" then obtain b where b: "b ∈ Ker" "b ≠ 𝟭" by blast then have "η b = η 𝟭" by (simp add: Ker_image) with b show "¬ inj_on η G" by (meson inj_onD kernel.sub source.unit_closed) next assume "¬ inj_on η G" then obtain a b where "a ≠ b" and ab: "a ∈ G" "b ∈ G" "η a = η b" by (meson inj_onI) then have "inverse a ⋅ b ≠ 𝟭" "η (inverse a ⋅ b) = 𝟭'" using ab source.invertible_right_inverse2 by force (metis ab commutes_with_composition invertible_image_lemma(2) source.invertible source.invertible_inverse_closed) then have "inverse a ⋅ b ∈ Ker" using Ker_memI ab by blast then show "Ker ≠ {𝟭}" using ‹inverse a ⋅ b ≠ 𝟭› by blast qed end (* group_homomorphism *) text ‹p 62, l 24› locale group_epimorphism = group_homomorphism + monoid_epimorphism η G "(⋅)" 𝟭 G' "(⋅')" "𝟭'" text ‹p 62, l 21› locale normal_subgroup_in_kernel = group_homomorphism + contained: normal_subgroup L G "(⋅)" 𝟭 for L + assumes subset: "L ⊆ Ker" begin text ‹p 62, l 21› notation contained.quotient_composition (infixl "[⋅]" 70) text ‹"homomorphism onto @{term "G // L"}"› text ‹p 62, ll 23--24› sublocale natural: group_epimorphism contained.Class G "(⋅)" 𝟭 "G // L" "([⋅])" "contained.Class 𝟭" .. text ‹p 62, ll 25--26› theorem left_coset_equality: assumes eq: "a ⋅| L = b ⋅| L" and [simp]: "a ∈ G" and b: "b ∈ G" shows "η a = η b" proof - obtain l where l: "b = a ⋅ l" "l ∈ L" by (metis b contained.Class_is_Left_Coset contained.Class_self eq kernel.Left_Coset_memE) then have "η a = η a ⋅' η l" using Ker_image monoid_homomorphism.commutes_with_composition subset by auto also have "… = η b" by (simp add: commutes_with_composition l) finally show ?thesis . qed text ‹$\bar{\eta}$› text ‹p 62, ll 26--27› definition "induced = (λA ∈ G // L. THE b. ∃a ∈ G. a ⋅| L = A ∧ b = η a)" text ‹p 62, ll 26--27› lemma induced_closed [intro, simp]: assumes [simp]: "A ∈ G // L" shows "induced A ∈ G'" proof - obtain a where a: "a ∈ G" "a ⋅| L = A" using contained.Class_is_Left_Coset contained.Partition_def assms by auto have "(THE b. ∃a ∈ G. a ⋅| L = A ∧ b = η a) ∈ G'" apply (rule theI2) using a by (auto intro: left_coset_equality) then show ?thesis unfolding induced_def by simp qed text ‹p 62, ll 26--27› lemma induced_undefined [intro, simp]: "A ∉ G // L ⟹ induced A = undefined" unfolding induced_def by simp text ‹p 62, ll 26--27› theorem induced_left_coset_closed [intro, simp]: "a ∈ G ⟹ induced (a ⋅| L) ∈ G'" using contained.Class_is_Left_Coset contained.Class_in_Partition by auto text ‹p 62, ll 26--27› theorem induced_left_coset_equality [simp]: assumes [simp]: "a ∈ G" shows "induced (a ⋅| L) = η a" proof - have "(THE b. ∃a' ∈ G. a' ⋅| L = a ⋅| L ∧ b = η a') = η a" by (rule the_equality) (auto intro: left_coset_equality) then show ?thesis unfolding induced_def using contained.Class_is_Left_Coset contained.Class_in_Partition by auto qed text ‹p 62, l 27› theorem induced_Left_Coset_commutes_with_composition [simp]: "⟦ a ∈ G; b ∈ G ⟧ ⟹ induced ((a ⋅| L) [⋅] (b ⋅| L)) = induced (a ⋅| L) ⋅' induced (b ⋅| L)" by (simp add: commutes_with_composition) text ‹p 62, ll 27--28› theorem induced_group_homomorphism: "group_homomorphism induced (G // L) ([⋅]) (contained.Class 𝟭) G' (⋅') 𝟭'" apply unfold_locales apply (auto elim!: contained.Left_CosetE simp: commutes_with_composition commutes_with_unit) using contained.factor_unit induced_left_coset_equality apply (fastforce simp: contained.Class_unit_normal_subgroup) done text ‹p 62, l 28› sublocale induced: group_homomorphism induced "G // L" "([⋅])" "contained.Class 𝟭" G' "(⋅')" "𝟭'" by (fact induced_group_homomorphism) text ‹p 62, ll 28--29› theorem factorization_lemma: "a ∈ G ⟹ compose G induced contained.Class a = η a" unfolding compose_def by (simp add: contained.Class_is_Left_Coset) text ‹p 62, ll 29--30› theorem factorization [simp]: "compose G induced contained.Class = η" by rule (simp add: compose_def contained.Class_is_Left_Coset map_undefined) text ‹ Jacobson does not state the uniqueness of @{term induced} explicitly but he uses it later, for rings, on p 107. › text ‹p 62, l 30› theorem uniqueness: assumes map: "β ∈ G // L →⇩_{E}G'" and factorization: "compose G β contained.Class = η" shows "β = induced" proof fix A show "β A = induced A" proof (cases "A ∈ G // L") case True then obtain a where [simp]: "A = contained.Class a" "a ∈ G" by fast then have "β (contained.Class a) = η a" by (metis compose_eq factorization) also have "… = induced (contained.Class a)" by (simp add: contained.Class_is_Left_Coset) finally show ?thesis by simp qed (simp add: induced_def PiE_arb [OF map]) qed text ‹p 62, l 31› theorem induced_image: "induced ` (G // L) = η ` G" by (metis factorization contained.natural.surjective surj_compose) text ‹p 62, l 33› interpretation L: normal_subgroup L Ker by unfold_locales (auto simp: subset, metis kernel.sub kernel.subgroup_inverse_equality contained.normal) text ‹p 62, ll 31--33› theorem induced_kernel: "induced.Ker = Ker / L.Congruence" (* Ker // L is apparently not the right thing *) proof - have "induced.Ker = { a ⋅| L | a. a ∈ G ∧ a ∈ Ker }" unfolding induced.Ker_equality by simp (metis (hide_lams) contained.Class_is_Left_Coset Ker_image Ker_memI induced_left_coset_equality contained.Class_in_Partition contained.representant_exists) also have "… = Ker / L.Congruence" using L.Class_is_Left_Coset L.Class_in_Partition by auto (metis L.Class_is_Left_Coset L.representant_exists kernel.sub) finally show ?thesis . qed text ‹p 62, ll 34--35› theorem induced_inj_on: "inj_on induced (G // L) ⟷ L = Ker" apply (simp add: induced.injective_iff_kernel_unit induced_kernel contained.Class_unit_normal_subgroup) apply rule using L.block_exists apply auto [1] using L.Block_self L.Class_unit_normal_subgroup L.quotient.unit_closed L.representant_exists apply auto done end (* normal_subgroup_in_kernel *) text ‹Fundamental Theorem of Homomorphisms of Groups› text ‹p 63, l 1› locale group_homomorphism_fundamental = group_homomorphism begin text ‹p 63, l 1› notation kernel.quotient_composition (infixl "[⋅]" 70) text ‹p 63, l 1› sublocale normal_subgroup_in_kernel where L = Ker by unfold_locales rule text ‹p 62, ll 36--37; p 63, l 1› text ‹ @{term induced} denotes Jacobson's $\bar{\eta}$. We have the commutativity of the diagram, where @{term induced} is unique: @{thm [display] factorization} @{thm [display] uniqueness} › end (* group_homomorphism_fundamental *) text ‹p 63, l 5› locale group_isomorphism = group_homomorphism + bijective_map η G G' begin text ‹p 63, l 5› sublocale monoid_isomorphism η G "(⋅)" 𝟭 G' "(⋅')" "𝟭'" by unfold_locales (auto simp: commutes_with_composition) text ‹p 63, l 6› lemma inverse_group_isomorphism: "group_isomorphism (restrict (inv_into G η) G') G' (⋅') 𝟭' G (⋅) 𝟭" using commutes_with_composition commutes_with_unit surjective by unfold_locales auto end (* group_isomorphism *) text ‹p 63, l 6› definition isomorphic_as_groups (infixl "≅⇩_{G}" 50) where "𝒢 ≅⇩_{G}𝒢' ⟷ (let (G, composition, unit) = 𝒢; (G', composition', unit') = 𝒢' in (∃η. group_isomorphism η G composition unit G' composition' unit'))" text ‹p 63, l 6› lemma isomorphic_as_groups_symmetric: "(G, composition, unit) ≅⇩_{G}(G', composition', unit') ⟹ (G', composition', unit') ≅⇩_{G}(G, composition, unit)" by (simp add: isomorphic_as_groups_def) (meson group_isomorphism.inverse_group_isomorphism) text ‹p 63, l 1› sublocale group_isomorphism ⊆ group_epimorphism .. text ‹p 63, l 1› locale group_epimorphism_fundamental = group_homomorphism_fundamental + group_epimorphism begin text ‹p 63, ll 1--2› interpretation image: group_homomorphism induced "G // Ker" "([⋅])" "kernel.Class 𝟭" "(η ` G)" "(⋅')" "𝟭'" by (simp add: surjective group_homomorphism_fundamental.intro induced_group_homomorphism) text ‹p 63, ll 1--2› sublocale image: group_isomorphism induced "G // Ker" "([⋅])" "kernel.Class 𝟭" "(η ` G)" "(⋅')" "𝟭'" using induced_group_homomorphism by unfold_locales (auto simp: bij_betw_def induced_image induced_inj_on induced.commutes_with_composition) end (* group_epimorphism_fundamental *) context group_homomorphism begin text ‹p 63, ll 5--7› theorem image_isomorphic_to_factor_group: "∃K composition unit. normal_subgroup K G (⋅) 𝟭 ∧ (η ` G, (⋅'), 𝟭') ≅⇩_{G}(G // K, composition, unit)" proof - interpret image: group_epimorphism_fundamental where G' = "η ` G" by unfold_locales (auto simp: commutes_with_composition) have "group_isomorphism image.induced (G // Ker) ([⋅]) (kernel.Class 𝟭) (η ` G) (⋅') 𝟭'" .. then have "(η ` G, (⋅'), 𝟭') ≅⇩_{G}(G // Ker, ([⋅]), kernel.Class 𝟭)" by (simp add: isomorphic_as_groups_def) (meson group_isomorphism.inverse_group_isomorphism) moreover have "normal_subgroup Ker G (⋅) 𝟭" .. ultimately show ?thesis by blast qed end (* group_homomorphism *) end

# Theory Ring_Theory

(* Copyright (c) 2015--2019 by Clemens Ballarin This file is licensed under the 3-clause BSD license. *) theory Ring_Theory imports Group_Theory begin no_notation plus (infixl "+" 65) no_notation minus (infixl "-" 65) no_notation uminus ("- _" [81] 80) no_notation quotient (infixl "'/'/" 90) section ‹Rings› subsection ‹Definition and Elementary Properties› text ‹Def 2.1› text ‹p 86, ll 20--28› locale ring = additive: abelian_group R "(+)" 𝟬 + multiplicative: monoid R "(⋅)" 𝟭 for R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭") + assumes distributive: "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ a ⋅ (b + c) = a ⋅ b + a ⋅ c" "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ (b + c) ⋅ a = b ⋅ a + c ⋅ a" begin text ‹p 86, ll 20--28› notation additive.inverse ("- _" [66] 65) abbreviation subtraction (infixl "-" 65) where "a - b ≡ a + (- b)" (* or, alternatively, a definition *) end (* ring *) text ‹p 87, ll 10--12› locale subring = additive: subgroup S R "(+)" 𝟬 + multiplicative: submonoid S R "(⋅)" 𝟭 for S and R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭") context ring begin text ‹p 88, ll 26--28› lemma right_zero [simp]: assumes [simp]: "a ∈ R" shows "a ⋅ 𝟬 = 𝟬" proof - have "a ⋅ 𝟬 = a ⋅ (𝟬 + 𝟬)" by simp also have "… = a ⋅ 𝟬 + a ⋅ 𝟬" by (simp add: distributive del: additive.left_unit additive.right_unit) finally have "a ⋅ 𝟬 - a ⋅ 𝟬 = a ⋅ 𝟬 + a ⋅ 𝟬 - a ⋅ 𝟬" by simp then show ?thesis by (simp add: additive.associative del: additive.invertible_left_cancel) qed text ‹p 88, l 29› lemma left_zero [simp]: assumes [simp]: "a ∈ R" shows "𝟬 ⋅ a = 𝟬" proof - have "𝟬 ⋅ a = (𝟬 + 𝟬) ⋅ a" by simp also have "… = 𝟬 ⋅ a + 𝟬 ⋅ a" by (simp add: distributive del: additive.left_unit additive.right_unit) finally have "𝟬 ⋅ a - 𝟬 ⋅ a = 𝟬 ⋅ a + 𝟬 ⋅ a - 𝟬 ⋅ a" by simp then show ?thesis by (simp add: additive.associative del: additive.invertible_left_cancel) qed text ‹p 88, ll 29--30; p 89, ll 1--2› lemma left_minus: assumes [simp]: "a ∈ R" "b ∈ R" shows "(- a) ⋅ b = - a ⋅ b" proof - have "𝟬 = 𝟬 ⋅ b" by simp also have "… = (a - a) ⋅ b" by simp also have "… = a ⋅ b + (- a) ⋅ b" by (simp add: distributive del: additive.invertible_right_inverse) finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + (- a) ⋅ b" by (simp add: additive.associative del: additive.invertible_left_inverse) then show ?thesis by simp qed text ‹p 89, l 3› lemma right_minus: assumes [simp]: "a ∈ R" "b ∈ R" shows "a ⋅ (- b) = - a ⋅ b" proof - have "𝟬 = a ⋅ 𝟬" by simp also have "… = a ⋅ (b - b)" by simp also have "… = a ⋅ b + a ⋅ (- b)" by (simp add: distributive del: additive.invertible_right_inverse) finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + a ⋅ (- b)" by (simp add: additive.associative del: additive.invertible_left_inverse) then show ?thesis by simp qed end (* ring *) subsection ‹Ideals, Quotient Rings› text ‹p 101, ll 2--5› locale ring_congruence = ring + additive: group_congruence R "(+)" 𝟬 E + multiplicative: monoid_congruence R "(⋅)" 𝟭 E for E begin text ‹p 101, ll 2--5› notation additive.quotient_composition (infixl "[+]" 65) notation additive.quotient.inverse ("[-] _" [66] 65) notation multiplicative.quotient_composition (infixl "[⋅]" 70) text ‹p 101, ll 5--11› sublocale quotient: ring "R / E" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭" by unfold_locales (auto simp: additive.Class_commutes_with_composition additive.associative additive.commutative multiplicative.Class_commutes_with_composition distributive elim!: additive.quotient_ClassE) end (* ring_congruence *) text ‹p 101, ll 12--13› locale subgroup_of_additive_group_of_ring = additive: subgroup I R "(+)" 𝟬 + ring R "(+)" "(⋅)" 𝟬 𝟭 for I and R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭") begin text ‹p 101, ll 13--14› definition "Ring_Congruence = {(a, b). a ∈ R ∧ b ∈ R ∧ a - b ∈ I}" text ‹p 101, ll 13--14› lemma Ring_CongruenceI: "⟦ a - b ∈ I; a ∈ R; b ∈ R ⟧ ⟹ (a, b) ∈ Ring_Congruence" using Ring_Congruence_def by blast text ‹p 101, ll 13--14› lemma Ring_CongruenceD: "(a, b) ∈ Ring_Congruence ⟹ a - b ∈ I" using Ring_Congruence_def by blast text ‹ Jacobson's definition of ring congruence deviates from that of group congruence; this complicates the proof. › text ‹p 101, ll 12--14› sublocale additive: subgroup_of_abelian_group I R "(+)" 𝟬 (* implies normal_subgroup *) rewrites additive_congruence: "additive.Congruence = Ring_Congruence" proof - show "subgroup_of_abelian_group I R (+) 𝟬" using additive.commutative additive.invertible_right_inverse2 by unfold_locales auto then interpret additive: subgroup_of_abelian_group I R "(+)" 𝟬 . { fix a b assume [simp]: "a ∈ R" "b ∈ R" have "a - b ∈ I ⟷ - (a - b) ∈ I" by auto also have "… ⟷ - a + b ∈ I" by (simp add: additive.commutative additive.inverse_composition_commute) finally have "a - b ∈ I ⟷ - a + b ∈ I" . } then show "additive.Congruence = Ring_Congruence" unfolding additive.Congruence_def Ring_Congruence_def by auto qed text ‹p 101, l 14› notation additive.Left_Coset (infixl "+|" 65) end (* subgroup_of_additive_group_of_ring *) text ‹Def 2.2› text ‹p 101, ll 21--22› locale ideal = subgroup_of_additive_group_of_ring + assumes ideal: "⟦ a ∈ R; b ∈ I ⟧ ⟹ a ⋅ b ∈ I" "⟦ a ∈ R; b ∈ I ⟧ ⟹ b ⋅ a ∈ I" context subgroup_of_additive_group_of_ring begin text ‹p 101, ll 14--17› theorem multiplicative_congruence_implies_ideal: assumes "monoid_congruence R (⋅) 𝟭 Ring_Congruence" shows "ideal I R (+) (⋅) 𝟬 𝟭" proof - interpret multiplicative: monoid_congruence R "(⋅)" 𝟭 Ring_Congruence by fact show ?thesis proof fix a b assume [simp]: "a ∈ R" "b ∈ I" have congs: "(a, a) ∈ Ring_Congruence" "(b, 𝟬) ∈ Ring_Congruence" by (auto simp: additive.ClassD additive.Class_unit_normal_subgroup) from congs have "(a ⋅ b, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce then show "a ⋅ b ∈ I" using additive.Class_unit_normal_subgroup by blast from congs have "(b ⋅ a, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce then show "b ⋅ a ∈ I" using additive.Class_unit_normal_subgroup by blast qed qed end (* subgroup_of_additive_group_of_ring *) context ideal begin text ‹p 101, ll 17--20› theorem multiplicative_congruence [intro]: assumes a: "(a, a') ∈ Ring_Congruence" and b: "(b, b') ∈ Ring_Congruence" shows "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence" proof - note Ring_CongruenceI [intro] Ring_CongruenceD [dest] from a b have [simp]: "a ∈ R" "a' ∈ R" "b ∈ R" "b' ∈ R" by auto from a have [simp]: "a - a' ∈ I" .. have "a ⋅ b - a' ⋅ b = (a - a') ⋅ b" by (simp add: distributive left_minus) also have "… ∈ I" by (simp add: ideal) finally have ab: "a ⋅ b - a' ⋅ b ∈ I" . ― ‹ll 18--19› from b have [simp]: "b - b' ∈ I" .. have "a' ⋅ b - a' ⋅ b' = a' ⋅ (b - b')" by (simp add: distributive right_minus) also have "… ∈ I" by (simp add: ideal) finally have a'b': "a' ⋅ b - a' ⋅ b' ∈ I" . ― ‹l 19› have "a ⋅ b - a' ⋅ b' = (a ⋅ b - a' ⋅ b) + (a' ⋅ b - a' ⋅ b')" by (simp add: additive.associative) (simp add: additive.associative [symmetric]) also have "… ∈ I" using ab a'b' by simp finally show "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence" by auto ― ‹ll 19--20› qed text ‹p 101, ll 23--24› sublocale ring_congruence where E = Ring_Congruence by unfold_locales rule end (* ideal *) context ring begin text ‹Pulled out of @{locale ideal} to achieve standard notation.› text ‹p 101, ll 24--26› abbreviation Quotient_Ring (infixl "'/'/" 75) where "S // I ≡ S / (subgroup_of_additive_group_of_ring.Ring_Congruence I R (+) 𝟬)" end (* ring *) text ‹p 101, ll 24--26› locale quotient_ring = ideal begin text ‹p 101, ll 24--26› sublocale quotient: ring "R // I" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭" .. text ‹p 101, l 26› lemmas Left_Coset = additive.Left_CosetE text ‹Equation 17 (1)› text ‹p 101, l 28› lemmas quotient_addition = additive.factor_composition text ‹Equation 17 (2)› text ‹p 101, l 29› theorem quotient_multiplication [simp]: "⟦ a ∈ R; b ∈ R ⟧ ⟹ (a +| I) [⋅] (b +| I) = a ⋅ b +| I" using multiplicative.Class_commutes_with_composition additive.Class_is_Left_Coset by auto text ‹p 101, l 30› lemmas quotient_zero = additive.factor_unit lemmas quotient_negative = additive.factor_inverse end (* quotient_ring *) subsection ‹Homomorphisms of Rings. Basic Theorems› text ‹Def 2.3› text ‹p 106, ll 7--9› locale ring_homomorphism = map η R R' + source: ring R "(+)" "(⋅)" 𝟬 𝟭 + target: ring R' "(+')" "(⋅')" "𝟬'" "𝟭'" + additive: group_homomorphism η R "(+)" 𝟬 R' "(+')" "𝟬'" + multiplicative: monoid_homomorphism η R "(⋅)" 𝟭 R' "(⋅')" "𝟭'" for η and R and addition (infixl "+" 65) and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭") and R' and addition' (infixl "+''" 65) and multiplication' (infixl "⋅''" 70) and zero' ("𝟬''") and unit' ("𝟭''") text ‹p 106, l 17› locale ring_epimorphism = ring_homomorphism + surjective_map η R R' text ‹p 106, ll 14--18› sublocale quotient_ring ⊆ natural: ring_epimorphism where η = additive.Class and R' = "R // I" and addition' = "([+])" and multiplication' = "([⋅])" and zero' = "additive.Class 𝟬" and unit' = "additive.Class 𝟭" .. context ring_homomorphism begin text ‹ Jacobson reasons via @{term "a - b ∈ additive.Ker"} being a congruence; we prefer the direct proof, since it is very simple. › text ‹p 106, ll 19--21› sublocale kernel: ideal where I = additive.Ker by unfold_locales (auto simp: additive.Ker_image multiplicative.commutes_with_composition) end (* ring_homomorphism *) text ‹p 106, l 22› locale ring_monomorphism = ring_homomorphism + injective_map η R R' context ring_homomorphism begin text ‹p 106, ll 21--23› theorem ring_monomorphism_iff_kernel_unit: "ring_monomorphism η R (+) (⋅) 𝟬 𝟭 R' (+') (⋅') 𝟬' 𝟭' ⟷ additive.Ker = {𝟬}" (is "?monom ⟷ ?ker") proof assume ?monom then interpret ring_monomorphism . show ?ker by (simp add: additive.injective_iff_kernel_unit [symmetric]) next assume ?ker then show ?monom by unfold_locales (simp add: additive.injective_iff_kernel_unit) qed end (* ring_homomorphism *) text ‹p 106, ll 23--25› sublocale ring_homomorphism ⊆ image: subring "η ` R" R' "(+')" "(⋅')" "𝟬'" "𝟭'" .. text ‹p 106, ll 26--27› locale ideal_in_kernel = ring_homomorphism + contained: ideal I R "(+)" "(⋅)" 𝟬 𝟭 for I + assumes subset: "I ⊆ additive.Ker" begin text ‹p 106, ll 26--27› notation contained.additive.quotient_composition (infixl "[+]" 65) notation contained.multiplicative.quotient_composition (infixl "[⋅]" 70) text ‹Provides @{text additive.induced}, which Jacobson calls $\bar{\eta}$.› text ‹p 106, l 30› sublocale additive: normal_subgroup_in_kernel η R "(+)" 𝟬 R' "(+')" "𝟬'" I rewrites "normal_subgroup.Congruence I R addition zero = contained.Ring_Congruence" by unfold_locales (rule subset contained.additive_congruence)+ text ‹Only the multiplicative part needs some work.› text ‹p 106, ll 27--30› sublocale induced: ring_homomorphism additive.induced "R // I" "([+])" "([⋅])" "contained.additive.Class 𝟬" "contained.additive.Class 𝟭" using contained.multiplicative.Class_commutes_with_composition by unfold_locales (auto elim!: contained.additive.Left_CosetE simp: contained.additive.Class_is_Left_Coset multiplicative.commutes_with_composition multiplicative.commutes_with_unit) text ‹p 106, l 30; p 107, ll 1--3› text ‹ @{term additive.induced} denotes Jacobson's $\bar{\eta}$. We have the commutativity of the diagram, where @{term additive.induced} is unique: @{thm [display] additive.factorization} @{thm [display] additive.uniqueness} › end (* ideal_in_kernel *) text ‹Fundamental Theorem of Homomorphisms of Rings› text ‹p 107, l 6› locale ring_homomorphism_fundamental = ring_homomorphism begin text ‹p 107, l 6› notation kernel.additive.quotient_composition (infixl "[+]" 65) notation kernel.multiplicative.quotient_composition (infixl "[⋅]" 70) text ‹p 107, l 6› sublocale ideal_in_kernel where I = additive.Ker by unfold_locales rule text ‹p 107, ll 8--9› sublocale natural: ring_epimorphism where η = kernel.additive.Class and R' = "R // additive.Ker" and addition' = "kernel.additive.quotient_composition" and multiplication' = "kernel.multiplicative.quotient_composition" and zero' = "kernel.additive.Class 𝟬" and unit' = "kernel.additive.Class 𝟭" .. text ‹p 107, l 9› sublocale induced: ring_monomorphism where η = additive.induced and R = "R // additive.Ker" and addition = "kernel.additive.quotient_composition" and multiplication = "kernel.multiplicative.quotient_composition" and zero = "kernel.additive.Class 𝟬" and unit = "kernel.additive.Class 𝟭" by unfold_locales (simp add: additive.induced_inj_on) end (* ring_homomorphism_fundamental *) text ‹p 107, l 11› locale ring_isomorphism = ring_homomorphism + bijective_map η R R' begin text ‹p 107, l 11› sublocale ring_monomorphism .. sublocale ring_epimorphism .. text ‹p 107, l 11› lemma inverse_ring_isomorphism: "ring_isomorphism (restrict (inv_into R η) R') R' (+') (⋅') 𝟬' 𝟭' R (+) (⋅) 𝟬 𝟭" using additive.commutes_with_composition [symmetric] additive.commutes_with_unit multiplicative.commutes_with_composition [symmetric] multiplicative.commutes_with_unit surjective by unfold_locales auto end (* ring_isomorphsim *) text ‹p 107, l 11› definition isomorphic_as_rings (infixl "≅⇩_{R}" 50) where "ℛ ≅⇩_{R}ℛ' ⟷ (let (R, addition, multiplication, zero, unit) = ℛ; (R', addition', multiplication', zero', unit') = ℛ' in (∃η. ring_isomorphism η R addition multiplication zero unit R' addition' multiplication' zero' unit'))" text ‹p 107, l 11› lemma isomorphic_as_rings_symmetric: "(R, addition, multiplication, zero, unit) ≅⇩_{R}(R', addition', multiplication', zero', unit') ⟹ (R', addition', multiplication', zero', unit') ≅⇩_{R}(R, addition, multiplication, zero, unit)" by (simp add: isomorphic_as_rings_def) (meson ring_isomorphism.inverse_ring_isomorphism) context ring_homomorphism begin text ‹Corollary› text ‹p 107, ll 11--12› theorem image_is_isomorphic_to_quotient_ring: "∃K add mult zero one. ideal K R (+) (⋅) 𝟬 𝟭 ∧ (η ` R, (+'), (⋅'), 𝟬', 𝟭') ≅⇩_{R}(R // K, add, mult, zero, one)" proof - interpret image: ring_homomorphism_fundamental where R' = "η ` R" by unfold_locales (auto simp: target.additive.commutative additive.commutes_with_composition multiplicative.commutes_with_composition target.distributive multiplicative.commutes_with_unit) have "ring_isomorphism image.additive.induced (R // additive.Ker) ([+]) ([⋅]) (kernel.additive.Class 𝟬) (kernel.additive.Class 𝟭) (η ` R) (+') (⋅') 𝟬' 𝟭'" by unfold_locales (simp add: image.additive.induced_image bij_betw_def) then have "(η ` R, (+'), (⋅'), 𝟬', 𝟭') ≅⇩_{R}(R // additive.Ker, ([+]), ([⋅]), kernel.additive.Class 𝟬, kernel.additive.Class 𝟭)" by (simp add: isomorphic_as_rings_def) (meson ring_isomorphism.inverse_ring_isomorphism) moreover have "ideal additive.Ker R (+) (⋅) 𝟬 𝟭" .. ultimately show ?thesis by blast qed end (* ring_homomorphism *) end