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.

Group Theory

The following problem is from [a Dutch math competition in 2014](https://www.a-eskwadraat.nl/Vereniging/Commissies/cieinfinity/MOAWOA%20Opgaven_2014.pdf). Let `G` be a group of which the commutator subgroup `[G, G]` is a subset of the 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 differently 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 is defined as `Z(G) = {z ∈ G | ∀ g ∈ G, z * g = g * z}`. **Hint**: If `f(a) = 1` then what do you know of the commutator of `a` with an arbitrary other element `b` of `G`?

Resources

Definitions File

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

Template File

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

Check File

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

Template File

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

Check 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

Terms and Conditions