src/HOL/Algebra/More_Group.thy
author paulson <lp15@cam.ac.uk>
Wed Jun 06 14:25:53 2018 +0100 (12 months ago)
changeset 68399 0b71d08528f0
parent 67341 df79ef3b3a41
permissions -rw-r--r--
resolution of name clashes in Algebra
     1 (*  Title:      HOL/Algebra/More_Group.thy
     2     Author:     Jeremy Avigad
     3 *)
     4 
     5 section \<open>More on groups\<close>
     6 
     7 theory More_Group
     8   imports Ring
     9 begin
    10 
    11 text \<open>
    12   Show that the units in any monoid give rise to a group.
    13 
    14   The file Residues.thy provides some infrastructure to use
    15   facts about the unit group within the ring locale.
    16 \<close>
    17 
    18 definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
    19   where "units_of G =
    20     \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
    21 
    22 lemma (in monoid) units_group: "group (units_of G)"
    23   apply (unfold units_of_def)
    24   apply (rule groupI)
    25       apply auto
    26    apply (subst m_assoc)
    27       apply auto
    28   apply (rule_tac x = "inv x" in bexI)
    29    apply auto
    30   done
    31 
    32 lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
    33   apply (rule group.group_comm_groupI)
    34    apply (rule units_group)
    35   apply (insert comm_monoid_axioms)
    36   apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    37   apply auto
    38   done
    39 
    40 lemma units_of_carrier: "carrier (units_of G) = Units G"
    41   by (auto simp: units_of_def)
    42 
    43 lemma units_of_mult: "mult (units_of G) = mult G"
    44   by (auto simp: units_of_def)
    45 
    46 lemma units_of_one: "one (units_of G) = one G"
    47   by (auto simp: units_of_def)
    48 
    49 lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
    50   apply (rule sym)
    51   apply (subst m_inv_def)
    52   apply (rule the1_equality)
    53    apply (rule ex_ex1I)
    54     apply (subst (asm) Units_def)
    55     apply auto
    56      apply (erule inv_unique)
    57         apply auto
    58     apply (rule Units_closed)
    59     apply (simp_all only: units_of_carrier [symmetric])
    60     apply (insert units_group)
    61     apply auto
    62    apply (subst units_of_mult [symmetric])
    63    apply (subst units_of_one [symmetric])
    64    apply (erule group.r_inv, assumption)
    65   apply (subst units_of_mult [symmetric])
    66   apply (subst units_of_one [symmetric])
    67   apply (erule group.l_inv, assumption)
    68   done
    69 
    70 lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
    71   unfolding inj_on_def by auto
    72 
    73 lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
    74   apply (auto simp add: image_def)
    75   apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
    76   apply auto
    77 (* auto should get this. I suppose we need "comm_monoid_simprules"
    78    for ac_simps rewriting. *)
    79   apply (subst m_assoc [symmetric])
    80   apply auto
    81   done
    82 
    83 lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
    84   by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
    85 
    86 lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
    87   by (metis monoid.l_one monoid_axioms one_closed right_cancel)
    88 
    89 lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
    90   using l_cancel_one by fastforce
    91 
    92 lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
    93   using r_cancel_one by fastforce
    94 
    95 (* This should be generalized to arbitrary groups, not just commutative
    96    ones, using Lagrange's theorem. *)
    97 
    98 lemma (in comm_group) power_order_eq_one:
    99   assumes fin [simp]: "finite (carrier G)"
   100     and a [simp]: "a \<in> carrier G"
   101   shows "a [^] card(carrier G) = one G"
   102 proof -
   103   have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
   104     by (subst (2) finprod_reindex [symmetric],
   105       auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   106   also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
   107     by (auto simp add: finprod_multf Pi_def)
   108   also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
   109     by (auto simp add: finprod_const)
   110   finally show ?thesis
   111 (* uses the preceeding lemma *)
   112     by auto
   113 qed
   114 
   115 end