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.

Download Files
### Definitions File

### Template File

### Check 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

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

Download Files
### Definitions File

### Template File

### Check 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

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