Proofs about Groups

An key part of mathematics is proofs, on this site I would like to include proofs in a consistant way across all the topics, I am therefore using a program called Isabelle which is a proof assistant. More about this program on this page.

So far, we don't have any of the imporant proofs on this page, just the initial constructions.

This is taken from Isabelle code (from this site) but I have not put the complete code here, just an outline.

Semigroup

We start with a semigroup, as an associative binary operation.

There is also an abelian group which add a commutitive axiom.

locale semigroup =
  fixes f :: "'a => 'a => 'a" (infixl "*" 70)
  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

locale abel_semigroup = semigroup +
  assumes commute [ac_simps]: "a * b = b * a"
begin

lemma left_commute [ac_simps]:
  "b * (a * c) = a * (b * c)"
proof -
  have "(b * a) * c = (a * b) * c"
    by (simp only: commute)
  then show ?thesis
    by (simp only: assoc)
qed

end

Monoids

We also add a monoid and commutative monoid which are the semigroups above with an identity element '1'.
locale monoid = semigroup +
  fixes z :: 'a ("1")
  assumes left_neutral [simp]: "1 * a = a"
  assumes right_neutral [simp]: "a * 1 = a"

locale comm_monoid = abel_semigroup +
  fixes z :: 'a ("1")
  assumes comm_neutral: "a * 1 = a"

sublocale comm_monoid < monoid proof
qed (simp_all add: commute comm_neutral)

Groups

Then, when groups are introduced in the Isabelle library code for groups, things seem to get a bit messy, there seems to be a switch over from '*' as the group operation to '+' even for non-abelian group.

Since we are using '+' for the binary operation then the inverse operation is a unary minus (-). We can also add a binary minus operation (although not part of the axioms) as shown here.
class group_add = minus + uminus + monoid_add +
  assumes left_minus [simp]: "- a + a = 0"
  assumes diff_minus: "a - b = a + (- b)"
begin

lemma minus_unique:
  assumes "a + b = 0" shows "- a = b"
proof -
  have "- a = - a + (a + b)" using assms by simp
  also have "… = b" by (simp add: add_assoc [symmetric])
  finally show ?thesis .
qed

lemma minus_zero [simp]: "- 0 = 0"
proof -
  have "0 + 0 = 0" by (rule add_0_right)
  thus "- 0 = 0" by (rule minus_unique)
qed

lemma minus_minus [simp]: "- (- a) = a"
proof -
  have "- a + a = 0" by (rule left_minus)
  thus "- (- a) = a" by (rule minus_unique)
qed

lemma right_minus [simp]: "a + - a = 0"
proof -
  have "a + - a = - (- a) + - a" by simp
  also have "… = 0" by (rule left_minus)
  finally show ?thesis .
qed

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Symmetry and the Monster - This is a popular science type book which traces the history leading up to the discovery of the largest symmetry groups.

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.