# Theory AbelCoset

theory AbelCoset
imports Coset Ring
(*  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 HOL.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 (add_monoid G)"

definition
a_l_coset    :: "[_, 'a, 'a set] ⇒ 'a set"    (infixl "<+ı" 60)
where "a_l_coset G = l_coset (add_monoid G)"

definition
A_RCOSETS  :: "[_, 'a set] ⇒ ('a set)set"   ("a'_rcosetsı _" [81] 80)
where "A_RCOSETS G H = RCOSETS (add_monoid G) H"

definition
set_add  :: "[_, 'a set ,'a set] ⇒ 'a set" (infixl "<+>ı" 60)

definition
A_SET_INV :: "[_,'a set] ⇒ 'a set"  ("a'_set'_invı _" [81] 80)
where "A_SET_INV G H = SET_INV (add_monoid G) H"

definition
a_r_congruent :: "[('a,'b)ring_scheme, 'a set] ⇒ ('a*'a)set"  ("racongı")
where "a_r_congruent G = r_congruent (add_monoid 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 (add_monoid 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 (add_monoid G) (add_monoid H) h"

locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H
for G (structure) and H (structure) +
fixes 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)

fixes G (structure)
shows "H <+> K ≡ ⋃h∈H. ⋃k∈K. {h ⊕ k}"

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›

sublocale abelian_group <
rewrites "carrier (add_monoid G) =   carrier G"
and "    one (add_monoid G) =      zero G"
and "  m_inv (add_monoid G) =     a_inv G"
and "finprod (add_monoid G) =    finsum G"
and "r_coset (add_monoid G) = a_r_coset G"
and "l_coset (add_monoid G) = a_l_coset G"
and "(λa k. pow (add_monoid G) a k) = (λa k. add_pow G k a)"
by (rule a_group)
(auto simp: m_inv_def a_inv_def finsum_def a_r_coset_def a_l_coset_def add_pow_def)

context abelian_group
begin

(*
*)

end

"[| 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])

"M ⊆ carrier G ==> M +> 𝟬 = M"
by (rule group.coset_mult_one [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])

"[| 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])

"[| 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 (add_monoid 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 (add_monoid 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 (add_monoid G) ⟧ ⟹
H +> x = H +> y"
using a_repr_independence' by (simp add: a_r_coset_def)

lemma (in abelian_group) a_coset_join2:
"⟦x ∈ carrier G;  subgroup H (add_monoid 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"
using r_neg1 by blast

subsubsection ‹Subgroups›

fixes H and G (structure)
assumes a_subgroup: "subgroup H (add_monoid G)"

fixes G (structure)
assumes a_subgroup: "subgroup H (add_monoid G)"

"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])

"𝟬 ∈ H"
by (rule subgroup.one_closed[OF a_subgroup,
simplified monoid_record_simps])

"x ∈ H ⟹ ⊖ x ∈ H"
by (rule subgroup.m_inv_closed[OF a_subgroup,
folded a_inv_def, simplified monoid_record_simps])

text ‹Every subgroup of an ‹abelian_group› is normal›

locale abelian_subgroup = additive_subgroup + abelian_group G +
assumes a_normal: "normal H (add_monoid 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 (add_monoid G)"
and a_comm: "!!x y. [| x ∈ carrier G; y ∈ carrier G |] ==> x ⊕⇘G⇙ y = y ⊕⇘G⇙ x"
shows "abelian_subgroup H G"
proof -
by (rule a_normal)

show "abelian_subgroup H G"
qed

lemma abelian_subgroupI2:
fixes G (structure)
and a_subgroup: "subgroup H (add_monoid G)"
shows "abelian_subgroup H G"
proof -
by (rule a_comm_group)
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 ⊕⇘G⇙ x}) = (⋃h∈H. {x ⊕⇘G⇙ h})"
using m_comm [simplified] by fastforce
qed
qed

lemma abelian_subgroupI3:
fixes G (structure)
and "abelian_group G"
shows "abelian_subgroup H G"
using assms abelian_subgroupI2 abelian_group.a_comm_group additive_subgroup_def by blast

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:
(subgroup N (add_monoid 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 (add_monoid 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 (add_monoid G) |] ==> y ∈ carrier G"
by (rule group.l_coset_carrier [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])

lemma (in abelian_group) a_l_repr_imp_subset:
assumes "y ∈ x <+ H" "x ∈ carrier G" "subgroup H (add_monoid G)"
shows "y <+ H ⊆ x <+ H"
by (metis (full_types) a_l_coset_defs(1) add.l_repr_independence assms set_eq_subset)

lemma (in abelian_group) a_l_repr_independence:
assumes y: "y ∈ x <+ H" and x: "x ∈ carrier G" and sb: "subgroup H (add_monoid G)"
shows "x <+ H = y <+ H"
apply (rule group.l_repr_independence [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
apply (rule y)
apply (rule x)
apply (rule sb)
done

"⟦H ⊆ carrier G; K ⊆ carrier G⟧ ⟹ H <+> K ⊆ carrier G"
by (rule group.setmult_subset_G [OF a_group,

lemma (in abelian_group) subgroup_add_id: "subgroup H (add_monoid G) ⟹ H <+> H = H"
by (rule group.subgroup_mult_id [OF a_group,

lemma (in abelian_subgroup) a_rcos_inv:
assumes x:     "x ∈ carrier G"
shows "a_set_inv (H +> x) = H +> (⊖ x)"
by (rule normal.rcos_inv [OF a_normal,
folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)

lemma (in abelian_group) a_setmult_rcos_assoc:
"⟦H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G⟧
⟹ H <+> (K +> x) = (H <+> K) +> x"
by (rule group.setmult_rcos_assoc [OF a_group,

lemma (in abelian_group) a_rcos_assoc_lcos:
"⟦H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G⟧
⟹ (H +> x) <+> K = H <+> (x <+ K)"
by (rule group.rcos_assoc_lcos [OF a_group,
folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_rcos_sum:
"⟦x ∈ carrier G; y ∈ carrier G⟧
⟹ (H +> x) <+> (H +> y) = H +> (x ⊕ y)"
by (rule normal.rcos_sum [OF a_normal,

"M ∈ a_rcosets H ⟹ H <+> M = M"
― ‹generalizes ‹subgroup_mult_id››
by (rule normal.rcosets_mult_eq [OF a_normal,

subsubsection ‹Congruence Relation›

lemma (in abelian_subgroup) a_equiv_rcong:
shows "equiv (carrier G) (racong H)"
by (rule subgroup.equiv_rcong [OF a_subgroup a_group,
folded a_r_congruent_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_l_coset_eq_rcong:
assumes a: "a ∈ carrier G"
shows "a <+ H = racong H  {a}"
by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)

lemma (in abelian_subgroup) a_rcos_equation:
shows
"⟦ha ⊕ a = h ⊕ b; a ∈ carrier G;  b ∈ carrier G;
h ∈ H;  ha ∈ H;  hb ∈ H⟧
⟹ hb ⊕ a ∈ (⋃h∈H. {h ⊕ b})"
by (rule group.rcos_equation [OF a_group a_subgroup,
folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_rcos_disjoint:
shows "⟦a ∈ a_rcosets H; b ∈ a_rcosets H; a≠b⟧ ⟹ a ∩ b = {}"
by (rule group.rcos_disjoint [OF a_group a_subgroup,
folded A_RCOSETS_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_rcos_self:
shows "x ∈ carrier G ⟹ x ∈ H +> x"
by (rule group.rcos_self [OF a_group _ a_subgroup,
folded a_r_coset_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_rcosets_part_G:
shows "⋃(a_rcosets H) = carrier G"
by (rule group.rcosets_part_G [OF a_group a_subgroup,
folded A_RCOSETS_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_cosets_finite:
"⟦c ∈ a_rcosets H;  H ⊆ carrier G;  finite (carrier G)⟧ ⟹ finite c"
by (rule group.cosets_finite [OF a_group,
folded A_RCOSETS_def, simplified monoid_record_simps])

lemma (in abelian_group) a_card_cosets_equal:
"⟦c ∈ a_rcosets H;  H ⊆ carrier G; finite(carrier G)⟧
⟹ card c = card H"

lemma (in abelian_group) rcosets_subset_PowG:
"additive_subgroup H G  ⟹ a_rcosets H ⊆ Pow(carrier G)"
by (rule group.rcosets_subset_PowG [OF a_group,
folded A_RCOSETS_def, simplified monoid_record_simps],

theorem (in abelian_group) a_lagrange:
⟹ card(a_rcosets H) * card(H) = order(G)"
by (rule group.lagrange [OF a_group,
folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])

subsubsection ‹Factorization›

lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def

lemma A_FactGroup_def':
fixes G (structure)
shows "G A_Mod H ≡ ⦇carrier = a_rcosets⇘G⇙ H, mult = set_add G, one = H⦈"
unfolding A_FactGroup_defs

lemma (in abelian_subgroup) a_setmult_closed:
"⟦K1 ∈ a_rcosets H; K2 ∈ a_rcosets H⟧ ⟹ K1 <+> K2 ∈ a_rcosets H"
by (rule normal.setmult_closed [OF a_normal,

lemma (in abelian_subgroup) a_setinv_closed:
"K ∈ a_rcosets H ⟹ a_set_inv K ∈ a_rcosets H"
by (rule normal.setinv_closed [OF a_normal,
folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_rcosets_assoc:
"⟦M1 ∈ a_rcosets H; M2 ∈ a_rcosets H; M3 ∈ a_rcosets H⟧
⟹ M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)"
by (rule normal.rcosets_assoc [OF a_normal,

lemma (in abelian_subgroup) a_subgroup_in_rcosets:
"H ∈ a_rcosets H"
by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group,
folded A_RCOSETS_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq:
"M ∈ a_rcosets H ⟹ a_set_inv M <+> M = H"
by (rule normal.rcosets_inv_mult_group_eq [OF a_normal,
folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps])

theorem (in abelian_subgroup) a_factorgroup_is_group:
"group (G A_Mod H)"
by (rule normal.factorgroup_is_group [OF a_normal,
folded A_FactGroup_def, simplified monoid_record_simps])

text ‹Since the Factorization is based on an \emph{abelian} subgroup, is results in
a commutative group›
theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
"comm_group (G A_Mod H)"
apply (intro comm_group.intro comm_monoid.intro) prefer 3
apply (rule a_factorgroup_is_group)
apply (rule group.axioms[OF a_factorgroup_is_group])
apply (rule comm_monoid_axioms.intro)
apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
done

lemma add_A_FactGroup [simp]: "X ⊗⇘(G A_Mod H)⇙ X' = X <+>⇘G⇙ X'"

lemma (in abelian_subgroup) a_inv_FactGroup:
"X ∈ carrier (G A_Mod H) ⟹ inv⇘G A_Mod H⇙ X = a_set_inv X"
by (rule normal.inv_FactGroup [OF a_normal,
folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])

text‹The coset map is a homomorphism from @{term G} to the quotient group
@{term "G Mod H"}›
lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
"(λa. H +> a) ∈ hom (add_monoid G) (G A_Mod H)"
by (rule normal.r_coset_hom_Mod [OF a_normal,
folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])

text ‹The isomorphism theorems have been omitted from lifting, at
least for now›

subsubsection‹The First Isomorphism Theorem›

text‹The quotient by the kernel of a homomorphism is isomorphic to the
range of that homomorphism.›

lemmas a_kernel_defs =
a_kernel_def kernel_def

lemma a_kernel_def':
"a_kernel R S h = {x ∈ carrier R. h x = 𝟬⇘S⇙}"
by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])

subsubsection ‹Homomorphisms›

lemma abelian_group_homI:
assumes "abelian_group G"
assumes "abelian_group H"
shows "abelian_group_hom G H h"
proof -
interpret G: abelian_group G by fact
interpret H: abelian_group H by fact
show ?thesis
apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
apply fact
apply fact
apply (rule a_group_hom)
done
qed

lemma (in abelian_group_hom) is_abelian_group_hom:
"abelian_group_hom G H h"
..

"[| x ∈ carrier G; y ∈ carrier G |]
==> h (x ⊕⇘G⇙ y) = h x ⊕⇘H⇙ h y"
by (rule group_hom.hom_mult[OF a_group_hom,
simplified ring_record_simps])

lemma (in abelian_group_hom) hom_closed [simp]:
"x ∈ carrier G ⟹ h x ∈ carrier H"
by (rule group_hom.hom_closed[OF a_group_hom,
simplified ring_record_simps])

lemma (in abelian_group_hom) zero_closed [simp]:
"h 𝟬 ∈ carrier H"
by (rule group_hom.one_closed[OF a_group_hom,
simplified ring_record_simps])

lemma (in abelian_group_hom) hom_zero [simp]:
"h 𝟬 = 𝟬⇘H⇙"
by (rule group_hom.hom_one[OF a_group_hom,
simplified ring_record_simps])

lemma (in abelian_group_hom) a_inv_closed [simp]:
"x ∈ carrier G ==> h (⊖x) ∈ carrier H"
by (rule group_hom.inv_closed[OF a_group_hom,
folded a_inv_def, simplified ring_record_simps])

lemma (in abelian_group_hom) hom_a_inv [simp]:
"x ∈ carrier G ==> h (⊖x) = ⊖⇘H⇙ (h x)"
by (rule group_hom.hom_inv[OF a_group_hom,
folded a_inv_def, simplified ring_record_simps])

"additive_subgroup (a_kernel G H h) G"
apply (rule group_hom.subgroup_kernel[OF a_group_hom,
folded a_kernel_def, simplified ring_record_simps])
done

text‹The kernel of a homomorphism is an abelian subgroup›
lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
"abelian_subgroup (a_kernel G H h) G"
apply (rule abelian_subgroupI)
apply (rule group_hom.normal_kernel[OF a_group_hom,
folded a_kernel_def, simplified ring_record_simps])
done

lemma (in abelian_group_hom) A_FactGroup_nonempty:
assumes X: "X ∈ carrier (G A_Mod a_kernel G H h)"
shows "X ≠ {}"
by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)

lemma (in abelian_group_hom) FactGroup_the_elem_mem:
assumes X: "X ∈ carrier (G A_Mod (a_kernel G H h))"
shows "the_elem (hX) ∈ carrier H"
by (rule group_hom.FactGroup_the_elem_mem[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)

lemma (in abelian_group_hom) A_FactGroup_hom:
"(λX. the_elem (hX)) ∈ hom (G A_Mod (a_kernel G H h))
by (rule group_hom.FactGroup_hom[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])

lemma (in abelian_group_hom) A_FactGroup_inj_on:
"inj_on (λX. the_elem (h  X)) (carrier (G A_Mod a_kernel G H h))"
by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])

text‹If the homomorphism @{term h} is onto @{term H}, then so is the
homomorphism from the quotient group›
lemma (in abelian_group_hom) A_FactGroup_onto:
assumes h: "h  carrier G = carrier H"
shows "(λX. the_elem (h  X))  carrier (G A_Mod a_kernel G H h) = carrier H"
by (rule group_hom.FactGroup_onto[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)

text‹If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.›
theorem (in abelian_group_hom) A_FactGroup_iso_set:
"h  carrier G = carrier H
⟹ (λX. the_elem (hX)) ∈ iso (G A_Mod (a_kernel G H h)) (add_monoid H)"
by (rule group_hom.FactGroup_iso_set[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])

corollary (in abelian_group_hom) A_FactGroup_iso :
"h  carrier G = carrier H
⟹  (G A_Mod (a_kernel G H h)) ≅  (add_monoid H)"
using A_FactGroup_iso_set unfolding is_iso_def by auto

subsubsection ‹Cosets›

text ‹Not eveything from \texttt{CosetExt.thy} is lifted here.›

assumes hH: "h ∈ H"
shows "h ∈ carrier G"
by (rule subgroup.mem_carrier [OF a_subgroup,
simplified monoid_record_simps]) (rule hH)

lemma (in abelian_subgroup) a_elemrcos_carrier:
assumes acarr: "a ∈ carrier G"
and a': "a' ∈ H +> a"
shows "a' ∈ carrier G"
by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')

lemma (in abelian_subgroup) a_rcos_const:
assumes hH: "h ∈ H"
shows "H +> h = H"
by (rule subgroup.rcos_const [OF a_subgroup a_group,
folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)

lemma (in abelian_subgroup) a_rcos_module_imp:
assumes xcarr: "x ∈ carrier G"
and x'cos: "x' ∈ H +> x"
shows "(x' ⊕ ⊖x) ∈ H"
by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)

lemma (in abelian_subgroup) a_rcos_module_rev:
assumes "x ∈ carrier G" "x' ∈ carrier G"
and "(x' ⊕ ⊖x) ∈ H"
shows "x' ∈ H +> x"
using assms
by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])

lemma (in abelian_subgroup) a_rcos_module:
assumes "x ∈ carrier G" "x' ∈ carrier G"
shows "(x' ∈ H +> x) = (x' ⊕ ⊖x ∈ H)"
using assms
by (rule subgroup.rcos_module [OF a_subgroup a_group,
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])

― ‹variant›
lemma (in abelian_subgroup) a_rcos_module_minus:
assumes "ring G"
assumes carr: "x ∈ carrier G" "x' ∈ carrier G"
shows "(x' ∈ H +> x) = (x' ⊖ x ∈ H)"
proof -
interpret G: ring G by fact
from carr
have "(x' ∈ H +> x) = (x' ⊕ ⊖x ∈ H)" by (rule a_rcos_module)
with carr
show "(x' ∈ H +> x) = (x' ⊖ x ∈ H)"
qed

lemma (in abelian_subgroup) a_repr_independence':
assumes y: "y ∈ H +> x"
and xcarr: "x ∈ carrier G"
shows "H +> x = H +> y"
apply (rule a_repr_independence)
apply (rule y)
apply (rule xcarr)
apply (rule a_subgroup)
done

lemma (in abelian_subgroup) a_repr_independenceD:
assumes ycarr: "y ∈ carrier G"
and repr:  "H +> x = H +> y"
shows "y ∈ H +> x"
by (rule group.repr_independenceD [OF a_group a_subgroup,
folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)

lemma (in abelian_subgroup) a_rcosets_carrier:
"X ∈ a_rcosets H ⟹ X ⊆ carrier G"
by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
folded A_RCOSETS_def, simplified monoid_record_simps])

assumes Acarr: "A ⊆ carrier G"
and Bcarr: "B ⊆ carrier G"
shows "A <+> B ⊆ carrier G"
by (rule monoid.set_mult_closed [OF a_monoid,
folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)

`