(* ------------------------------------------------------------------------- *)
(* Cyclic Group *)
(* ------------------------------------------------------------------------- *)
(*===========================================================================*)
(* add all dependent libraries for script *)
open HolKernel boolLib bossLib Parse;
(* declare new theory at start *)
val _ = new_theory "groupCyclic";
(* ------------------------------------------------------------------------- *)
(* val _ = load "jcLib"; *)
open jcLib;
(* Get dependent theories local *)
(* (* val _ = load "monoidTheory"; *) *)
(* (* val _ = load "groupTheory"; *) *)
(* (* val _ = load "subgroupTheory"; *) *)
(* val _ = load "groupOrderTheory"; *)
open monoidTheory monoidOrderTheory;
open groupTheory subgroupTheory groupOrderTheory;
open groupMapTheory;
(* val _ = load "groupInstancesTheory"; *)
open groupInstancesTheory;
(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
open helperNumTheory helperSetTheory;
(* val _ = load "helperFunctionTheory"; *)
open helperFunctionTheory;
(* val _ = load "GaussTheory"; *)
open GaussTheory;
open EulerTheory;
(* open dependent theories *)
open pred_setTheory listTheory arithmeticTheory;
(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open dividesTheory gcdTheory;
(* ------------------------------------------------------------------------- *)
(* Cyclic Group Documentation *)
(* ------------------------------------------------------------------------- *)
(* Overloads:
*)
(* Definitions and Theorems (# are exported):
Helper Theroems:
Cyclic Group has a generator:
cyclic_def |- !g. cyclic g <=> Group g /\ ?z. z IN G /\ !x. x IN G ==> ?n. x = z ** n
cyclic_gen_def |- !g. cyclic g ==> cyclic_gen g IN G /\
!x. x IN G ==> ?n. x = cyclic_gen g ** n
# cyclic_group |- !g. cyclic g ==> Group g
cyclic_element |- !g. cyclic g ==> !x. x IN G ==> ?n. x = cyclic_gen g ** n
cyclic_gen_element |- !g. cyclic g ==> cyclic_gen g IN G
cyclic_generated_group |- !g. FiniteGroup g ==> !x. x IN G ==> cyclic (gen x)
cyclic_gen_order |- !g. cyclic g /\ FINITE G ==> (ord (cyclic_gen g) = CARD G)
cyclic_gen_power_order |- !g. cyclic g /\ FINITE G ==> !n. 0 < n /\ (CARD G MOD n = 0) ==>
(ord (cyclic_gen g ** (CARD G DIV n)) = n)
cyclic_generated_by_gen |- !g. cyclic g /\ FINITE G ==> (g = gen (cyclic_gen g))
cyclic_element_by_gen |- !g. cyclic g /\ FINITE G ==>
!x. x IN G ==> ?n. n < CARD G /\ (x = cyclic_gen g ** n)
cyclic_element_in_generated |- !g. cyclic g /\ FINITE G ==>
!x. x IN G ==> x IN (Gen (cyclic_gen g ** (CARD G DIV ord x)))
cyclic_finite_has_order_divisor |- !g. cyclic g /\ FINITE G ==>
!n. n divides CARD G ==> ?x. x IN G /\ (ord x = n)
Cyclic Group Properties:
cyclic_finite_alt |- !g. FiniteGroup g ==> (cyclic g <=> ?z. z IN G /\ (ord z = CARD G))
cyclic_group_comm |- !g. cyclic g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x)
cyclic_group_abelian |- !g. cyclic g ==> AbelianGroup g
Cyclic Subgroups:
cyclic_subgroup_cyclic |- !g h. cyclic g /\ h <= g ==> cyclic h
cyclic_subgroup_condition |- !g. cyclic g /\ FINITE G ==>
!n. (?h. h <= g /\ (CARD H = n)) <=> n divides CARD G
Cyclic Group Examples:
cyclic_uroots_has_primitive |- !g. FINITE G /\ cyclic g ==>
!n. ?z. z IN (uroots n).carrier /\ (ord z = CARD (uroots n).carrier)
cyclic_uroots_cyclic |- !g. cyclic g ==> !n. cyclic (uroots n)
add_mod_order_1 |- !n. 1 < n ==> (order (add_mod n) 1 = n)
add_mod_cylic |- !n. 0 < n ==> cyclic (add_mod n)
Cyclic Generators:
cyclic_generators_def |- !g. cyclic_generators g = {z | z IN G /\ (ord z = CARD G)}
cyclic_generators_element |- !g z. z IN cyclic_generators g <=> z IN G /\ (ord z = CARD G)
cyclic_generators_subset |- !g. cyclic_generators g SUBSET G
cyclic_generators_finite |- !g. FINITE G ==> FINITE (cyclic_generators g)
cyclic_generators_nonempty |- !g. cyclic g /\ FINITE G ==> cyclic_generators g <> {}
cyclic_generators_coprimes_bij |- !g. cyclic g /\ FINITE G ==>
BIJ (\j. cyclic_gen g ** j) (coprimes (CARD G)) (cyclic_generators g)
cyclic_generators_card |- !g. cyclic g /\ FINITE G ==> (CARD (cyclic_generators g) = phi (CARD G))
cyclic_generators_gen_cofactor_eq_orders |- !g. cyclic g /\ FINITE G ==> !n. n divides CARD G ==>
(cyclic_generators (Generated g (cyclic_gen g ** (CARD G DIV n))) = orders g n)
cyclic_orders_card |- !g. cyclic g /\ FINITE G ==>
!n. CARD (orders g n) = if n divides CARD G then phi n else 0
Partition by order equality:
eq_order_def |- !g x y. eq_order g x y <=> (ord x = ord y)
eq_order_equiv |- !g. eq_order g equiv_on G
cyclic_orders_nonempty |- !g. cyclic g /\ FINITE G ==> !n. n divides CARD G ==> orders g n <> {}
cyclic_eq_order_partition |- !g. cyclic g /\ FINITE G ==>
(partition (eq_order g) G = {orders g n | n | n divides CARD G})
cyclic_eq_order_partition_alt |- !g. cyclic g /\ FINITE G ==>
(partition (eq_order g) G = {orders g n | n | n IN divisors (CARD G)})
cyclic_eq_order_partition_by_card |- !g. cyclic g /\ FINITE G ==>
(IMAGE CARD (partition (eq_order g) G) = IMAGE phi (divisors (CARD G)))
eq_order_is_feq_order |- !g. eq_order g = feq ord
orders_is_feq_class_order |- !g. orders g = feq_class ord G
cyclic_image_ord_is_divisors |- !g. cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G))
cyclic_orders_partition |- !g. cyclic g /\ FINITE G ==>
(partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G)))
Finite Cyclic Group Existence:
finite_cyclic_group_existence |- !n. 0 < n ==> ?g. cyclic g /\ (CARD g.carrier = n)
Cyclic Group index relative to a generator:
cyclic_index_exists |- !g x. cyclic g /\ x IN G ==>
?n. (x = cyclic_gen g ** n) /\ (FINITE G ==> n < CARD G)
cyclic_index_def |- !g x. cyclic g /\ x IN G ==>
(x = cyclic_gen g ** cyclic_index g x) /\
(FINITE G ==> cyclic_index g x < CARD G)
finite_cyclic_index_property |- !g. cyclic g /\ FINITE G ==>
!n. n < CARD G ==> (cyclic_index g (cyclic_gen g ** n) = n)
finite_cyclic_index_unique |- !g x. cyclic g /\ FINITE G /\ x IN G ==>
!n. n < CARD G ==> ((x = cyclic_gen g ** n) <=> (n = cyclic_index g x))
finite_cyclic_index_add |- !g x y. cyclic g /\ FINITE G /\ x IN G /\ y IN G ==>
(cyclic_index g (x * y) =
(cyclic_index g x + cyclic_index g y) MOD CARD G)
Finite Cyclic Group Uniqueness:
finite_cyclic_group_homo |- !g1 g2. cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2
finite_cyclic_group_bij |- !g1 g2. cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier
finite_cyclic_group_iso |- !g1 g2. cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
GroupIso (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2
finite_cyclic_group_uniqueness |- !g1 g2. cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
?f. GroupIso f g1 g2
finite_cyclic_group_add_mod_homo |- !g. cyclic g /\ FINITE G ==>
GroupHomo (\n. cyclic_gen g ** n) (add_mod (CARD G)) g
finite_cyclic_group_add_mod_bij |- !g. cyclic g /\ FINITE G ==>
BIJ (\n. cyclic_gen g ** n) (add_mod (CARD G)).carrier G
finite_cyclic_group_add_mod_iso |- !g. cyclic g /\ FINITE G ==>
GroupIso (\n. cyclic_gen g ** n) (add_mod (CARD G)) g
Isomorphism between Cyclic Groups:
cyclic_iso_gen |- !g h f. cyclic g /\ cyclic h /\ FINITE G /\ GroupIso f g h ==>
f (cyclic_gen g) IN cyclic_generators h
*)
(* ------------------------------------------------------------------------- *)
(* Cyclic Group has a generator. *)
(* ------------------------------------------------------------------------- *)
(* Define Cyclic Group *)
val cyclic_def = Define`
cyclic (g:'a group) <=> Group g /\ ?z. z IN G /\ (!x. x IN G ==> ?n. x = z ** n)
`;
(* Apply Skolemization *)
val lemma = prove(
``!(g:'a group). ?z. cyclic g ==> z IN G /\ !x. x IN G ==> ?n. x = z ** n``,
metis_tac[cyclic_def]);
(*
- SKOLEM_THM;
> val it = |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) : thm
*)
(* Define cyclic generator *)
(*
- SIMP_RULE bool_ss [SKOLEM_THM] lemma;
> val it = |- ?f. !g. cyclic g ==> f g IN G /\ !x. x IN G ==> ?n. x = f g ** n: thm
*)
val cyclic_gen_def = new_specification(
"cyclic_gen_def",
["cyclic_gen"],
SIMP_RULE bool_ss [SKOLEM_THM] lemma);
(*
> val cyclic_gen_def = |-
!g. cyclic g ==> cyclic_gen g IN G /\ !x. x IN G ==> ?n. x = cyclic_gen g ** n: thm
*)
(* Theorem: cyclic g ==> Group g *)
(* Proof: by cyclic_def *)
val cyclic_group = store_thm(
"cyclic_group",
``!g:'a group. cyclic g ==> Group g``,
rw[cyclic_def]);
(* export simple result *)
val _ = export_rewrites ["cyclic_group"];
(* Theorem: cyclic g ==> !x. x IN G ==> ?n. x = (cyclic_gen g) ** n *)
(* Proof: by cyclic_gen_def. *)
val cyclic_element = store_thm(
"cyclic_element",
``!g:'a group. cyclic g ==> (!x. x IN G ==> ?n. x = (cyclic_gen g) ** n)``,
rw[cyclic_gen_def]);
(* Theorem cyclic g ==> (cyclic_gen g) IN G *)
(* Proof: by cyclic_gen_def. *)
val cyclic_gen_element = store_thm(
"cyclic_gen_element",
``!g:'a group. cyclic g ==> (cyclic_gen g) IN G``,
rw[cyclic_gen_def]);
(* Theorem: FiniteGroup g ==> !x. x IN G ==> cyclic (gen x) *)
(* Proof:
By cyclic_def, this is to show:
(1) x IN G ==> Group (gen x)
True by generated_group.
(2) ?z. z IN (Gen x) /\ !x'. x' IN (Gen x) ==> ?n. x' = (gen x).exp z n
x IN (Gen x) by generated_gen_element
Let z = x, the assertion is true by generated_element
*)
val cyclic_generated_group = store_thm(
"cyclic_generated_group",
``!g:'a group. FiniteGroup g ==> !x. x IN G ==> cyclic (gen x)``,
rpt strip_tac >>
`Group g /\ FINITE G` by metis_tac[FiniteGroup_def] >>
rw[cyclic_def] >-
rw[generated_group] >>
`x IN (Gen x)` by rw[generated_gen_element] >>
metis_tac[generated_subgroup, generated_element, subgroup_exp, subgroup_element]);
(* Theorem: cyclic g /\ FINITE G ==> ord (cyclic_gen g) = CARD G *)
(* Proof:
Let z = cyclic_gen g.
!x. x IN G ==> ?n. x = z ** n by cyclic_element
==> x IN (Gen z) by generated_element
Hence G SUBSET (Gen z) by SUBSET_DEF
But (gen z) <= g by generated_subgroup
So (Gen z) SUBSET G by Subgroup_def
Hence (Gen z) = G by SUBSET_ANTISYM
or ord z = CARD (Gen z) by generated_group_card, group_order_pos
= CARD G by above
*)
val cyclic_gen_order = store_thm(
"cyclic_gen_order",
``!g:'a group. cyclic g /\ FINITE G ==> (ord (cyclic_gen g) = CARD G)``,
rpt strip_tac >>
`Group g /\ cyclic_gen g IN G /\ !x. x IN G ==> ?n. x = cyclic_gen g ** n` by rw[cyclic_gen_def] >>
`FiniteGroup g` by rw[FiniteGroup_def] >>
`G SUBSET (Gen (cyclic_gen g))` by rw[generated_element, SUBSET_DEF] >>
`(Gen (cyclic_gen g)) SUBSET G` by metis_tac[generated_subgroup, Subgroup_def] >>
metis_tac[generated_group_card, group_order_pos, SUBSET_ANTISYM]);
(* Theorem: cyclic g /\ FINITE G ==>
!n. 0 < n /\ ((CARD G) MOD n = 0) ==> (ord (cyclic_gen g ** (CARD G DIV n)) = n) *)
(* Proof:
First, Group g by cyclic_group
Therefore FiniteGroup g by FiniteGroup_def
Let t = (cyclic_gen g) ** m, where m = (CARD G) DIV n.
Since (cyclic_gen g) IN G by cyclic_gen_element
so t IN G by group_exp_element
Since ord (cyclic_gen g) = CARD G by cyclic_gen_order
so ord t * gcd (CARD G) m = CARD G by group_order_power
But CARD G
= m * n + ((CARD G) MOD n) by DIVISION
= m * n since (CARD G) MOD n = 0
= n * m by MULT_COMM
so gcd (CARD G) m = m by GCD_MULTIPLE_ALT
But CARD G <> 0 by group_carrier_nonempty, CARD_EQ_0
so m = (CARD G) DIV n <> 0 by GCD_EQ_0
Therefore ord t * m = n * m
or ord t = n by MULT_RIGHT_CANCEL
*)
val cyclic_gen_power_order = store_thm(
"cyclic_gen_power_order",
``!g:'a group. cyclic g /\ FINITE G ==>
!n. 0 < n /\ ((CARD G) MOD n = 0) ==> (ord (cyclic_gen g ** (CARD G DIV n)) = n)``,
rpt strip_tac >>
`Group g` by rw[] >>
`FiniteGroup g` by rw[FiniteGroup_def] >>
qabbrev_tac `m = (CARD G) DIV n` >>
qabbrev_tac `t = (cyclic_gen g) ** m` >>
`(cyclic_gen g) IN G` by rw[cyclic_gen_element] >>
`t IN G` by rw[Abbr`t`] >>
`ord (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >>
`ord t * gcd (CARD G) m = CARD G` by metis_tac[group_order_power] >>
`CARD G = m * n + ((CARD G) MOD n)` by rw[DIVISION, Abbr`m`] >>
`_ = n * m` by rw[MULT_COMM] >>
`gcd (CARD G) m = m` by metis_tac[GCD_MULTIPLE_ALT] >>
`m <> 0` by metis_tac[group_carrier_nonempty, CARD_EQ_0, GCD_EQ_0] >>
metis_tac[MULT_RIGHT_CANCEL]);
(* Theorem: cyclic g ==> (g = (gen (cyclic_gen g))) *)
(* Proof:
Since cyclic g ==> Group g by cyclic_group
Let z = cyclic_gen g.
Then z IN G by cyclic_gen_element
and (Gen z) SUBSET G by generated_subset
Now, show: G SUBSET (Gen z)
or show: x IN G ==> x IN (Gen z) by SUBSET_DEF
Since cyclic g and x IN G,
?j. x = z ** j by cyclic_gen_def
hence x IN x IN (Gen z) by generated_element
Thus (Gen z) SUBSET G
and G SUBSET (Gen z)
==> G = Gen z by SUBSET_ANTISYM
also (gen z).op = $*
and (gen z).id = #e by generated_property
Therefore g = (gen z) by monoid_component_equality
*)
val xcyclic_generated_by_gen = store_thm(
"xcyclic_generated_by_gen",
``!g:'a group. cyclic g ==> (g = (gen (cyclic_gen g)))``,
rpt strip_tac >>
`Group g` by rw[] >>
qabbrev_tac `z = cyclic_gen g` >>
`z IN G` by rw[cyclic_gen_element, Abbr`z`] >>
`(Gen z) SUBSET G` by rw[generated_subset] >>
`G SUBSET (Gen z)` by metis_tac[SUBSET_DEF, cyclic_gen_def, generated_element] >>
`G = Gen z` by rw[SUBSET_ANTISYM] >>
metis_tac[monoid_component_equality, generated_property]);
(* Theorem: cyclic g /\ FINITE G ==> !x. x IN G ==>
?n. n < CARD G /\ (x = (cyclic_gen g) ** n) *)
(* Proof:
Since cyclic g ==> Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and 0 < m by finite_group_card_pos
also ord z = m by cyclic_gen_order
Now ?k. x = z ** k by cyclic_element
Since k MOD m < m by MOD_LESS
and z ** k = z (k MOD m) by group_exp_mod, 0 < m
Just take n = k MOD m.
*)
val cyclic_element_by_gen = store_thm(
"cyclic_element_by_gen",
``!g:'a group. cyclic g /\ FINITE G ==> !x. x IN G ==>
?n. n < CARD G /\ (x = (cyclic_gen g) ** n)``,
rpt strip_tac >>
`Group g` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `z = cyclic_gen g` >>
qabbrev_tac `m = CARD G` >>
`z IN G` by rw[cyclic_gen_element, Abbr`z`] >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
`ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >>
`?k. x = z ** k` by rw[cyclic_element, Abbr`z`] >>
qexists_tac `k MOD m` >>
metis_tac[group_exp_mod, MOD_LESS]);
(* Theorem: cyclic g /\ FINITE G ==> !x. x IN G ==>
x IN (Gen ((cyclic_gen g) ** ((CARD G) DIV (ord x)))) *)
(* Proof:
Since cyclic g ==> Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def, FINITE G
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
and 0 < m by finite_group_card_pos
Let n = ord x, k = m DIV n, y = z ** k.
To show: x IN (Gen y)
Note n divides m by group_order_divides
Since x IN G,
?t. x = z ** t by cyclic_element
But x ** n = #e by order_property
or (z ** t) ** n = #e by x = z ** t
or z ** (t * n) = #e by group_exp_mult
Thus m divides (t * n) by group_order_divides_exp, m = ord z
so k divides t by dividend_divides_divisor_multiple, n divides m
Hence ?s. t = s * k by divides_def
and x = z ** t
= z ** (s * k) by t = s * k
= z ** (k * s) by MULT_COMM
= (z ** k) ** s by group_exp_mult
= y ** s by y = z ** k
Therefore x IN (Gen y) by generated_element
*)
val cyclic_element_in_generated = store_thm(
"cyclic_element_in_generated",
``!g:'a group. cyclic g /\ FINITE G ==> !x. x IN G ==>
x IN (Gen ((cyclic_gen g) ** ((CARD G) DIV (ord x))))``,
rpt strip_tac >>
`Group g ` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `m = CARD G` >>
qabbrev_tac `z = cyclic_gen g` >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
`z IN G /\ (ord z = m)` by rw[GSYM cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >>
qabbrev_tac `n = ord x` >>
qabbrev_tac `k = m DIV n` >>
qabbrev_tac `y = z ** k` >>
`n divides m` by rw[group_order_divides, Abbr`n`, Abbr`m`] >>
`?t. x = z ** t` by rw[cyclic_element, Abbr`z`] >>
`x ** n = #e` by rw[order_property, Abbr`n`] >>
`z ** (t * n) = #e` by rw[group_exp_mult] >>
`m divides (t * n)` by rw[GSYM group_order_divides_exp] >>
`k divides t` by rw[GSYM dividend_divides_divisor_multiple, Abbr`k`] >>
`?s. t = s * k` by rw[GSYM divides_def] >>
`x = y ** s` by metis_tac[group_exp_mult, MULT_COMM] >>
metis_tac[generated_element]);
(* Theorem: cyclic g /\ FINITE G ==> !n. n divides CARD G ==> ?x. x IN G /\ (ord x = n) *)
(* Proof:
Note cyclic g ==> Group g by cyclic_group
and Group g /\ FINITE G ==> FiniteGroup g by FiniteGroup_def
Let z = cyclic_gen g, m = CARD G.
Note 0 < m by finite_group_card_pos
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
Let x = z ** (m DIV n),
Then x IN G by group_exp_element
and ord x = n by group_order_exp_cofactor, 0 < m
*)
val cyclic_finite_has_order_divisor = store_thm(
"cyclic_finite_has_order_divisor",
``!g:'a group. cyclic g /\ FINITE G ==> !n. n divides CARD G ==> ?x. x IN G /\ (ord x = n)``,
rpt strip_tac >>
`Group g` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `z = cyclic_gen g` >>
qabbrev_tac `m = CARD G` >>
`z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
qabbrev_tac `x = z ** (m DIV n)` >>
metis_tac[group_order_exp_cofactor, group_exp_element]);
(* ------------------------------------------------------------------------- *)
(* Cyclic Group Properties *)
(* ------------------------------------------------------------------------- *)
(* Theorem: FiniteGroup g ==> cyclic g <=> ?z. z IN G /\ (ord z = CARD G) *)
(* Proof:
If part: cyclic g ==> ?z. z IN G /\ (ord z = CARD G)
Let z = cyclic_gen g.
cyclic g ==> z IN G by cyclic_gen_element
cyclic g /\ FINITE G ==> (ord z = CARD G) by cyclic_gen_order
Only-if part: ?z. z IN G /\ (ord z = CARD G) ==> cyclic g
Note 0 < CARD G by finite_group_card_pos
(Gen z) SUBSET G by generated_subset
CARD (Gen z) = ord z by generated_group_card
(Gen z) = G by SUBSET_EQ_CARD
Thus !x. x IN G ==> ?n. x = z ** n by generated_element
*)
val cyclic_finite_alt = store_thm(
"cyclic_finite_alt",
``!g:'a group. FiniteGroup g ==> (cyclic g <=> (?z. z IN G /\ (ord z = CARD G)))``,
rpt strip_tac >>
`Group g /\ FINITE G` by metis_tac[FiniteGroup_def] >>
rw[EQ_IMP_THM] >-
metis_tac[cyclic_gen_element, cyclic_gen_order] >>
rw[cyclic_def] >>
qexists_tac `z` >>
rw[] >>
`(Gen z) SUBSET G` by metis_tac[generated_subset] >>
`CARD (Gen z) = ord z` by rw[generated_group_card, finite_group_card_pos] >>
`Gen z = G` by metis_tac[SUBSET_EQ_CARD, SUBSET_FINITE] >>
metis_tac[generated_element]);
(* Theorem: cyclic g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x) *)
(* Proof:
Let z = cyclic_gen g.
x IN G ==> ?n. x = z ** n by cyclic_element
y IN G ==> ?m. y = z ** m by cyclic_element
x * y
= (z ** n) * (z ** m)
= z ** (n + m) by group_exp_add
= z ** (m + n) by ADD_COMM
= (z ** m) * (z ** n) by group_exp_add
= y * x
*)
val cyclic_group_comm = store_thm(
"cyclic_group_comm",
``!g:'a group. cyclic g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x)``,
metis_tac[cyclic_group, cyclic_gen_def, cyclic_element, group_exp_add, ADD_COMM]);;
(* Theorem: cyclic g ==> AbelianGroup g *)
(* Proof: by cyclic_group_comm, cyclic_group, AbelianGroup_def *)
val cyclic_group_abelian = store_thm(
"cyclic_group_abelian",
``!g:'a group. cyclic g ==> AbelianGroup g``,
rw[cyclic_group_comm, AbelianGroup_def]);
(* ------------------------------------------------------------------------- *)
(* Cyclic Subgroups *)
(* ------------------------------------------------------------------------- *)
(* Theorem: cyclic g /\ h <= g ==> cyclic h *)
(* Proof:
Let z = cyclic_gen g.
h <= g <=> Group h /\ Group g /\ H SUBSET G by Subgroup_def
Hence H <> {} by group_carrier_nonempty
and #e IN H by group_id_element, subgroup_id
If H = {#e},
!x. x IN H ==> x = #e, #e ** 1 = #e by group_exp_1, IN_SING
Hence cyclic h by cyclic_def
If H <> {#e}, there is an x IN H and x <> #e by ONE_ELEMENT_SING
!x. x IN H ==> x IN G by SUBSET_DEF
==> ?n. x = z ** n by cyclic_element
Let m = MIN_SET {n | 0 < n /\ z ** n IN H}
Let s = z ** m, s IN H by group_exp_element
Then for any x IN H, ?n. x = z ** n by above
Now n = q * m + r by DIVISION
x = z ** n
= z ** (q * m + r)
= z ** q * m * z ** r by group_comm_op_exp
= (z ** m) ** q * z ** r by group_exp_mult, MULT_COMM
= s ** q * z ** r
Hence z ** r = |/ (s ** q) * x by group_rsolve
or z ** r IN H by group_op_element, group_exp_element
But 0 <= r < m, and m is minimum.
Hence r = 0, or z ** r = #e by group_exp_0
Therefore for any x IN H, ?q. x = s ** q.
Result follows by cyclic_def.
*)
val cyclic_subgroup_cyclic = store_thm(
"cyclic_subgroup_cyclic",
``!g h:'a group. cyclic g /\ h <= g ==> cyclic h``,
rpt strip_tac >>
`Group g /\ (cyclic_gen g) IN G` by rw[cyclic_gen_def] >>
`Group h /\ (h.op = g.op) /\ !x. x IN H ==> x IN G` by metis_tac[Subgroup_def, SUBSET_DEF] >>
qabbrev_tac `z = cyclic_gen g` >>
`H <> {}` by rw[group_carrier_nonempty] >>
`#e IN H` by metis_tac[subgroup_id, group_id_element] >>
`!x. x IN H ==> ?n. x = z ** n` by rw[cyclic_element, Abbr`z`] >>
`!x. x IN H ==> !n. h.exp x n = x ** n` by rw[subgroup_exp] >>
`!x. x IN H ==> (h.inv x = |/ x)` by rw[subgroup_inv] >>
rw[cyclic_def] >>
Cases_on `H = {#e}` >-
rw[] >>
`?x. x IN H /\ x <> #e` by metis_tac[ONE_ELEMENT_SING] >>
`?n. x = z ** n` by rw[] >>
`n <> 0` by metis_tac[group_exp_0] >>
`0 < n` by decide_tac >>
qabbrev_tac `s = {n | 0 < n /\ z ** n IN H}` >>
`n IN s` by rw[Abbr`s`] >>
`s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >>
`MIN_SET s IN s /\ !n. n IN s ==> MIN_SET s <= n` by metis_tac[MIN_SET_LEM] >>
qabbrev_tac `m = MIN_SET s` >>
`!n. n IN s <=> 0 < n /\ z ** n IN H` by rw[Abbr`s`] >>
`0 < m /\ z ** m IN H` by metis_tac[] >>
qexists_tac `z ** m` >>
rw[] >>
`?n'. x' = z ** n'` by rw[] >>
`?q r. ?r q. (n' = q * m + r) /\ r < m` by rw[DA] >>
`x' = z ** (q * m + r)` by rw[] >>
`_ = z ** (q * m) * z ** r` by rw[group_exp_add] >>
`_ = z ** (m * q) * z ** r` by metis_tac[MULT_COMM] >>
`_ = (z ** m) ** q * z ** r` by metis_tac[group_exp_mult] >>
`(z ** m) ** q IN H` by metis_tac[group_exp_element] >>
Cases_on `r = 0` >-
metis_tac[group_exp_0, group_rid] >>
`0 < r` by decide_tac >>
`|/ ((z ** m) ** q) IN H` by metis_tac[group_inv_element] >>
`z ** r IN H` by metis_tac[group_rsolve, group_exp_element, group_op_element] >>
`m <= r` by metis_tac[] >>
`~(r < m)` by decide_tac);
(* Theorem: cyclic g /\ FINITE G ==> !n. (?h. h <= g /\ (CARD H = n)) <=> (n divides (CARD G)) *)
(* Proof:
If part: h <= g ==> CARD H divides CARD G
True by Lagrange_thm.
Only-if part: n divides CARD G ==> ?h. h <= g /\ (CARD H = n)
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and (ord z = m) by cyclic_gen_order
Since n divides m,
?k. m = k * n by divides_def
Thus k divides m by divides_def, MULT_COMM
and gcd k m = k by divides_iff_gcd_fix
Note Group g by cyclic_group
and FiniteGroup g by FiniteGroup_def, FINITE G.
Let x = z ** k,
Then x IN G by group_exp_element
and n * k
= m by MULT_COMM, m = k * n
= ord (z ** k) * gcd m k by group_order_power
= ord x * gcd k m by GCD_SYM
= ord x * k by above
Since 0 < m, m <> 0 by finite_group_card_pos
so k <> 0 and n <> 0 by MULT_EQ_0
thus ord x = n by EQ_MULT_RCANCEL, k <> 0
Take h = gen x,
then h <= g by generated_subgroup
and CARD (Gen x)
= ord x = n by generated_group_card
*)
val cyclic_subgroup_condition = store_thm(
"cyclic_subgroup_condition",
``!g:'a group. cyclic g /\ FINITE G ==> !n. (?h. h <= g /\ (CARD H = n)) <=> (n divides (CARD G))``,
rw[EQ_IMP_THM] >-
rw[Lagrange_thm] >>
qabbrev_tac `z = cyclic_gen g` >>
qabbrev_tac `m = CARD G` >>
`z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >>
`?k. m = k * n` by rw[GSYM divides_def] >>
`k divides m` by metis_tac[divides_def, MULT_COMM] >>
`gcd k m = k` by rw[GSYM divides_iff_gcd_fix] >>
qabbrev_tac `x = z ** k` >>
`Group g ` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
`ord x * k = n * k` by metis_tac[group_order_power, GCD_SYM, MULT_COMM] >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
`m <> 0` by decide_tac >>
`k <> 0 /\ n <> 0` by metis_tac[MULT_EQ_0] >>
`ord x = n` by metis_tac[EQ_MULT_RCANCEL] >>
`x IN G` by rw[Abbr`x`] >>
qexists_tac `gen x` >>
metis_tac[generated_subgroup, generated_group_card, NOT_ZERO_LT_ZERO]);
(* ------------------------------------------------------------------------- *)
(* Cyclic Group Examples *)
(* ------------------------------------------------------------------------- *)
(* Theorem: FINITE G /\ cyclic g ==>
!n. ?z. z IN (uroots n).carrier /\ (ord z = CARD (uroots n).carrier) *)
(* Proof:
cyclic g
==> AbelianGroup g by cyclic_group_abelian
==> (uroots n) <= g by group_uroots_subgroup
==> cyclic (uroots n) by cyclic_subgroup_cyclic
==> (cyclic_gen (uroots n)) IN (uroots n).carrier
by cyclic_gen_element
==> ord (cyclic_gen (uroots n)) = CARD (uroots n)
by cyclic_gen_order, subgroup_order
*)
val cyclic_uroots_has_primitive = store_thm(
"cyclic_uroots_has_primitive",
``!g:'a group. FINITE G /\ cyclic g ==>
!n. ?z. z IN (uroots n).carrier /\ (ord z = CARD (uroots n).carrier)``,
rpt strip_tac >>
`Group g` by rw[] >>
`AbelianGroup g` by rw[cyclic_group_abelian] >>
`(uroots n) <= g` by rw[group_uroots_subgroup] >>
`cyclic (uroots n)` by metis_tac[cyclic_subgroup_cyclic] >>
`(cyclic_gen (uroots n)) IN (uroots n).carrier` by rw[cyclic_gen_element] >>
metis_tac[cyclic_gen_order, subgroup_order, Subgroup_def, SUBSET_FINITE]);
(* This cyclic_uroots_has_primitive, originally for the next one, is not used. *)
(* Theorem: cyclic g ==> cyclic (uroots n) *)
(* Proof:
Note AbelianGroup g by cyclic_group_abelian
and (uroots n) <= g by group_uroots_subgroup
Thus cyclic (uroots n) by cyclic_subgroup_cyclic
*)
val cyclic_uroots_cyclic = store_thm(
"cyclic_uroots_cyclic",
``!g:'a group. cyclic g ==> !n. cyclic (uroots n)``,
rpt strip_tac >>
`AbelianGroup g` by rw[cyclic_group_abelian] >>
`(uroots n) <= g` by rw[group_uroots_subgroup] >>
metis_tac[cyclic_subgroup_cyclic]);
(* Theorem: 1 < n ==> (order (add_mod n) 1 = n) *)
(* Proof:
Since 1 IN (add_mod n).carrier by add_mod_element, 1 < n
and !m. (add_mod n).exp 1 m = m MOD n by add_mod_exp, 0 < n
Therefore,
(add_mod n).exp 1 n = n MOD n = 0 by DIVMOD_ID, 0 < n
and !m. 0 < m /\ m < n,
(add_mod n).exp 1 m = m <> 0 by NOT_ZERO_LT_ZERO, 0 < n
Now (add_mod n).id = 0 by add_mod_property
so order (add_mod n) 1 = n by group_order_thm
*)
val add_mod_order_1 = store_thm(
"add_mod_order_1",
``!n. 1 < n ==> (order (add_mod n) 1 = n)``,
rpt strip_tac >>
`0 < n` by decide_tac >>
`!m. (add_mod n).exp 1 m = m MOD n` by rw[add_mod_exp] >>
`1 IN (add_mod n).carrier` by rw[add_mod_element] >>
`(add_mod n).exp 1 n = 0` by rw[] >>
`!m. 0 < m /\ m < n ==> (add_mod n).exp 1 m <> 0` by rw[NOT_ZERO_LT_ZERO] >>
metis_tac[group_order_thm, add_mod_property]);
(* Theorem: 0 < n ==> cyclic (add_mod n) *)
(* Proof:
Note Group (add_mod n) by add_mod_group
and FiniteGroup (add_mod n) by add_mod_finite_group
and (add_mod n).id = 0 by add_mod_property
and CARD (add_mod n).carrier = n by add_mod_property
If n = 1,
Since order (add_mod 1) 0 = 1 by group_order_id
and 0 IN (add_mod 1).carrier by group_id_element
and CARD (add_mod 1).carrier = 1 by above
Thus cyclic (add_mod 1) by cyclic_finite_alt
If n <> 1, 1 < n.
Since 1 IN (add_mod n).carrier by add_mod_element, 1 < n
and order (add_mod n) 1 = n by add_mod_order_1, 1 < n
Thus cyclic (add_mod n) by cyclic_finite_alt
*)
val add_mod_cylic = store_thm(
"add_mod_cylic",
``!n. 0 < n ==> cyclic (add_mod n)``,
rpt strip_tac >>
`Group (add_mod n)` by rw[add_mod_group] >>
`FiniteGroup (add_mod n)` by rw[add_mod_finite_group] >>
`((add_mod n).id = 0) /\ (CARD (add_mod n).carrier = n)` by rw[add_mod_property] >>
Cases_on `n = 1` >-
metis_tac[cyclic_finite_alt, group_order_id, group_id_element] >>
`1 < n` by decide_tac >>
metis_tac[cyclic_finite_alt, add_mod_order_1, add_mod_element]);
(* ------------------------------------------------------------------------- *)
(* Order of elements in a Cyclic Group *)
(* ------------------------------------------------------------------------- *)
(*
From FiniteField theory, knowing that F* is cyclic, we can prove stronger results:
(1) Let G be cyclic with |G| = n, so it has a generator z with (order z = n).
(2) All elements in G are known: 1, g, g^2, ...., g^(n-1).
(3) Thus all their orders are known: n/gcd(0,n), n/gcd(1,n), n/gcd(2,n), ..., n/gcd(n-1,n).
(4) Counting, CARD (order_eq k) = phi k.
(5) As a result, n = SUM (phi k), over k | n.
*)
(* ------------------------------------------------------------------------- *)
(* Cyclic Generators *)
(* ------------------------------------------------------------------------- *)
(* Define the set of generators for cyclic group *)
val cyclic_generators_def = Define `
cyclic_generators (g:'a group) = {z | z IN G /\ (ord z = CARD G)}
`;
(* Theorem: z IN cyclic_generators g <=> z IN G /\ (ord z = CARD G) *)
(* Proof: by cyclic_generators_def *)
val cyclic_generators_element = store_thm(
"cyclic_generators_element",
``!g:'a group. !z. z IN cyclic_generators g <=> z IN G /\ (ord z = CARD G)``,
rw[cyclic_generators_def]);
(* Theorem: (cyclic_generators g) SUBSET G *)
(* Proof: by cyclic_generators_def, SUBSET_DEF *)
val cyclic_generators_subset = store_thm(
"cyclic_generators_subset",
``!g:'a group. (cyclic_generators g) SUBSET G``,
rw[cyclic_generators_def, SUBSET_DEF]);
(* Theorem: FINITE G ==> FINITE (cyclic_generators g) *)
(* Proof: by cyclic_generators_subset, SUBSET_FINITE *)
val cyclic_generators_finite = store_thm(
"cyclic_generators_finite",
``!g:'a group. FINITE G ==> FINITE (cyclic_generators g)``,
metis_tac[cyclic_generators_subset, SUBSET_FINITE]);
(* Theorem: cyclic g /\ FINITE G ==> (cyclic_generators g) <> {} *)
(* Proof:
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order, FINITE G
Hence z IN cyclic_generators g by cyclic_generators_element
or (cyclic_generators g) <> {} by MEMBER_NOT_EMPTY
*)
val cyclic_generators_nonempty = store_thm(
"cyclic_generators_nonempty",
``!g:'a group. cyclic g /\ FINITE G ==> (cyclic_generators g) <> {}``,
metis_tac[cyclic_generators_element, cyclic_gen_element, cyclic_gen_order, MEMBER_NOT_EMPTY]);
(* Theorem: cyclic g /\ FINITE G ==>
BIJ (\j. (cyclic_gen g) ** j) (coprimes (CARD G)) (cyclic_generators g) *)
(* Proof:
Since cyclic g ==> Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def, FINITE G
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
and 0 < m by finite_group_card_pos
Expanding by BIJ_DEF, INJ_DEF, and SURJ_DEF, this is to show:
(1) z IN G /\ (ord z = m) /\ j IN coprimes m ==> z ** j IN cyclic_generators g
Since z ** j IN G by group_exp_element
and coprime j m by coprimes_element
so ord (z ** j) = m by group_order_power_eq_order
Hence z ** j IN cyclic_generators g by cyclic_generators_element
(2) z IN G /\ (ord z = m) /\ j IN coprimes m /\ j' IN coprimes m /\ z ** j = z ** j' ==> j = j'
If m = 1,
then coprimes 1 = {1} by coprimes_1
hence j = 1 = j' by IN_SING
If m <> 1, 1 < m.
then j IN coprimes m ==> j < m by coprimes_element_less
and j' IN coprimes m ==> j' < m by coprimes_element_less
Therefore j = j' by group_exp_equal
(3) same as (1)
(4) z IN G /\ (ord z = m) /\ x IN cyclic_generators g ==> ?j. j IN coprimes m /\ (z ** j = x)
Since x IN cyclic_generators g
==> x IN G /\ (ord x = m) by cyclic_generators_element
Also ?k. k < m /\ (x = z ** k) by cyclic_element_by_gen
If m = 1,
then ord x = 1 ==> x = #e by group_order_eq_1
then ord z = 1 ==> z = #e by group_order_eq_1
Take j = 1,
and 1 IN (coprimes 1) by coprimes_1, IN_SING
with z ** 1 = x by group_exp_1
If m <> 1,
then x <> #e by group_order_eq_1
thus k <> 0 by group_exp_0
so 0 < k, and k < m ==> k <= m by LESS_IMP_LESS_OR_EQ
Also ord (z ** k) = m ==> coprime k m by group_order_power_eq_order
Take j = k, and j IN coprimes m by coprimes_element
*)
val cyclic_generators_coprimes_bij = store_thm(
"cyclic_generators_coprimes_bij",
``!g:'a group. cyclic g /\ FINITE G ==>
BIJ (\j. (cyclic_gen g) ** j) (coprimes (CARD G)) (cyclic_generators g)``,
rpt strip_tac >>
`Group g ` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `z = cyclic_gen g` >>
qabbrev_tac `m = CARD G` >>
`z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >| [
qabbrev_tac `m = ord z` >>
`coprime j m` by metis_tac[coprimes_element] >>
`z ** j IN G` by rw[] >>
`ord (z ** j) = m` by metis_tac[group_order_power_eq_order] >>
metis_tac[cyclic_generators_element],
qabbrev_tac `m = ord z` >>
Cases_on `m = 1` >-
metis_tac[coprimes_1, IN_SING] >>
`1 < m` by decide_tac >>
metis_tac[coprimes_element_less, group_exp_equal],
qabbrev_tac `m = ord z` >>
`coprime j m` by metis_tac[coprimes_element] >>
`z ** j IN G` by rw[] >>
`ord (z ** j) = m` by metis_tac[group_order_power_eq_order] >>
metis_tac[cyclic_generators_element],
qabbrev_tac `m = ord z` >>
`x IN G /\ (ord x = m)` by metis_tac[cyclic_generators_element] >>
`?k. k < m /\ (x = z ** k)` by metis_tac[cyclic_element_by_gen] >>
Cases_on `m = 1` >-
metis_tac[group_order_eq_1, coprimes_1, IN_SING, group_exp_1] >>
`x <> #e` by metis_tac[group_order_eq_1] >>
`k <> 0` by metis_tac[group_exp_0] >>
`0 < k /\ k <= m` by decide_tac >>
metis_tac[group_order_power_eq_order, coprimes_element]
]);
(* Theorem: cyclic g /\ FINITE G ==> (CARD (cyclic_generators g) = phi (CARD G)) *)
(* Proof:
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
Now BIJ (\j. z ** j) (coprimes m) (cyclic_generators g) by cyclic_generators_coprimes_bij
Since FINITE (coprimes m) by coprimes_finite
and FINITE (cyclic_generators g) by cyclic_generators_finite
Hence CARD (cyclic_generators g)
= CARD (coprimes m) by FINITE_BIJ_CARD_EQ
= phi m by phi_def
*)
val cyclic_generators_card = store_thm(
"cyclic_generators_card",
``!g:'a group. cyclic g /\ FINITE G ==> (CARD (cyclic_generators g) = phi (CARD G))``,
rpt strip_tac >>
qabbrev_tac `z = cyclic_gen g` >>
qabbrev_tac `m = CARD G` >>
`z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >>
`BIJ (\j. z ** j) (coprimes m) (cyclic_generators g)` by rw[cyclic_generators_coprimes_bij, Abbr`z`, Abbr`m`] >>
`FINITE (coprimes m)` by rw[coprimes_finite] >>
`FINITE (cyclic_generators g)` by rw[cyclic_generators_finite] >>
metis_tac[phi_def, FINITE_BIJ_CARD_EQ]);
(*
Goolge: order of elements in a cyclic group.
Pattern of orders of elements in a cyclic group
http://math.stackexchange.com/questions/158281/pattern-of-orders-of-elements-in-a-cyclic-group
The number of elements of order d, where d is a divisor of n, is φ(d).
Let G be a cyclic group of order n, and let a in G be a generator. Let d be a divisor of n.
Certainly, a^{n/d} is an element of G of order d (in other words, is a subgroup of G of order d).
If a^{t} in G is an element of order d, then (a^{t})^{d} = e, hence n ∣ td, and thus (n/d) ∣ t.
This shows that a^{t} in , and thus = (since they are both subgroups of order d).
Thus, there is exactly one subgroup, let's call it H_{d}, of G of order d, for each divisor d of n,
and all of these subgroups are themselves cyclic.
Any cyclic group of order d has ϕ(d) generators, i.e. there are ϕ(d) elements of order d in H_{d},
and hence there are ϕ(d) elements of order d in G. Here, ϕ is Euler's phi function.
This can be checked to make sense via the identity: n = SUM ϕ(d), over d | n.
*)
(* Theorem: cyclic g /\ FINITE G ==> !n. n divides (CARD G) ==>
(cyclic_generators (Generated g ((cyclic_gen g) ** ((CARD G) DIV n))) = orders g n) *)
(* Proof:
Since cyclic g ==> Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def, FINITE G
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
and 0 < m by finite_group_card_pos
Let k = m DIV n, y = z ** k, h = Generated g y.
Then y IN G by group_exp_element
and h <= g by generated_subgroup, y IN G
Expanding by cyclic_generators_def, orders_def, this is to show:
(1) h <= g /\ x IN H ==> x IN G
True by Subgroup_def, SUBSET_DEF.
(2) h <= g /\ order h x = CARD H ==> ord x = n
Note ord x = CARD H by subgroup_order
= ord y by generated_group_card, group_order_pos
= n by group_order_exp_cofactor
(3) h <= g /\ x IN G /\ (ord x) divides m ==> x IN H
True by cyclic_element_in_generated.
(4) h <= g /\ x IN G ==> order h x = CARD H
Note x IN H by cyclic_element_in_generated
and (ord x) divides m by group_order_divides
order h x
= ord x by subgroup_order, x IN H
= ord (z ** k) by group_order_exp_cofactor, (ord x) divides m = ord z
= ord y by y = z ** k
= CARD H by generated_group_card, group_order_pos
*)
val cyclic_generators_gen_cofactor_eq_orders = store_thm(
"cyclic_generators_gen_cofactor_eq_orders",
``!g:'a group. cyclic g /\ FINITE G ==> !n. n divides (CARD G) ==>
(cyclic_generators (Generated g ((cyclic_gen g) ** ((CARD G) DIV n))) = orders g n)``,
rpt strip_tac >>
`Group g ` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `m = CARD G` >>
qabbrev_tac `z = cyclic_gen g` >>
`z IN G` by rw[cyclic_gen_element, Abbr`z`] >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
`ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >>
qabbrev_tac `k = m DIV n` >>
qabbrev_tac `y = z ** k` >>
qabbrev_tac `h = Generated g y` >>
`y IN G` by rw[Abbr`y`, Abbr`z`] >>
`h <= g` by rw[generated_subgroup, Abbr`h`] >>
rw[cyclic_generators_def, orders_def, EXTENSION, EQ_IMP_THM] >-
metis_tac[Subgroup_def, SUBSET_DEF] >-
metis_tac[subgroup_order, generated_group_card, group_order_exp_cofactor, group_order_pos] >-
metis_tac[cyclic_element_in_generated] >>
qabbrev_tac `m = ord z` >>
qabbrev_tac `n = ord x` >>
`x IN H` by metis_tac[cyclic_element_in_generated] >>
`order h x = n` by rw[subgroup_order, Abbr`n`] >>
`ord y = n` by rw[group_order_exp_cofactor, Abbr`m`, Abbr`y`, Abbr`k`] >>
`CARD H = ord y` by rw[generated_group_card, group_order_pos, Abbr`h`] >>
decide_tac);
(* Theorem: cyclic g /\ FINITE G ==>
!n. CARD (orders g n) = if (n divides CARD G) then phi n else 0 *)
(* Proof:
Let m = CARD G.
Note 0 < m by finite_group_card_pos
Since cyclic g ==> Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def, FINITE G
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
If n divides m, to show: CARD (orders g n) = phi n
Let k = m DIV n, y = z ** k, h = Generated g y.
Then y IN G by group_exp_element
and ord y = n by group_order_exp_cofactor
also h <= g by generated_subgroup
and CARD H = n by generated_group_card, group_order_pos
Also cyclic h by cyclic_subgroup_cyclic
and FINITE H by finite_subgroup_carrier_finite
Hence CARD (orders g n)
= CARD (cyclic_generators h) by cyclic_generators_gen_cofactor_eq_orders
= phi n by cyclic_generators_card, FINITE H
If ~(n divides m), to show: CARD (orders g n) = 0
By contradiction, suppose CARD (orders g n) <> 0.
Since FINITE (orders g n) by orders_finite
so orders g n <> {} by CARD_EQ_0
Thus ?x. x IN orders g n by MEMBER_NOT_EMPTY
or x IN G /\ (ord x = n) by orders_element
Now (ord x) divides m by group_order_divides
which contradicts ~(n divides m).
*)
val cyclic_orders_card = store_thm(
"cyclic_orders_card",
``!g:'a group. cyclic g /\ FINITE G ==>
!n. CARD (orders g n) = if (n divides CARD G) then phi n else 0``,
rpt strip_tac >>
`Group g ` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `z = cyclic_gen g` >>
qabbrev_tac `m = CARD G` >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
`z IN G` by rw[cyclic_gen_element, Abbr`z`] >>
`ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >>
Cases_on `n divides m` >| [
simp[] >>
qabbrev_tac `k = m DIV n` >>
qabbrev_tac `y = z ** k` >>
qabbrev_tac `h = Generated g y` >>
`y IN G` by rw[Abbr`y`] >>
`ord y = n` by metis_tac[group_order_exp_cofactor] >>
`h <= g` by rw[generated_subgroup, Abbr`h`] >>
`CARD H = n` by rw[generated_group_card, group_order_pos, Abbr`h`] >>
`cyclic h` by metis_tac[cyclic_subgroup_cyclic] >>
`FINITE H` by metis_tac[finite_subgroup_carrier_finite] >>
metis_tac[cyclic_generators_gen_cofactor_eq_orders, cyclic_generators_card],
simp[] >>
spose_not_then strip_assume_tac >>
`FINITE (orders g n)` by rw[orders_finite] >>
`orders g n <> {}` by rw[GSYM CARD_EQ_0] >>
metis_tac[MEMBER_NOT_EMPTY, orders_element, group_order_divides]
]);
(* ------------------------------------------------------------------------- *)
(* Partition by order equality *)
(* ------------------------------------------------------------------------- *)
(* Define a relation: eq_order *)
val eq_order_def = Define `
eq_order (g:'a group) x y <=> (ord x = ord y)
`;
(* Theorem: (eq_order g) equiv_on G *)
(* Proof: by eq_order_def, equiv_on_def *)
val eq_order_equiv = store_thm(
"eq_order_equiv",
``!g:'a group. (eq_order g) equiv_on G``,
rw[eq_order_def, equiv_on_def]);
(* Theorem: cyclic g /\ FINITE G ==> !n. n divides CARD G ==> orders g n <> {} *)
(* Proof:
Let z = cyclic_gen g, m = CARD G.
Note 0 < m by finite_group_card_pos
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
Let x = z ** (m DIV n)
Then x IN G by group_exp_element
and ord x = n by group_order_exp_cofactor
so x IN (orders g n) by orders_element
Thus orders g n <> {} by MEMBER_NOT_EMPTY
*)
val cyclic_orders_nonempty = store_thm(
"cyclic_orders_nonempty",
``!g:'a group. cyclic g /\ FINITE G ==> !n. n divides CARD G ==> orders g n <> {}``,
rpt strip_tac >>
`Group g ` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `z = cyclic_gen g` >>
qabbrev_tac `m = CARD G` >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
`z IN G` by rw[cyclic_gen_element, Abbr`z`] >>
`ord z = m` by rw[cyclic_gen_order, Abbr`z`, Abbr`m`] >>
qabbrev_tac `x = z ** (m DIV n)` >>
`x IN G` by rw[Abbr`x`] >>
`ord x = n` by metis_tac[group_order_exp_cofactor] >>
metis_tac[orders_element, MEMBER_NOT_EMPTY]);
(* Theorem: cyclic g /\ FINITE G ==>
(partition (eq_order g) G = {orders g n | n | n divides (CARD G)}) *)
(* Proof:
Expanding by partition_def, eq_order_def, orders_def, this is to show:
(1) x' IN G /\ ... ==> ?n. ... (ord x' = n) ... /\ n divides CARD G
Let n = ord x',
Result is true since n divides CARD G by group_order_divides
(2) n divides CARD G /\ ... (ord x'' = n) ... ==> ?x'. x' IN G /\ ... (ord x' = ord x'') ...
Since n divides CARD G
==> (orders g n) <> {} by cyclic_orders_nonempty
==> ?z. z IN G /\ (ord z = n) by orders_element, , MEMBER_NOT_EMPTY
Let x' = z, then the result follows.
*)
val cyclic_eq_order_partition = store_thm(
"cyclic_eq_order_partition",
``!g:'a group. cyclic g /\ FINITE G ==>
(partition (eq_order g) G = {orders g n | n | n divides (CARD G)})``,
rpt strip_tac >>
`Group g ` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
rw[partition_def, eq_order_def, orders_def, EXTENSION, EQ_IMP_THM] >-
metis_tac[group_order_divides] >>
metis_tac[orders_element, cyclic_orders_nonempty, MEMBER_NOT_EMPTY]);
(* Theorem: cyclic g /\ FINITE G ==>
(partition (eq_order g) G = {orders g n | n | n IN divisors (CARD G)}) *)
(* Proof:
Note Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def
==> 0 < CARD G by finite_group_card_pos, FiniteGroup g
partition (eq_order g) G
= {orders g n | n | n divides (CARD G)} by cyclic_eq_order_partition
= {orders g n | n | n IN divisors (CARD G)} by rw[divisors_element_alt
*)
val cyclic_eq_order_partition_alt = store_thm(
"cyclic_eq_order_partition_alt",
``!g:'a group. cyclic g /\ FINITE G ==>
(partition (eq_order g) G = {orders g n | n | n IN divisors (CARD G)})``,
rpt strip_tac >>
`0 < CARD G` by metis_tac[finite_group_card_pos, cyclic_group, FiniteGroup_def] >>
rw[cyclic_eq_order_partition, divisors_element_alt]);
(* We have shown: in a finite cyclic group G,
For each divisor d | |G|, there are phi(d) elements of order d.
Since each element must have some order in a finite group,
the sum of phi(d) over all divisors d will count all elements in the group,
that is, n = SUM phi(d), over d | n.
*)
(* Theorem: cyclic g /\ FINITE G ==>
(IMAGE CARD (partition (eq_order g) g.carrier) = IMAGE phi (divisors (CARD G))) *)
(* Proof:
Since cyclic g ==> Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def
Let z = cyclic_gen g, m = CARD G.
Then z IN G by cyclic_gen_element
and ord z = m by cyclic_gen_order
and 0 < m by finite_group_card_pos
Apply partition_def, eq_order_def, to show:
(1) ?x''. (CARD s = phi x'') /\ x'' IN divisors m
Note s = orders g n by orders_def
Let n = ord x'', y = z ** (m DIV n).
Then n divides m by group_order_divides
and y IN G by group_exp_element
and ord y = n by group_order_exp_cofactor
Since 0 < m, n IN divisors m by divisors_element_alt
hence CARD s = phi n by cyclic_orders_card
So take x'' = n.
(2) x' IN divisors m ==> ?x''. (phi x' = CARD x'') /\ ?x. x IN orders g x'
Let n = x', y = z ** (m DIV n).
Since n IN divisors m,
==> n divides m by divisors_element
Let s = orders g n,
Then CARD s = phi n by cyclic_orders_card
and y IN G by group_exp_element
and ord y = n by group_order_exp_cofactor
so y IN orders g n by orders_element
So take x'' = y.
*)
val cyclic_eq_order_partition_by_card = store_thm(
"cyclic_eq_order_partition_by_card",
``!g:'a group. cyclic g /\ FINITE G ==>
(IMAGE CARD (partition (eq_order g) g.carrier) = IMAGE phi (divisors (CARD G)))``,
rpt strip_tac >>
`Group g` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
qabbrev_tac `m = CARD G` >>
qabbrev_tac `z = cyclic_gen g` >>
`z IN G /\ (ord z = m)` by rw[cyclic_gen_element, cyclic_gen_order, Abbr`z`, Abbr`m`] >>
`0 < m` by rw[finite_group_card_pos, Abbr`m`] >>
rw[partition_def, eq_order_def, EXTENSION, EQ_IMP_THM] >| [
qabbrev_tac `m = ord z` >>
qabbrev_tac `n = ord x''` >>
(`x' = orders g n` by (rw[orders_def, EXTENSION] >> metis_tac[])) >>
qabbrev_tac `y = z ** (m DIV n)` >>
`n divides m` by metis_tac[group_order_divides] >>
`y IN G` by rw[Abbr`y`] >>
`ord y = n` by rw[group_order_exp_cofactor, Abbr`y`, Abbr`m`] >>
metis_tac[cyclic_orders_card, divisors_element_alt],
qabbrev_tac `m = ord z` >>
qabbrev_tac `n = x'` >>
qabbrev_tac `y = z ** (m DIV n)` >>
`n <= m /\ n divides m` by metis_tac[divisors_element] >>
`y IN G` by rw[Abbr`y`] >>
`ord y = n` by rw[group_order_exp_cofactor, Abbr`y`, Abbr`m`] >>
metis_tac[cyclic_orders_card, orders_element]
]);
(* Theorem: eq_order g = feq ord *)
(* Proof:
eq_order g x y
<=> ord x = ord y by eq_order_def
<=> feq ord x y by feq_def
Hence true by FUN_EQ_THM.
*)
val eq_order_is_feq_order = store_thm(
"eq_order_is_feq_order",
``!g:'a group. eq_order g = feq ord``,
rw[eq_order_def, feq_def, FUN_EQ_THM]);
(* Theorem: orders g = feq_class ord G *)
(* Proof:
orders g n
= {x | x IN G /\ (ord x = n)} by orders_def
= feq_class ord G n by feq_class_def
Hence true by FUN_EQ_THM.
*)
val orders_is_feq_class_order = store_thm(
"orders_is_feq_class_order",
``!g:'a group. orders g = feq_class ord G``,
rw[orders_def, feq_class_def, FUN_EQ_THM]);
(* Theorem: cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G)) *)
(* Proof:
Note cyclic g ==> Group g by cyclic_group
and Group g /\ FINITE G ==> FiniteGroup g by FiniteGroup_def
If part: x IN G ==> ord x <= CARD G /\ (ord x) divides (CARD G)
Since FiniteGroup g ==> 0 < CARD G by finite_group_card_pos
also ==> (ord x) divides (CARD G) by group_order_divides
Hence ord x <= CARD G by DIVIDES_LE
Only-if part: n <= CARD G /\ n divides CARD G ==> ?x. x IN G /\ (ord x = n)
True by cyclic_finite_has_order_divisor.
*)
val cyclic_image_ord_is_divisors = store_thm(
"cyclic_image_ord_is_divisors",
``!g:'a group. cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G))``,
rpt strip_tac >>
`Group g` by rw[] >>
`FiniteGroup g` by metis_tac[FiniteGroup_def] >>
rw[EXTENSION, divisors_def, EQ_IMP_THM] >-
rw[group_order_divides, DIVIDES_LE, finite_group_card_pos] >-
rw[group_order_divides] >>
metis_tac[cyclic_finite_has_order_divisor]);
(* Theorem: cyclic g /\ FINITE G ==> (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G))) *)
(* Proof:
Since cyclic g /\ FINITE G
==> FiniteGroup g by FiniteGroup_def, cyclic_group
so 0 < CARD G by finite_group_card_pos
Then partition (eq_order g) G
= {orders g n | n | n divides CARD G} by cyclic_eq_order_partition
= IMAGE (orders g) (divisors (CARD G)) by divisors_def, EXTENSION, DIVIDES_LE
*)
val cyclic_orders_partition = store_thm(
"cyclic_orders_partition",
``!g:'a group. cyclic g /\ FINITE G ==> (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G)))``,
rpt strip_tac >>
`FiniteGroup g` by metis_tac[FiniteGroup_def, cyclic_group] >>
`0 < CARD G` by rw[finite_group_card_pos] >>
`partition (eq_order g) G = {orders g n | n | n divides CARD G}` by rw[cyclic_eq_order_partition] >>
rw[divisors_def, EXTENSION] >>
metis_tac[DIVIDES_LE]);
(* ------------------------------------------------------------------------- *)
(* Finite Cyclic Group Existence. *)
(* ------------------------------------------------------------------------- *)
(* Theorem: 0 < n ==> ?g:num group. cyclic g /\ (CARD g.carrier = n) *)
(* Proof:
Let g = add_mod n.
Then cyclic (add_mod n) by add_mod_cylic
and CARD g.carrier = n by add_mod_card
*)
val finite_cyclic_group_existence = store_thm(
"finite_cyclic_group_existence",
``!n. 0 < n ==> ?g:num group. cyclic g /\ (CARD g.carrier = n)``,
rpt strip_tac >>
qexists_tac `add_mod n` >>
rpt strip_tac >-
rw[add_mod_cylic] >>
rw[add_mod_card]);
(* ------------------------------------------------------------------------- *)
(* Cyclic Group index relative to a generator. *)
(* ------------------------------------------------------------------------- *)
(* Extract cyclic index w.r.t a generator *)
(* Theorem: cyclic g /\ x IN G ==> ?n. (x = (cyclic_gen g) ** n) /\ (FINITE G ==> n < CARD G) *)
(* Proof:
Note Group g by cyclic_def
and cyclic_gen g IN G /\
?k. x = (cyclic_gen g) ** k by cyclic_gen_def
If FINITE G,
Then FiniteGroup g by FiniteGroup_def
so 0 < CARD G by finite_group_card_pos
and ord (cyclic_gen g) = CARD G by cyclic_gen_order
Take n = k MOD (CARD G).
Then (cyclic_gen g) ** n
= (cyclic_gen g) ** k by group_exp_mod, 0 < CARD G
= x by above
and n < CARD G by MOD_LESS, 0 < CARD G
If INFINITE G,
Take n = k, the result follows.
*)
val cyclic_index_exists = store_thm(
"cyclic_index_exists",
``!(g:'a group) x. cyclic g /\ x IN G ==> ?n. (x = (cyclic_gen g) ** n) /\ (FINITE G ==> n < CARD G)``,
rpt strip_tac >>
`Group g` by rw[] >>
`cyclic_gen g IN G /\ ?n. x = (cyclic_gen g) ** n` by rw[cyclic_gen_def] >>
Cases_on `FINITE G` >| [
rw[] >>
`FiniteGroup g` by rw[FiniteGroup_def] >>
`0 < CARD G` by rw[finite_group_card_pos] >>
`ord (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >>
qexists_tac `n MOD (CARD G)` >>
rw[Once group_exp_mod],
metis_tac[]
]);
(* Apply Skolemization *)
val lemma = prove(
``!(g:'a group) x. ?n. cyclic g /\ x IN G ==> (x = (cyclic_gen g) ** n) /\ (FINITE G ==> n < CARD G)``,
metis_tac[cyclic_index_exists]);
(*
- SKOLEM_THM;
> val it = |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) : thm
*)
(* Define cyclic generator *)
(*
- SIMP_RULE (bool_ss) [SKOLEM_THM] lemma;
> val it =
|- ?f. !g x. cyclic g /\ x IN G ==> x = cyclic_gen g ** f g x /\ (FINITE G ==> f g x < CARD G): thm
*)
val cyclic_index_def = new_specification(
"cyclic_index_def",
["cyclic_index"],
SIMP_RULE bool_ss [SKOLEM_THM] lemma);
(*
val cyclic_index_def =
|- !g x. cyclic g /\ x IN G ==> x = cyclic_gen g ** cyclic_index g x /\
(FINITE G ==> cyclic_index g x < CARD G): thm
*)
(* Theorem: cyclic g /\ FINITE G ==>
!n. n < CARD G ==> (cyclic_index g (cyclic_gen g ** n) = n) *)
(* Proof:
Note Group g by cyclic_group
==> FiniteGroup g by FiniteGroup_def
Let x = (cyclic_gen g) ** n.
Note cyclic_gen g IN G by cyclic_gen_def
Then x IN G by group_exp_element
Thus (x = (cyclic_gen g) ** (cyclic_index g x)) /\
cyclic_index g x < CARD G by cyclic_index_def
Now ord (cyclic_gen g) = CARD G by cyclic_gen_order
and 0 < CARD G by finite_group_card_pos
Thus n = cyclic_index g x by group_exp_equal
*)
val finite_cyclic_index_property = store_thm(
"finite_cyclic_index_property",
``!g:'a group. cyclic g /\ FINITE G ==>
!n. n < CARD G ==> (cyclic_index g ((cyclic_gen g) ** n) = n)``,
rpt strip_tac >>
`Group g` by rw[] >>
`FiniteGroup g` by rw[FiniteGroup_def] >>
qabbrev_tac `x = (cyclic_gen g) ** n` >>
`cyclic_gen g IN G` by rw[cyclic_gen_def] >>
`x IN G` by rw[Abbr`x`] >>
`(x = (cyclic_gen g) ** (cyclic_index g x)) /\ cyclic_index g x < CARD G` by fs[cyclic_index_def] >>
`ord (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >>
metis_tac[group_exp_equal, finite_group_card_pos]);
(* Theorem: cyclic g /\ FINITE G /\ x IN G ==>
!n. n < CARD G ==> ((x = (cyclic_gen g) ** n) <=> (n = cyclic_index g x)) *)
(* Proof:
If part: (x = (cyclic_gen g) ** n) ==> (n = cyclic_index g x)
This is true by finite_cyclic_index_property.
Only-if part: (n = cyclic_index g x) ==> (x = (cyclic_gen g) ** n)
This is true by cyclic_index_def
*)
val finite_cyclic_index_unique = store_thm(
"finite_cyclic_index_unique",
``!g:'a group x. cyclic g /\ FINITE G /\ x IN G ==>
!n. n < CARD G ==> ((x = (cyclic_gen g) ** n) <=> (n = cyclic_index g x))``,
rpt strip_tac >>
`Group g` by rw[] >>
rw[cyclic_index_def, EQ_IMP_THM] >>
rw[finite_cyclic_index_property]);
(* Theorem: cyclic g /\ FINITE G /\ x IN G /\ y IN G ==>
(cyclic_index g (x * y) = ((cyclic_index g x) + (cyclic_index g y)) MOD (CARD G)) *)
(* Proof:
Note Group g by cyclic_group
so FiniteGroup g by FiniteGroup_def
and x * y IN G by group_op_element
Let z = cyclic_gen g.
Then z IN G by cyclic_gen_def
and ord z = CARD G by cyclic_gen_order
Note 0 < CARD G by finite_group_card_pos
Let h = cyclic_index g x, k = cyclic_index g y.
z ** ((h + k) MOD CARD G)
= z ** (h + k) by group_exp_mod
= (z ** h) * (z ** k) by group_exp_add
= x * y by cyclic_index_def
Note (h + k) MOD (CARD G) < CARD G by MOD_LESS
Thus (h + k) MOD (CARD G) = cyclic_index g (x * y) by finite_cyclic_index_unique
*)
val finite_cyclic_index_add = store_thm(
"finite_cyclic_index_add",
``!g:'a group x y. cyclic g /\ FINITE G /\ x IN G /\ y IN G ==>
(cyclic_index g (x * y) = ((cyclic_index g x) + (cyclic_index g y)) MOD (CARD G))``,
rpt strip_tac >>
`Group g` by rw[] >>
`FiniteGroup g` by rw[FiniteGroup_def] >>
`x * y IN G` by rw[] >>
qabbrev_tac `z = cyclic_gen g` >>
`z IN G` by rw[cyclic_gen_def, Abbr`z`] >>
`ord z = CARD G` by rw[cyclic_gen_order, Abbr`z`] >>
`0 < CARD G` by rw[finite_group_card_pos] >>
qabbrev_tac `h = cyclic_index g x` >>
qabbrev_tac `k = cyclic_index g y` >>
`z ** ((h + k) MOD CARD G) = z ** (h + k)` by metis_tac[group_exp_mod] >>
`_ = (z ** h) * (z ** k)` by rw[] >>
`_ = x * y` by metis_tac[cyclic_index_def] >>
`0 < CARD G` by rw[finite_group_card_pos] >>
`(h + k) MOD (CARD G) < CARD G` by rw[] >>
metis_tac[finite_cyclic_index_unique]);
(* ------------------------------------------------------------------------- *)
(* Finite Cyclic Group Uniqueness. *)
(* ------------------------------------------------------------------------- *)
(* Theorem: cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2 *)
(* Proof:
Note Group g2 by cyclic_group
and FiniteGroup g2 by FiniteGroup_def
Note cyclic_gen g2 IN g2.carrier by cyclic_gen_def
and order g2 (cyclic_gen g2) = CARD g2.carrier by cyclic_gen_order
By GroupHomo_def, this is to show:
(1) x IN g1.carrier ==> g2.exp (cyclic_gen g2) (cyclic_index g1 x) IN g2.carrier
This is true by group_exp_element
(2) x IN g1.carrier /\ x' IN g1.carrier ==>
g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.op x x')) =
g2.op (g2.exp (cyclic_gen g2) (cyclic_index g1 x)) (g2.exp (cyclic_gen g2) (cyclic_index g1 x'))
g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.op x x'))
= g2.exp (cyclic_gen g2) (((cyclic_index g1 x) +
(cyclic_index g1 x')) MOD (CARD g1.carrier)) by finite_cyclic_index_add
= g2.exp (cyclic_gen g2) ((cyclic_index g1 x) + (cyclic_index g1 x')) by group_exp_mod, group_order_pos
= g2.op (g2.exp (cyclic_gen g2) (cyclic_index g1 x))
(g2.exp (cyclic_gen g2) (cyclic_index g1 x')) by group_exp_add
*)
val finite_cyclic_group_homo = store_thm(
"finite_cyclic_group_homo",
``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2``,
rpt strip_tac >>
`Group g2 /\ FiniteGroup g2` by rw[FiniteGroup_def, cyclic_group] >>
`cyclic_gen g2 IN g2.carrier` by rw[cyclic_gen_def] >>
`order g2 (cyclic_gen g2) = CARD g2.carrier` by rw[cyclic_gen_order] >>
rw[GroupHomo_def] >>
`g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.op x x')) =
g2.exp (cyclic_gen g2) (((cyclic_index g1 x) + (cyclic_index g1 x')) MOD (CARD g1.carrier))` by rw[finite_cyclic_index_add] >>
`_ = g2.exp (cyclic_gen g2) ((cyclic_index g1 x) + (cyclic_index g1 x'))` by metis_tac[group_exp_mod, group_order_pos] >>
rw[group_exp_add]);
(* Theorem: cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier *)
(* Proof:
Note Group g2 by cyclic_group
and FiniteGroup g2 by FiniteGroup_def
Note cyclic_gen g2 IN g2.carrier by cyclic_gen_def
and order g2 (cyclic_gen g2) = CARD g2.carrier by cyclic_gen_order
By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show:
(1) x IN g1.carrier ==> g2.exp (cyclic_gen g2) (cyclic_index g1 x) IN g2.carrier
This is true by group_exp_element
(2) x IN g1.carrier /\ x' IN g1.carrier /\
g2.exp (cyclic_gen g2) (cyclic_index g1 x) = g2.exp (cyclic_gen g2) (cyclic_index g1 x') ==> x = x'
Note cyclic_index g1 x < CARD g2.carrier by cyclic_index_def
and cyclic_index g1 x' < CARD g2.carrier by cyclic_index_def
Thus cyclic_index g1 x = cyclic_index g1 x' by group_exp_equal, group_order_ps
x
= g1.exp (cyclic_gen g1) (cyclic_index g1 x) by finite_cyclic_index_unique
= g1.exp (cyclic_gen g1) (cyclic_index g1 x') by above
= x' by finite_cyclic_index_unique
(3) x IN g2.carrier ==> ?x'. x' IN g1.carrier /\ g2.exp (cyclic_gen g2) (cyclic_index g1 x') = x
Note Group g1 by cyclic_group
and FiniteGroup g1 by FiniteGroup_def
Note cyclic_gen g1 IN g2.carrier by cyclic_gen_def
and order g1 (cyclic_gen g1) = CARD g1.carrier by cyclic_gen_order
and cyclic_index g2 x < CARD g2.carrier by cyclic_index_def
Let x' = g1.exp (cyclic_gen g1) (cyclic_index g2 x).
Then g1.exp (cyclic_gen g1) (cyclic_index g2 x) IN g1.carrier by group_exp_element
and g2.exp (cyclic_gen g2) (cyclic_index g1 (g1.exp (cyclic_gen g1) (cyclic_index g2 x)))
= g2.exp (cyclic_gen g2) (cyclic_index g2 x) by finite_cyclic_index_property
= x by cyclic_index_def
*)
val finite_cyclic_group_bij = store_thm(
"finite_cyclic_group_bij",
``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier``,
rpt strip_tac >>
`Group g2 /\ FiniteGroup g2` by rw[FiniteGroup_def, cyclic_group] >>
`cyclic_gen g2 IN g2.carrier` by rw[cyclic_gen_def] >>
`order g2 (cyclic_gen g2) = CARD g2.carrier` by rw[cyclic_gen_order] >>
rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >| [
`cyclic_index g1 x < CARD g2.carrier /\ cyclic_index g1 x' < CARD g2.carrier` by metis_tac[cyclic_index_def] >>
`cyclic_index g1 x = cyclic_index g1 x'` by metis_tac[group_exp_equal, group_order_pos] >>
metis_tac[finite_cyclic_index_unique],
`Group g1 /\ FiniteGroup g1` by rw[FiniteGroup_def, cyclic_group] >>
`cyclic_gen g1 IN g1.carrier` by rw[cyclic_gen_def] >>
`order g1 (cyclic_gen g1) = CARD g1.carrier` by rw[cyclic_gen_order] >>
qexists_tac `g1.exp (cyclic_gen g1) (cyclic_index g2 x)` >>
rw[] >>
`cyclic_index g2 x < CARD g2.carrier` by rw[cyclic_index_def] >>
`cyclic_index g1 (g1.exp (cyclic_gen g1) (cyclic_index g2 x)) = cyclic_index g2 x` by fs[finite_cyclic_index_property] >>
rw[cyclic_index_def]
]);
(* Theorem: cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
GroupIso (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2 *)
(* Proof:
By GroupIso_def, this is to show:
(1) GroupHomo (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2
This is true by finite_cyclic_group_homo
(2) BIJ (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier g2.carrier
This is true by finite_cyclic_group_bij
*)
val finite_cyclic_group_iso = store_thm(
"finite_cyclic_group_iso",
``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\
FINITE g1.carrier /\ FINITE g2.carrier /\ (CARD g1.carrier = CARD g2.carrier) ==>
GroupIso (\x. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2``,
rw[GroupIso_def] >-
rw[finite_cyclic_group_homo] >>
rw[finite_cyclic_group_bij]);
(* Theorem: cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\
(CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2 *)
(* Proof:
Let f = \x. g2.exp (cyclic_gen g2) (cyclic_index g1 x).
The result follows by finite_cyclic_group_iso
*)
val finite_cyclic_group_uniqueness = store_thm(
"finite_cyclic_group_uniqueness",
``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\
(CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2``,
metis_tac[finite_cyclic_group_iso]);
(* This completes the classification of finite cyclic groups. *)
(* Another proof of uniqueness *)
(* Theorem: cyclic g /\ FINITE G ==> GroupHomo (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g *)
(* Proof:
Note Group g by cyclic_group
and FiniteGroup g by FiniteGroup_def
and cyclic_gen g IN G by cyclic_gen_def
and order g (cyclic_gen g) = CARD G by cyclic_gen_order
By GroupHomo_def, this is to show:
(1) (cyclic_gen g) ** n IN G, true by group_exp_element
(2) n < CARD G /\ n' < CARD G ==>
cyclic_gen g ** ((n + n') MOD CARD G) = cyclic_gen g ** n * cyclic_gen g ** n'
Note cyclic_gen g ** ((n + n') MOD CARD G)
= cyclic_gen g ** (n + n') by group_exp_mod, 0 < CARD G
= cyclic_gen g ** n * cyclic_gen g ** n' by group_exp_add
*)
val finite_cyclic_group_add_mod_homo = store_thm(
"finite_cyclic_group_add_mod_homo",
``!g:'a group. cyclic g /\ FINITE G ==> GroupHomo (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g``,
rpt strip_tac >>
`Group g /\ FiniteGroup g` by rw[FiniteGroup_def, cyclic_group] >>
`cyclic_gen g IN G` by rw[cyclic_gen_def] >>
`order g (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >>
rw[GroupHomo_def] >>
`0 < CARD G` by decide_tac >>
`cyclic_gen g ** ((n + n') MOD CARD G) = cyclic_gen g ** (n + n')` by metis_tac[group_exp_mod] >>
rw[]);
(* Theorem: cyclic g /\ FINITE G ==> BIJ (\n. (cyclic_gen g) ** n) (add_mod (CARD G)).carrier G *)
(* Proof:
Note Group g by cyclic_group
and FiniteGroup g by FiniteGroup_def
and cyclic_gen g IN G by cyclic_gen_def
and order g (cyclic_gen g) = CARD G by cyclic_gen_order
By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show:
(1) (cyclic_gen g) ** n IN G, true by group_exp_element
(2) n < CARD G /\ n' < CARD G /\ cyclic_gen g ** n = cyclic_gen g ** n' ==> n = n'
This is true by finite_cyclic_index_property
(3) x IN G ==> ?n. n < CARD G /\ (cyclic_gen g ** n = x)
This is true by cyclic_index_def
*)
val finite_cyclic_group_add_mod_bij = store_thm(
"finite_cyclic_group_add_mod_bij",
``!g:'a group. cyclic g /\ FINITE G ==> BIJ (\n. (cyclic_gen g) ** n) (add_mod (CARD G)).carrier G``,
rpt strip_tac >>
`Group g /\ FiniteGroup g` by rw[FiniteGroup_def, cyclic_group] >>
`cyclic_gen g IN G` by rw[cyclic_gen_def] >>
`order g (cyclic_gen g) = CARD G` by rw[cyclic_gen_order] >>
rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >-
metis_tac[finite_cyclic_index_property] >>
metis_tac[cyclic_index_def]);
(* Theorem: cyclic g /\ FINITE G ==> GroupIso (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g *)
(* Proof:
By GroupIso_def, this is to show:
(1) GroupHomo (\n. cyclic_gen g ** n) (add_mod (CARD G)) g
This is true by finite_cyclic_group_add_mod_homo
(2) BIJ (\n. cyclic_gen g ** n) (add_mod (CARD G)).carrier G
This is true by finite_cyclic_group_add_mod_bij
*)
val finite_cyclic_group_add_mod_iso = store_thm(
"finite_cyclic_group_add_mod_iso",
``!g:'a group. cyclic g /\ FINITE G ==> GroupIso (\n. (cyclic_gen g) ** n) (add_mod (CARD G)) g``,
rw_tac std_ss[GroupIso_def] >-
rw[finite_cyclic_group_add_mod_homo] >>
rw[finite_cyclic_group_add_mod_bij]);
(* Theorem: cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\
(CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2 *)
(* Proof:
Note Group g1 by cyclic_group
so FiniteGroup g1 by FiniteGroup_def
==> 0 < CARD g1.carrier by finite_group_card_pos
Thus Group (add_mod (CARD g1.carrier)) by add_mod_group, 0 < CARD g1.carrier
Let f1 = (\n. g1.exp (cyclic_gen g1) n),
f2 = (\n. g2.exp (cyclic_gen g2) n).
Now GroupIso f1 (add_mod (CARD g1.carrier)) g1 by finite_cyclic_group_add_mod_iso
and GroupIso f2 (add_mod (CARD g2.carrier)) g2 by finite_cyclic_group_add_mod_iso
Thus GroupIso (LINV f1 (add_mod (CARD g1.carrier)).carrier) g1 (add_mod (CARD g1.carrier))
by group_iso_sym
or ?f. GroupIso f g1 g2 by group_iso_trans
*)
val finite_cyclic_group_uniqueness = store_thm(
"finite_cyclic_group_uniqueness",
``!g1:'a group g2:'b group. cyclic g1 /\ cyclic g2 /\ FINITE g1.carrier /\ FINITE g2.carrier /\
(CARD g1.carrier = CARD g2.carrier) ==> ?f. GroupIso f g1 g2``,
rpt strip_tac >>
`Group g1 /\ FiniteGroup g1` by rw[cyclic_group, FiniteGroup_def] >>
`0 < CARD g1.carrier` by rw[finite_group_card_pos] >>
`Group (add_mod (CARD g1.carrier))` by rw[add_mod_group] >>
`GroupIso (\n. g1.exp (cyclic_gen g1) n) (add_mod (CARD g1.carrier)) g1` by rw[finite_cyclic_group_add_mod_iso] >>
`GroupIso (\n. g2.exp (cyclic_gen g2) n) (add_mod (CARD g2.carrier)) g2` by rw[finite_cyclic_group_add_mod_iso] >>
metis_tac[group_iso_sym, group_iso_trans]);
(* ------------------------------------------------------------------------- *)
(* Isomorphism between Cyclic Groups *)
(* ------------------------------------------------------------------------- *)
(* Theorem: cyclic g /\ cyclic h /\ FINITE G /\
GroupIso f g h ==> f (cyclic_gen g) IN (cyclic_generators h) *)
(* Proof:
Note Group g /\ Group h by cyclic_group
and cyclic_gen g IN G by cyclic_gen_element
By cyclic_generators_element, this is to show:
(1) f (cyclic_gen g) IN h.carrier, true by group_iso_element
(2) order h (f (cyclic_gen g)) = CARD h.carrier
order h (f (cyclic_gen g))
= ord (cyclic_gen g) by group_iso_order
= CARD G by cyclic_gen_order, FINITE G
= CARD h.carrier by group_iso_card_eq
*)
val cyclic_iso_gen = store_thm(
"cyclic_iso_gen",
``!(g:'a group) (h:'b group) f. cyclic g /\ cyclic h /\ FINITE G /\
GroupIso f g h ==> f (cyclic_gen g) IN (cyclic_generators h)``,
rpt strip_tac >>
`Group g /\ Group h` by rw[] >>
`cyclic_gen g IN G` by rw[cyclic_gen_element] >>
rw[cyclic_generators_element] >-
metis_tac[group_iso_element] >>
`order h (f (cyclic_gen g)) = ord (cyclic_gen g)` by rw[group_iso_order] >>
`_ = CARD G` by rw[cyclic_gen_order] >>
metis_tac[group_iso_card_eq]);
(* ------------------------------------------------------------------------- *)
(* export theory at end *)
val _ = export_theory();
(*===========================================================================*)