(* Title: HOL/Algebra/AbelCoset.thy
Author: Stephan Hohe, TU Muenchen
*)
theory AbelCoset
imports Coset Ring
begin
subsection \More Lifting from Groups to Abelian Groups\
subsubsection \Definitions\
text \Hiding \<+>\ from @{theory Sum_Type} until I come
up with better syntax here\
no_notation Sum_Type.Plus (infixr "<+>" 65)
definition
a_r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "+>\" 60)
where "a_r_coset G = r_coset \carrier = carrier G, mult = add G, one = zero G\"
definition
a_l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<+\" 60)
where "a_l_coset G = l_coset \carrier = carrier G, mult = add G, one = zero G\"
definition
A_RCOSETS :: "[_, 'a set] \ ('a set)set" ("a'_rcosets\ _" [81] 80)
where "A_RCOSETS G H = RCOSETS \carrier = carrier G, mult = add G, one = zero G\ H"
definition
set_add :: "[_, 'a set ,'a set] \ 'a set" (infixl "<+>\" 60)
where "set_add G = set_mult \carrier = carrier G, mult = add G, one = zero G\"
definition
A_SET_INV :: "[_,'a set] \ 'a set" ("a'_set'_inv\ _" [81] 80)
where "A_SET_INV G H = SET_INV \carrier = carrier G, mult = add G, one = zero G\ H"
definition
a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \ ('a*'a)set" ("racong\")
where "a_r_congruent G = r_congruent \carrier = carrier G, mult = add G, one = zero G\"
definition
A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \ ('a set) monoid" (infixl "A'_Mod" 65)
\\Actually defined for groups rather than monoids\
where "A_FactGroup G H = FactGroup \carrier = carrier G, mult = add G, one = zero G\ H"
definition
a_kernel :: "('a, 'm) ring_scheme \ ('b, 'n) ring_scheme \ ('a \ 'b) \ 'a set"
\\the kernel of a homomorphism (additive)\
where "a_kernel G H h =
kernel \carrier = carrier G, mult = add G, one = zero G\
\carrier = carrier H, mult = add H, one = zero H\ h"
locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H
for G (structure) and H (structure) +
fixes h
assumes a_group_hom: "group_hom \carrier = carrier G, mult = add G, one = zero G\
\carrier = carrier H, mult = add H, one = zero H\ h"
lemmas a_r_coset_defs =
a_r_coset_def r_coset_def
lemma a_r_coset_def':
fixes G (structure)
shows "H +> a \ \h\H. {h \ a}"
unfolding a_r_coset_defs
by simp
lemmas a_l_coset_defs =
a_l_coset_def l_coset_def
lemma a_l_coset_def':
fixes G (structure)
shows "a <+ H \ \h\H. {a \ h}"
unfolding a_l_coset_defs
by simp
lemmas A_RCOSETS_defs =
A_RCOSETS_def RCOSETS_def
lemma A_RCOSETS_def':
fixes G (structure)
shows "a_rcosets H \ \a\carrier G. {H +> a}"
unfolding A_RCOSETS_defs
by (fold a_r_coset_def, simp)
lemmas set_add_defs =
set_add_def set_mult_def
lemma set_add_def':
fixes G (structure)
shows "H <+> K \ \h\H. \k\K. {h \ k}"
unfolding set_add_defs
by simp
lemmas A_SET_INV_defs =
A_SET_INV_def SET_INV_def
lemma A_SET_INV_def':
fixes G (structure)
shows "a_set_inv H \ \h\H. {\ h}"
unfolding A_SET_INV_defs
by (fold a_inv_def)
subsubsection \Cosets\
lemma (in abelian_group) a_coset_add_assoc:
"[| M \ carrier G; g \ carrier G; h \ carrier G |]
==> (M +> g) +> h = M +> (g \ h)"
by (rule group.coset_mult_assoc [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_coset_add_zero [simp]:
"M \ carrier G ==> M +> \ = M"
by (rule group.coset_mult_one [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_coset_add_inv1:
"[| M +> (x \ (\ y)) = M; x \ carrier G ; y \ carrier G;
M \ carrier G |] ==> M +> x = M +> y"
by (rule group.coset_mult_inv1 [OF a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
lemma (in abelian_group) a_coset_add_inv2:
"[| M +> x = M +> y; x \ carrier G; y \ carrier G; M \ carrier G |]
==> M +> (x \ (\ y)) = M"
by (rule group.coset_mult_inv2 [OF a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
lemma (in abelian_group) a_coset_join1:
"[| H +> x = H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> x \ H"
by (rule group.coset_join1 [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_solve_equation:
"\subgroup H \carrier = carrier G, mult = add G, one = zero G\; x \ H; y \ H\ \ \h\H. y = h \ x"
by (rule group.solve_equation [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_repr_independence:
"\y \ H +> x; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ \ \ H +> x = H +> y"
by (rule group.repr_independence [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_coset_join2:
"\x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\; x\H\ \ H +> x = H"
by (rule group.coset_join2 [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_monoid) a_r_coset_subset_G:
"[| H \ carrier G; x \ carrier G |] ==> H +> x \ carrier G"
by (rule monoid.r_coset_subset_G [OF a_monoid,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_rcosI:
"[| h \ H; H \ carrier G; x \ carrier G|] ==> h \ x \ H +> x"
by (rule group.rcosI [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_rcosetsI:
"\H \ carrier G; x \ carrier G\ \ H +> x \ a_rcosets H"
by (rule group.rcosetsI [OF a_group,
folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
text\Really needed?\
lemma (in abelian_group) a_transpose_inv:
"[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |]
==> (\ x) \ z = y"
by (rule group.transpose_inv [OF a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
(*
--"duplicate"
lemma (in abelian_group) a_rcos_self:
"[| x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> x \ H +> x"
by (rule group.rcos_self [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
*)
subsubsection \Subgroups\
locale additive_subgroup =
fixes H and G (structure)
assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"
lemma (in additive_subgroup) is_additive_subgroup:
shows "additive_subgroup H G"
by (rule additive_subgroup_axioms)
lemma additive_subgroupI:
fixes G (structure)
assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"
shows "additive_subgroup H G"
by (rule additive_subgroup.intro) (rule a_subgroup)
lemma (in additive_subgroup) a_subset:
"H \ carrier G"
by (rule subgroup.subset[OF a_subgroup,
simplified monoid_record_simps])
lemma (in additive_subgroup) a_closed [intro, simp]:
"\x \ H; y \ H\ \ x \ y \ H"
by (rule subgroup.m_closed[OF a_subgroup,
simplified monoid_record_simps])
lemma (in additive_subgroup) zero_closed [simp]:
"\ \ H"
by (rule subgroup.one_closed[OF a_subgroup,
simplified monoid_record_simps])
lemma (in additive_subgroup) a_inv_closed [intro,simp]:
"x \ H \ \ x \ H"
by (rule subgroup.m_inv_closed[OF a_subgroup,
folded a_inv_def, simplified monoid_record_simps])
subsubsection \Additive subgroups are normal\
text \Every subgroup of an \abelian_group\ is normal\
locale abelian_subgroup = additive_subgroup + abelian_group G +
assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\"
lemma (in abelian_subgroup) is_abelian_subgroup:
shows "abelian_subgroup H G"
by (rule abelian_subgroup_axioms)
lemma abelian_subgroupI:
assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\"
and a_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \\<^bsub>G\<^esub> y = y \\<^bsub>G\<^esub> x"
shows "abelian_subgroup H G"
proof -
interpret normal "H" "\carrier = carrier G, mult = add G, one = zero G\"
by (rule a_normal)
show "abelian_subgroup H G"
by standard (simp add: a_comm)
qed
lemma abelian_subgroupI2:
fixes G (structure)
assumes a_comm_group: "comm_group \carrier = carrier G, mult = add G, one = zero G\"
and a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"
shows "abelian_subgroup H G"
proof -
interpret comm_group "\carrier = carrier G, mult = add G, one = zero G\"
by (rule a_comm_group)
interpret subgroup "H" "\carrier = carrier G, mult = add G, one = zero G\"
by (rule a_subgroup)
show "abelian_subgroup H G"
apply unfold_locales
proof (simp add: r_coset_def l_coset_def, clarsimp)
fix x
assume xcarr: "x \ carrier G"
from a_subgroup have Hcarr: "H \ carrier G"
unfolding subgroup_def by simp
from xcarr Hcarr show "(\h\H. {h \\<^bsub>G\<^esub> x}) = (\h\H. {x \\<^bsub>G\<^esub> h})"
using m_comm [simplified] by fastforce
qed
qed
lemma abelian_subgroupI3:
fixes G (structure)
assumes asg: "additive_subgroup H G"
and ag: "abelian_group G"
shows "abelian_subgroup H G"
apply (rule abelian_subgroupI2)
apply (rule abelian_group.a_comm_group[OF ag])
apply (rule additive_subgroup.a_subgroup[OF asg])
done
lemma (in abelian_subgroup) a_coset_eq:
"(\x \ carrier G. H +> x = x <+ H)"
by (rule normal.coset_eq[OF a_normal,
folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_subgroup) a_inv_op_closed1:
shows "\x \ carrier G; h \ H\ \ (\ x) \ h \ x \ H"
by (rule normal.inv_op_closed1 [OF a_normal,
folded a_inv_def, simplified monoid_record_simps])
lemma (in abelian_subgroup) a_inv_op_closed2:
shows "\x \ carrier G; h \ H\ \ x \ h \ (\ x) \ H"
by (rule normal.inv_op_closed2 [OF a_normal,
folded a_inv_def, simplified monoid_record_simps])
text\Alternative characterization of normal subgroups\
lemma (in abelian_group) a_normal_inv_iff:
"(N \ \carrier = carrier G, mult = add G, one = zero G\) =
(subgroup N \carrier = carrier G, mult = add G, one = zero G\ \ (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))"
(is "_ = ?rhs")
by (rule group.normal_inv_iff [OF a_group,
folded a_inv_def, simplified monoid_record_simps])
lemma (in abelian_group) a_lcos_m_assoc:
"[| M \ carrier G; g \ carrier G; h \ carrier G |]
==> g <+ (h <+ M) = (g \ h) <+ M"
by (rule group.lcos_m_assoc [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_lcos_mult_one:
"M \ carrier G ==> \ <+ M = M"
by (rule group.lcos_mult_one [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_l_coset_subset_G:
"[| H \ carrier G; x \ carrier G |] ==> x <+ H \ carrier G"
by (rule group.l_coset_subset_G [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_l_coset_swap:
"\y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\\ \ x \ y <+ H"
by (rule group.l_coset_swap [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_l_coset_carrier:
"[| y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> y \