src/HOL/Algebra/AbelCoset.thy
author ballarin
Thu, 03 Aug 2006 14:57:26 +0200
changeset 20318 0e0ea63fe768
child 21502 7f3ea2b3bab6
permissions -rw-r--r--
Restructured algebra library, added ideals and quotient rings.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     1
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     2
  Title:     HOL/Algebra/AbelCoset.thy
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     3
  Id:        $Id$
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     4
  Author:    Stephan Hohe, TU Muenchen
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     5
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     6
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     7
theory AbelCoset
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     8
imports Coset Ring
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
     9
begin
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    10
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    11
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    12
section {* More Lifting from Groups to Abelian Groups *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    13
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    14
subsection {* Definitions *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    15
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    16
text {* Hiding @{text "<+>"} from \texttt{Sum\_Type.thy} until I come
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    17
  up with better syntax here *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    18
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    19
hide const Plus
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    20
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    21
constdefs (structure G)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    22
  a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    23
  "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    24
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    25
  a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    26
  "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    27
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    28
  A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _" [81] 80)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    29
  "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    30
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    31
  set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    32
  "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    33
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    34
  A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _" [81] 80)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    35
  "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    36
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    37
constdefs (structure G)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    38
  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    39
                  ("racong\<index> _")
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    40
   "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    41
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    42
constdefs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    43
  A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    44
     (infixl "A'_Mod" 65)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    45
    --{*Actually defined for groups rather than monoids*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    46
  "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    47
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    48
constdefs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    49
  a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    50
             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    51
    --{*the kernel of a homomorphism (additive)*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    52
  "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    53
                              \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    54
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    55
locale abelian_group_hom = abelian_group G + abelian_group H + var h +
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    56
  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    57
                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    58
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    59
lemmas a_r_coset_defs =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    60
  a_r_coset_def r_coset_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    61
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    62
lemma a_r_coset_def':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    63
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    64
  shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    65
unfolding a_r_coset_defs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    66
by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    67
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    68
lemmas a_l_coset_defs =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    69
  a_l_coset_def l_coset_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    70
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    71
lemma a_l_coset_def':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    72
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    73
  shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    74
unfolding a_l_coset_defs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    75
by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    76
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    77
lemmas A_RCOSETS_defs =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    78
  A_RCOSETS_def RCOSETS_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    79
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    80
lemma A_RCOSETS_def':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    81
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    82
  shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    83
unfolding A_RCOSETS_defs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    84
by (fold a_r_coset_def, simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    85
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    86
lemmas set_add_defs =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    87
  set_add_def set_mult_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    88
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    89
lemma set_add_def':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    90
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    91
  shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    92
unfolding set_add_defs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    93
by simp
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    94
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    95
lemmas A_SET_INV_defs =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    96
  A_SET_INV_def SET_INV_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    97
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    98
lemma A_SET_INV_def':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
    99
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   100
  shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   101
unfolding A_SET_INV_defs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   102
by (fold a_inv_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   103
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   104
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   105
subsection {* Cosets *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   106
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   107
lemma (in abelian_group) a_coset_add_assoc:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   108
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   109
      ==> (M +> g) +> h = M +> (g \<oplus> h)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   110
by (rule group.coset_mult_assoc [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   111
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   112
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   113
lemma (in abelian_group) a_coset_add_zero [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   114
  "M \<subseteq> carrier G ==> M +> \<zero> = M"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   115
by (rule group.coset_mult_one [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   116
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   117
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   118
lemma (in abelian_group) a_coset_add_inv1:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   119
     "[| M +> (x \<oplus> (\<ominus> y)) = M;  x \<in> carrier G ; y \<in> carrier G;
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   120
         M \<subseteq> carrier G |] ==> M +> x = M +> y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   121
by (rule group.coset_mult_inv1 [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   122
    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   123
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   124
lemma (in abelian_group) a_coset_add_inv2:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   125
     "[| M +> x = M +> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   126
      ==> M +> (x \<oplus> (\<ominus> y)) = M"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   127
by (rule group.coset_mult_inv2 [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   128
    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   129
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   130
lemma (in abelian_group) a_coset_join1:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   131
     "[| H +> x = H;  x \<in> carrier G;  subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   132
by (rule group.coset_join1 [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   133
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   134
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   135
lemma (in abelian_group) a_solve_equation:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   136
    "\<lbrakk>subgroup H (|carrier = carrier G, mult = add G, one = zero G|); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   137
by (rule group.solve_equation [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   138
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   139
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   140
lemma (in abelian_group) a_repr_independence:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   141
     "\<lbrakk>y \<in> H +> x;  x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<rbrakk> \<Longrightarrow> H +> x = H +> y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   142
by (rule group.repr_independence [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   143
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   144
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   145
lemma (in abelian_group) a_coset_join2:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   146
     "\<lbrakk>x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>; x\<in>H\<rbrakk> \<Longrightarrow> H +> x = H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   147
by (rule group.coset_join2 [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   148
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   149
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   150
lemma (in abelian_monoid) a_r_coset_subset_G:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   151
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H +> x \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   152
by (rule monoid.r_coset_subset_G [OF a_monoid,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   153
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   154
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   155
lemma (in abelian_group) a_rcosI:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   156
     "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   157
by (rule group.rcosI [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   158
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   159
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   160
lemma (in abelian_group) a_rcosetsI:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   161
     "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H +> x \<in> a_rcosets H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   162
by (rule group.rcosetsI [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   163
    folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   164
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   165
text{*Really needed?*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   166
lemma (in abelian_group) a_transpose_inv:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   167
     "[| x \<oplus> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   168
      ==> (\<ominus> x) \<oplus> z = y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   169
by (rule group.transpose_inv [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   170
    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   171
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   172
(*
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   173
--"duplicate"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   174
lemma (in abelian_group) a_rcos_self:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   175
     "[| x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   176
by (rule group.rcos_self [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   177
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   178
*)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   179
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   180
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   181
subsection {* Subgroups *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   182
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   183
locale additive_subgroup = var H + struct G +
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   184
  assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   185
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   186
lemma (in additive_subgroup) is_additive_subgroup:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   187
  shows "additive_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   188
by -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   189
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   190
lemma additive_subgroupI:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   191
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   192
  assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   193
  shows "additive_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   194
by (rule additive_subgroup.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   195
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   196
lemma (in additive_subgroup) a_subset:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   197
     "H \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   198
by (rule subgroup.subset[OF a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   199
    simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   200
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   201
lemma (in additive_subgroup) a_closed [intro, simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   202
     "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> y \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   203
by (rule subgroup.m_closed[OF a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   204
    simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   205
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   206
lemma (in additive_subgroup) zero_closed [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   207
     "\<zero> \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   208
by (rule subgroup.one_closed[OF a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   209
    simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   210
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   211
lemma (in additive_subgroup) a_inv_closed [intro,simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   212
     "x \<in> H \<Longrightarrow> \<ominus> x \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   213
by (rule subgroup.m_inv_closed[OF a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   214
    folded a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   215
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   216
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   217
subsection {* Normal additive subgroups *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   218
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   219
subsubsection {* Definition of @{text "abelian_subgroup"} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   220
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   221
text {* Every subgroup of an @{text "abelian_group"} is normal *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   222
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   223
locale abelian_subgroup = additive_subgroup H G + abelian_group G +
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   224
  assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   225
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   226
lemma (in abelian_subgroup) is_abelian_subgroup:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   227
  shows "abelian_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   228
by -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   229
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   230
lemma abelian_subgroupI:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   231
  assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   232
      and a_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus>\<^bsub>G\<^esub> y = y \<oplus>\<^bsub>G\<^esub> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   233
  shows "abelian_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   234
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   235
  interpret normal ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   236
  by (rule a_normal)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   237
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   238
  show "abelian_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   239
  by (unfold_locales, simp add: a_comm)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   240
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   241
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   242
lemma abelian_subgroupI2:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   243
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   244
  assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   245
      and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   246
  shows "abelian_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   247
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   248
  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   249
  by (rule a_comm_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   250
  interpret subgroup ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   251
  by (rule a_subgroup)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   252
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   253
  show "abelian_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   254
  apply unfold_locales
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   255
  proof (simp add: r_coset_def l_coset_def, clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   256
    fix x
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   257
    assume xcarr: "x \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   258
    from a_subgroup
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   259
        have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   260
    from xcarr Hcarr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   261
        show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   262
        using m_comm[simplified]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   263
        by fast
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   264
  qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   265
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   266
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   267
lemma abelian_subgroupI3:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   268
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   269
  assumes asg: "additive_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   270
      and ag: "abelian_group G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   271
  shows "abelian_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   272
apply (rule abelian_subgroupI2)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   273
 apply (rule abelian_group.a_comm_group[OF ag])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   274
apply (rule additive_subgroup.a_subgroup[OF asg])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   275
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   276
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   277
lemma (in abelian_subgroup) a_coset_eq:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   278
     "(\<forall>x \<in> carrier G. H +> x = x <+ H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   279
by (rule normal.coset_eq[OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   280
    folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   281
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   282
lemma (in abelian_subgroup) a_inv_op_closed1:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   283
  shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> h \<oplus> x \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   284
by (rule normal.inv_op_closed1 [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   285
    folded a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   286
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   287
lemma (in abelian_subgroup) a_inv_op_closed2:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   288
  shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus> x) \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   289
by (rule normal.inv_op_closed2 [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   290
    folded a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   291
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   292
text{*Alternative characterization of normal subgroups*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   293
lemma (in abelian_group) a_normal_inv_iff:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   294
     "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) = 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   295
      (subgroup N \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   296
      (is "_ = ?rhs")
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   297
by (rule group.normal_inv_iff [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   298
    folded a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   299
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   300
lemma (in abelian_group) a_lcos_m_assoc:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   301
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   302
      ==> g <+ (h <+ M) = (g \<oplus> h) <+ M"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   303
by (rule group.lcos_m_assoc [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   304
    folded a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   305
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   306
lemma (in abelian_group) a_lcos_mult_one:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   307
     "M \<subseteq> carrier G ==> \<zero> <+ M = M"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   308
by (rule group.lcos_mult_one [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   309
    folded a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   310
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   311
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   312
lemma (in abelian_group) a_l_coset_subset_G:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   313
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <+ H \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   314
by (rule group.l_coset_subset_G [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   315
    folded a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   316
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   317
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   318
lemma (in abelian_group) a_l_coset_swap:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   319
     "\<lbrakk>y \<in> x <+ H;  x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>\<rbrakk> \<Longrightarrow> x \<in> y <+ H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   320
by (rule group.l_coset_swap [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   321
    folded a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   322
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   323
lemma (in abelian_group) a_l_coset_carrier:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   324
     "[| y \<in> x <+ H;  x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> y \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   325
by (rule group.l_coset_carrier [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   326
    folded a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   327
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   328
lemma (in abelian_group) a_l_repr_imp_subset:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   329
  assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   330
  shows "y <+ H \<subseteq> x <+ H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   331
by (rule group.l_repr_imp_subset [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   332
    folded a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   333
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   334
lemma (in abelian_group) a_l_repr_independence:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   335
  assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   336
  shows "x <+ H = y <+ H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   337
by (rule group.l_repr_independence [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   338
    folded a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   339
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   340
lemma (in abelian_group) setadd_subset_G:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   341
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   342
by (rule group.setmult_subset_G [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   343
    folded set_add_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   344
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   345
lemma (in abelian_group) subgroup_add_id: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<Longrightarrow> H <+> H = H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   346
by (rule group.subgroup_mult_id [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   347
    folded set_add_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   348
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   349
lemma (in abelian_subgroup) a_rcos_inv:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   350
  assumes x:     "x \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   351
  shows "a_set_inv (H +> x) = H +> (\<ominus> x)" 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   352
by (rule normal.rcos_inv [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   353
    folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   354
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   355
lemma (in abelian_group) a_setmult_rcos_assoc:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   356
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   357
      \<Longrightarrow> H <+> (K +> x) = (H <+> K) +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   358
by (rule group.setmult_rcos_assoc [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   359
    folded set_add_def a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   360
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   361
lemma (in abelian_group) a_rcos_assoc_lcos:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   362
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   363
      \<Longrightarrow> (H +> x) <+> K = H <+> (x <+ K)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   364
by (rule group.rcos_assoc_lcos [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   365
     folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   366
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   367
lemma (in abelian_subgroup) a_rcos_sum:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   368
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   369
      \<Longrightarrow> (H +> x) <+> (H +> y) = H +> (x \<oplus> y)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   370
by (rule normal.rcos_sum [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   371
    folded set_add_def a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   372
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   373
lemma (in abelian_subgroup) rcosets_add_eq:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   374
  "M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   375
  -- {* generalizes @{text subgroup_mult_id} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   376
by (rule normal.rcosets_mult_eq [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   377
    folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   378
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   379
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   380
subsection {* Congruence Relation *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   381
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   382
lemma (in abelian_subgroup) a_equiv_rcong:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   383
   shows "equiv (carrier G) (racong H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   384
by (rule subgroup.equiv_rcong [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   385
    folded a_r_congruent_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   386
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   387
lemma (in abelian_subgroup) a_l_coset_eq_rcong:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   388
  assumes a: "a \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   389
  shows "a <+ H = racong H `` {a}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   390
by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   391
    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   392
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   393
lemma (in abelian_subgroup) a_rcos_equation:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   394
  shows
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   395
     "\<lbrakk>ha \<oplus> a = h \<oplus> b; a \<in> carrier G;  b \<in> carrier G;  
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   396
        h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   397
      \<Longrightarrow> hb \<oplus> a \<in> (\<Union>h\<in>H. {h \<oplus> b})"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   398
by (rule group.rcos_equation [OF a_group a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   399
    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   400
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   401
lemma (in abelian_subgroup) a_rcos_disjoint:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   402
  shows "\<lbrakk>a \<in> a_rcosets H; b \<in> a_rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   403
by (rule group.rcos_disjoint [OF a_group a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   404
    folded A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   405
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   406
lemma (in abelian_subgroup) a_rcos_self:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   407
  shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   408
by (rule group.rcos_self [OF a_group a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   409
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   410
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   411
lemma (in abelian_subgroup) a_rcosets_part_G:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   412
  shows "\<Union>(a_rcosets H) = carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   413
by (rule group.rcosets_part_G [OF a_group a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   414
    folded A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   415
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   416
lemma (in abelian_subgroup) a_cosets_finite:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   417
     "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   418
by (rule group.cosets_finite [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   419
    folded A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   420
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   421
lemma (in abelian_group) a_card_cosets_equal:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   422
     "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   423
      \<Longrightarrow> card c = card H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   424
by (rule group.card_cosets_equal [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   425
    folded A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   426
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   427
lemma (in abelian_group) rcosets_subset_PowG:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   428
     "additive_subgroup H G  \<Longrightarrow> a_rcosets H \<subseteq> Pow(carrier G)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   429
by (rule group.rcosets_subset_PowG [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   430
    folded A_RCOSETS_def, simplified monoid_record_simps],
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   431
    rule additive_subgroup.a_subgroup)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   432
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   433
theorem (in abelian_group) a_lagrange:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   434
     "\<lbrakk>finite(carrier G); additive_subgroup H G\<rbrakk>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   435
      \<Longrightarrow> card(a_rcosets H) * card(H) = order(G)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   436
by (rule group.lagrange [OF a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   437
    folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   438
    (fast intro!: additive_subgroup.a_subgroup)+
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   439
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   440
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   441
subsection {* Factorization *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   442
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   443
lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   444
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   445
lemma A_FactGroup_def':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   446
  includes struct G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   447
  shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   448
unfolding A_FactGroup_defs
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   449
by (fold A_RCOSETS_def set_add_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   450
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   451
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   452
lemma (in abelian_subgroup) a_setmult_closed:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   453
     "\<lbrakk>K1 \<in> a_rcosets H; K2 \<in> a_rcosets H\<rbrakk> \<Longrightarrow> K1 <+> K2 \<in> a_rcosets H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   454
by (rule normal.setmult_closed [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   455
    folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   456
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   457
lemma (in abelian_subgroup) a_setinv_closed:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   458
     "K \<in> a_rcosets H \<Longrightarrow> a_set_inv K \<in> a_rcosets H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   459
by (rule normal.setinv_closed [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   460
    folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   461
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   462
lemma (in abelian_subgroup) a_rcosets_assoc:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   463
     "\<lbrakk>M1 \<in> a_rcosets H; M2 \<in> a_rcosets H; M3 \<in> a_rcosets H\<rbrakk>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   464
      \<Longrightarrow> M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   465
by (rule normal.rcosets_assoc [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   466
    folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   467
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   468
lemma (in abelian_subgroup) a_subgroup_in_rcosets:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   469
     "H \<in> a_rcosets H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   470
by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   471
    folded A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   472
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   473
lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   474
     "M \<in> a_rcosets H \<Longrightarrow> a_set_inv M <+> M = H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   475
by (rule normal.rcosets_inv_mult_group_eq [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   476
    folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   477
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   478
theorem (in abelian_subgroup) a_factorgroup_is_group:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   479
  "group (G A_Mod H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   480
by (rule normal.factorgroup_is_group [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   481
    folded A_FactGroup_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   482
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   483
text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   484
        a commutative group *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   485
theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   486
  "comm_group (G A_Mod H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   487
apply (intro comm_group.intro comm_monoid.intro) prefer 3
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   488
  apply (rule a_factorgroup_is_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   489
 apply (rule group.axioms[OF a_factorgroup_is_group])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   490
apply (rule comm_monoid_axioms.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   491
apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   492
apply (simp add: a_rcos_sum a_comm)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   493
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   494
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   495
lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   496
by (simp add: A_FactGroup_def set_add_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   497
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   498
lemma (in abelian_subgroup) a_inv_FactGroup:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   499
     "X \<in> carrier (G A_Mod H) \<Longrightarrow> inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   500
by (rule normal.inv_FactGroup [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   501
    folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   502
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   503
text{*The coset map is a homomorphism from @{term G} to the quotient group
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   504
  @{term "G Mod H"}*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   505
lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   506
  "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   507
by (rule normal.r_coset_hom_Mod [OF a_normal,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   508
    folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   509
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   510
text {* The isomorphism theorems have been omitted from lifting, at
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   511
  least for now *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   512
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   513
subsection{*The First Isomorphism Theorem*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   514
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   515
text{*The quotient by the kernel of a homomorphism is isomorphic to the 
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   516
  range of that homomorphism.*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   517
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   518
lemmas a_kernel_defs =
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   519
  a_kernel_def kernel_def
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   520
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   521
lemma a_kernel_def':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   522
  "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   523
by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   524
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   525
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   526
subsection {* Homomorphisms *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   527
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   528
lemma abelian_group_homI:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   529
  includes abelian_group G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   530
  includes abelian_group H
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   531
  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   532
                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   533
  shows "abelian_group_hom G H h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   534
by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   535
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   536
lemma (in abelian_group_hom) is_abelian_group_hom:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   537
  "abelian_group_hom G H h"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   538
by (unfold_locales)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   539
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   540
lemma (in abelian_group_hom) hom_add [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   541
  "[| x : carrier G; y : carrier G |]
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   542
        ==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   543
by (rule group_hom.hom_mult[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   544
    simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   545
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   546
lemma (in abelian_group_hom) hom_closed [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   547
  "x \<in> carrier G \<Longrightarrow> h x \<in> carrier H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   548
by (rule group_hom.hom_closed[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   549
    simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   550
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   551
lemma (in abelian_group_hom) zero_closed [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   552
  "h \<zero> \<in> carrier H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   553
by (rule group_hom.one_closed[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   554
    simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   555
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   556
lemma (in abelian_group_hom) hom_zero [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   557
  "h \<zero> = \<zero>\<^bsub>H\<^esub>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   558
by (rule group_hom.hom_one[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   559
    simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   560
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   561
lemma (in abelian_group_hom) a_inv_closed [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   562
  "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   563
by (rule group_hom.inv_closed[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   564
    folded a_inv_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   565
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   566
lemma (in abelian_group_hom) hom_a_inv [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   567
  "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   568
by (rule group_hom.hom_inv[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   569
    folded a_inv_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   570
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   571
lemma (in abelian_group_hom) additive_subgroup_a_kernel:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   572
  "additive_subgroup (a_kernel G H h) G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   573
apply (rule additive_subgroup.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   574
apply (rule group_hom.subgroup_kernel[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   575
       folded a_kernel_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   576
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   577
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   578
text{*The kernel of a homomorphism is an abelian subgroup*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   579
lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   580
  "abelian_subgroup (a_kernel G H h) G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   581
apply (rule abelian_subgroupI)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   582
apply (rule group_hom.normal_kernel[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   583
       folded a_kernel_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   584
apply (simp add: G.a_comm)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   585
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   586
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   587
lemma (in abelian_group_hom) A_FactGroup_nonempty:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   588
  assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   589
  shows "X \<noteq> {}"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   590
by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   591
    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   592
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   593
lemma (in abelian_group_hom) FactGroup_contents_mem:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   594
  assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   595
  shows "contents (h`X) \<in> carrier H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   596
by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   597
    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   598
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   599
lemma (in abelian_group_hom) A_FactGroup_hom:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   600
     "(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   601
          \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   602
by (rule group_hom.FactGroup_hom[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   603
    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   604
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   605
lemma (in abelian_group_hom) A_FactGroup_inj_on:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   606
     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   607
by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   608
    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   609
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   610
text{*If the homomorphism @{term h} is onto @{term H}, then so is the
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   611
homomorphism from the quotient group*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   612
lemma (in abelian_group_hom) A_FactGroup_onto:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   613
  assumes h: "h ` carrier G = carrier H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   614
  shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   615
by (rule group_hom.FactGroup_onto[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   616
    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   617
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   618
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   619
 quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   620
theorem (in abelian_group_hom) A_FactGroup_iso:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   621
  "h ` carrier G = carrier H
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   622
   \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   623
          (| carrier = carrier H, mult = add H, one = zero H |)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   624
by (rule group_hom.FactGroup_iso[OF a_group_hom,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   625
    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   626
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   627
section {* Lemmas Lifted from CosetExt.thy *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   628
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   629
text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   630
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   631
subsection {* General Lemmas from \texttt{AlgebraExt.thy} *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   632
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   633
lemma (in additive_subgroup) a_Hcarr [simp]:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   634
  assumes hH: "h \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   635
  shows "h \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   636
by (rule subgroup.mem_carrier [OF a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   637
    simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   638
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   639
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   640
subsection {* Lemmas for Right Cosets *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   641
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   642
lemma (in abelian_subgroup) a_elemrcos_carrier:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   643
  assumes acarr: "a \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   644
      and a': "a' \<in> H +> a"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   645
  shows "a' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   646
by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   647
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   648
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   649
lemma (in abelian_subgroup) a_rcos_const:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   650
  assumes hH: "h \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   651
  shows "H +> h = H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   652
by (rule subgroup.rcos_const [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   653
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   654
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   655
lemma (in abelian_subgroup) a_rcos_module_imp:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   656
  assumes xcarr: "x \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   657
      and x'cos: "x' \<in> H +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   658
  shows "(x' \<oplus> \<ominus>x) \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   659
by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   660
    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   661
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   662
lemma (in abelian_subgroup) a_rcos_module_rev:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   663
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   664
      and xixH: "(x' \<oplus> \<ominus>x) \<in> H"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   665
  shows "x' \<in> H +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   666
by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   667
    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   668
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   669
lemma (in abelian_subgroup) a_rcos_module:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   670
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   671
  shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   672
by (rule subgroup.rcos_module [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   673
    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   674
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   675
--"variant"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   676
lemma (in abelian_subgroup) a_rcos_module_minus:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   677
  includes ring G
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   678
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   679
  shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   680
proof -
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   681
  from carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   682
      have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   683
  from this and carr
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   684
      show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   685
      by (simp add: minus_eq)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   686
qed
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   687
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   688
lemma (in abelian_subgroup) a_repr_independence':
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   689
  assumes "y \<in> H +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   690
      and "x \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   691
  shows "H +> x = H +> y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   692
apply (rule a_repr_independence, assumption+)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   693
apply (rule a_subgroup)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   694
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   695
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   696
lemma (in abelian_subgroup) a_repr_independenceD:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   697
  assumes ycarr: "y \<in> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   698
      and repr:  "H +> x = H +> y"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   699
  shows "y \<in> H +> x"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   700
by (rule group.repr_independenceD [OF a_group a_subgroup,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   701
    folded a_r_coset_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   702
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   703
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   704
subsection {* Lemmas for the Set of Right Cosets *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   705
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   706
lemma (in abelian_subgroup) a_rcosets_carrier:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   707
  "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   708
by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   709
    folded A_RCOSETS_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   710
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   711
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   712
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   713
subsection {* Addition of Subgroups *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   714
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   715
lemma (in abelian_monoid) set_add_closed:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   716
  assumes Acarr: "A \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   717
      and Bcarr: "B \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   718
  shows "A <+> B \<subseteq> carrier G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   719
by (rule monoid.set_mult_closed [OF a_monoid,
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   720
    folded set_add_def, simplified monoid_record_simps])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   721
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   722
lemma (in abelian_group) add_additive_subgroups:
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   723
  assumes subH: "additive_subgroup H G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   724
      and subK: "additive_subgroup K G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   725
  shows "additive_subgroup (H <+> K) G"
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   726
apply (rule additive_subgroup.intro)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   727
apply (unfold set_add_def)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   728
apply (intro comm_group.mult_subgroups)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   729
  apply (rule a_comm_group)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   730
 apply (rule additive_subgroup.a_subgroup[OF subH])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   731
apply (rule additive_subgroup.a_subgroup[OF subK])
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   732
done
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   733
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff changeset
   734
end