src/HOL/Algebra/More_Group.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 66760 d44ea023ac09
child 67341 df79ef3b3a41
permissions -rw-r--r--
tuned: each session has at most one defining entry;
haftmann@65416
     1
(*  Title:      HOL/Algebra/More_Group.thy
haftmann@65416
     2
    Author:     Jeremy Avigad
haftmann@65416
     3
*)
haftmann@65416
     4
haftmann@65416
     5
section \<open>More on groups\<close>
haftmann@65416
     6
haftmann@65416
     7
theory More_Group
wenzelm@66760
     8
  imports Ring
haftmann@65416
     9
begin
haftmann@65416
    10
haftmann@65416
    11
text \<open>
haftmann@65416
    12
  Show that the units in any monoid give rise to a group.
haftmann@65416
    13
haftmann@65416
    14
  The file Residues.thy provides some infrastructure to use
haftmann@65416
    15
  facts about the unit group within the ring locale.
haftmann@65416
    16
\<close>
haftmann@65416
    17
wenzelm@66760
    18
definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
wenzelm@66760
    19
  where "units_of G =
wenzelm@66760
    20
    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
haftmann@65416
    21
wenzelm@66760
    22
lemma (in monoid) units_group: "group (units_of G)"
haftmann@65416
    23
  apply (unfold units_of_def)
haftmann@65416
    24
  apply (rule groupI)
wenzelm@66760
    25
      apply auto
wenzelm@66760
    26
   apply (subst m_assoc)
wenzelm@66760
    27
      apply auto
haftmann@65416
    28
  apply (rule_tac x = "inv x" in bexI)
wenzelm@66760
    29
   apply auto
haftmann@65416
    30
  done
haftmann@65416
    31
wenzelm@66760
    32
lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
haftmann@65416
    33
  apply (rule group.group_comm_groupI)
wenzelm@66760
    34
   apply (rule units_group)
haftmann@65416
    35
  apply (insert comm_monoid_axioms)
haftmann@65416
    36
  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
haftmann@65416
    37
  apply auto
haftmann@65416
    38
  done
haftmann@65416
    39
haftmann@65416
    40
lemma units_of_carrier: "carrier (units_of G) = Units G"
wenzelm@66760
    41
  by (auto simp: units_of_def)
haftmann@65416
    42
wenzelm@66760
    43
lemma units_of_mult: "mult (units_of G) = mult G"
wenzelm@66760
    44
  by (auto simp: units_of_def)
haftmann@65416
    45
wenzelm@66760
    46
lemma units_of_one: "one (units_of G) = one G"
wenzelm@66760
    47
  by (auto simp: units_of_def)
haftmann@65416
    48
wenzelm@66760
    49
lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
haftmann@65416
    50
  apply (rule sym)
haftmann@65416
    51
  apply (subst m_inv_def)
haftmann@65416
    52
  apply (rule the1_equality)
wenzelm@66760
    53
   apply (rule ex_ex1I)
wenzelm@66760
    54
    apply (subst (asm) Units_def)
wenzelm@66760
    55
    apply auto
wenzelm@66760
    56
     apply (erule inv_unique)
wenzelm@66760
    57
        apply auto
wenzelm@66760
    58
    apply (rule Units_closed)
wenzelm@66760
    59
    apply (simp_all only: units_of_carrier [symmetric])
wenzelm@66760
    60
    apply (insert units_group)
wenzelm@66760
    61
    apply auto
wenzelm@66760
    62
   apply (subst units_of_mult [symmetric])
wenzelm@66760
    63
   apply (subst units_of_one [symmetric])
wenzelm@66760
    64
   apply (erule group.r_inv, assumption)
haftmann@65416
    65
  apply (subst units_of_mult [symmetric])
haftmann@65416
    66
  apply (subst units_of_one [symmetric])
haftmann@65416
    67
  apply (erule group.l_inv, assumption)
haftmann@65416
    68
  done
haftmann@65416
    69
wenzelm@66760
    70
lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
haftmann@65416
    71
  unfolding inj_on_def by auto
haftmann@65416
    72
wenzelm@66760
    73
lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
haftmann@65416
    74
  apply (auto simp add: image_def)
haftmann@65416
    75
  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
haftmann@65416
    76
  apply auto
haftmann@65416
    77
(* auto should get this. I suppose we need "comm_monoid_simprules"
haftmann@65416
    78
   for ac_simps rewriting. *)
haftmann@65416
    79
  apply (subst m_assoc [symmetric])
haftmann@65416
    80
  apply auto
haftmann@65416
    81
  done
haftmann@65416
    82
wenzelm@66760
    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"
haftmann@65416
    84
  apply auto
haftmann@65416
    85
  apply (subst l_cancel [symmetric])
wenzelm@66760
    86
     prefer 4
wenzelm@66760
    87
     apply (erule ssubst)
wenzelm@66760
    88
     apply auto
haftmann@65416
    89
  done
haftmann@65416
    90
wenzelm@66760
    91
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"
haftmann@65416
    92
  apply auto
haftmann@65416
    93
  apply (subst r_cancel [symmetric])
wenzelm@66760
    94
     prefer 4
wenzelm@66760
    95
     apply (erule ssubst)
wenzelm@66760
    96
     apply auto
haftmann@65416
    97
  done
haftmann@65416
    98
haftmann@65416
    99
(* Is there a better way to do this? *)
wenzelm@66760
   100
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"
haftmann@65416
   101
  apply (subst eq_commute)
haftmann@65416
   102
  apply simp
haftmann@65416
   103
  done
haftmann@65416
   104
wenzelm@66760
   105
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"
haftmann@65416
   106
  apply (subst eq_commute)
haftmann@65416
   107
  apply simp
haftmann@65416
   108
  done
haftmann@65416
   109
haftmann@65416
   110
(* This should be generalized to arbitrary groups, not just commutative
haftmann@65416
   111
   ones, using Lagrange's theorem. *)
haftmann@65416
   112
haftmann@65416
   113
lemma (in comm_group) power_order_eq_one:
haftmann@65416
   114
  assumes fin [simp]: "finite (carrier G)"
wenzelm@66760
   115
    and a [simp]: "a \<in> carrier G"
haftmann@65416
   116
  shows "a (^) card(carrier G) = one G"
haftmann@65416
   117
proof -
haftmann@65416
   118
  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
haftmann@65416
   119
    by (subst (2) finprod_reindex [symmetric],
haftmann@65416
   120
      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
haftmann@65416
   121
  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
haftmann@65416
   122
    by (auto simp add: finprod_multf Pi_def)
haftmann@65416
   123
  also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
haftmann@65416
   124
    by (auto simp add: finprod_const)
haftmann@65416
   125
  finally show ?thesis
haftmann@65416
   126
(* uses the preceeding lemma *)
haftmann@65416
   127
    by auto
haftmann@65416
   128
qed
haftmann@65416
   129
haftmann@65416
   130
end