Cookies disclaimer

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.

[Proof Ground 2021] Group Theory

Resources

Download Files

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
Download Files

Definitions File



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