I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
theory Defs
imports "HOL-Algebra.Generated_Groups"
begin
text \<open>In case you are a unfamiliar with \<open>HOL-Algebra\<close>, here is a very brief primer:
\<^item> Groups are ``structures''. Usually we need to refer to these structures explicitly, i.e.
@{term "\<one>\<^bsub>H\<^esub>"}, @{term "(\<otimes>\<^bsub>H\<^esub>)"}, \<open>inv\<^bsub>H\<^esub>\<close> are the neutral element, the group operation, and the
inverse of group \<open>H\<close>, respectively.
\<^item> We fix the group \<open>G\<close> below, so \<open>\<one>\<close>, \<open>\<otimes>\<close>, \<open>inv\<close> will refer to \<open>G\<close> implicitly.
\<^item> The carrier set of a group \<open>G\<close> is denoted @{term "carrier G"}.
\<^item> Don't forget that most existing theorems (e.g. @{thm hom_mult}) will need to be equipped with the
facts \<open>hom\<close>, \<open>group_G\<close>, \<open>group_H\<close>, \<open>x \<in> carrier G\<close>, \<dots>.
\<close>
definition (in group)
"center = {z \<in> carrier G . \<forall> g \<in> carrier G. z \<otimes> g = g \<otimes> z}"
end
theory Submission
imports Defs
begin
text \<open>In case you are a unfamiliar with \<open>HOL-Algebra\<close>, here is a very brief primer:
\<^item> Groups are ``structures''. Usually we need to refer to these structures explicitly, i.e.
@{term "\<one>\<^bsub>H\<^esub>"}, @{term "(\<otimes>\<^bsub>H\<^esub>)"}, \<open>inv\<^bsub>H\<^esub>\<close> are the neutral element, the group operation, and the
inverse of group \<open>H\<close>, respectively.
\<^item> We fix the group \<open>G\<close> below, so \<open>\<one>\<close>, \<open>\<otimes>\<close>, \<open>inv\<close> will refer to \<open>G\<close> implicitly.
\<^item> The carrier set of a group \<open>G\<close> is denoted @{term "carrier G"}.
\<^item> Don't forget that most existing theorems (e.g. @{thm hom_mult}) will need to be equipped with the
facts \<open>hom\<close>, \<open>group_G\<close>, \<open>group_H\<close>, \<open>x \<in> carrier G\<close>, \<dots>.
\<close>
theorem solution:
fixes G (structure) and H (structure) and f
assumes
hom: "f \<in> hom G H" and
group_G: "group G" and
group_H: "group H" and
h1: "\<forall>a b. a \<otimes> b \<otimes> inv a \<otimes> inv b \<in> group.center G" and
h2: "\<forall>x \<in> group.center G. f x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>"
shows "inj_on f (carrier G)"
sorry
end
theory Check
imports Submission
begin
theorem solution:
fixes G (structure) and H (structure) and f
assumes
hom: "f \<in> hom G H" and
group_G: "group G" and
group_H: "group H" and
h1: "\<forall>a b. a \<otimes> b \<otimes> inv a \<otimes> inv b \<in> group.center G" and
h2: "\<forall>x \<in> group.center G. f x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>"
shows "inj_on f (carrier G)"
using assms by (rule Submission.solution)
end
import group_theory.subgroup
open function subgroup
/-
Let `G` be a group of which the commutator subgroup `[G, G]` is a subset of het center `Z(G)`.
Suppose that `f : G → H` is a homomorphism from `G` to a group `H` with the property that the
restriction of `f` to `Z(G)` is injective. Prove that `f` is injective.
The hypotheses are formulated slightly in the formal statement.
Recall:
- The commutator subgroup `[G, G]` is the subgroup that is generated by all commutators
`a * b * a⁻¹ * b⁻¹`.
- The center `Z(G) = {z ∈ G | ∀ g ∈ G, z * g = g * z}`.
-/
lemma group_theory_problem {G H : Type*} [group G] [group H] (f : G →* H)
(h1 : ∀ a b, a * b * a⁻¹ * b⁻¹ ∈ center G) (h2 : ∀ x ∈ center G, f x = 1 → x = 1) :
injective f :=
sorry
-- A hint is provided in the solutions file
import .submission
open function subgroup
lemma check {G H : Type*} [group G] [group H] : ∀ (f : G →* H)
(h1 : ∀ a b, a * b * a⁻¹ * b⁻¹ ∈ center G) (h2 : ∀ x ∈ center G, f x = 1 → x = 1),
injective f :=
group_theory_problem