Theory Field_Mult_Cyclic
section ‹A finite subgroup of the multiplicative group of a field is cyclic›
theory Field_Mult_Cyclic
imports Poly_Ring Group_Operations
begin
text ‹In particular the multiplicative group of a finite field (e.g.\ ‹GF(p⇧n)›) is cyclic.
The argument splits into a group-theoretic part and a field-theoretic part.
If a finite group @{term G} satisfies the
∗‹root bound› that for every @{term "n > 0"} at most @{term n} elements @{term x} satisfy
‹x⇧n = 1›, then @{term G} is cyclic. The field part supplies the root bound: the elements
@{term x} of the multiplicative group with ‹x⇧n = 1› are roots of the polynomial ‹X⇧n - 1›,
and a field has at most @{term n} such roots.›
subsection ‹The order of a power in a finite group›
context Group
begin
text ‹In a finite group, the order of @{term "power a k"} is @{term "element_order a div gcd (element_order a) k"}.
This is the key computation behind counting the elements of each order in a cyclic group.›
lemma element_order_power:
assumes fin: "finite G" and aG: "a ∈ G"
shows "element_order (power a k) = element_order a div gcd (element_order a) k"
proof -
define e where "e = element_order a"
define d where "d = gcd e k"
have e_pos: "e > 0" unfolding e_def using element_order_pos[OF fin aG] .
have ak: "power a k ∈ G" using aG by simp
have pow_iff: "power (power a k) m = 𝟭 ⟷ (e div d) dvd m" for m
proof -
have step: "power (power a k) m = 𝟭 ⟷ e dvd (k * m)"
using aG e_def element_order_dvd fin power_mult power_element_order power_unit
by (metis dvd_def)
have d_pos: "d > 0" unfolding d_def using e_pos by simp
have d_dvd_e: "d dvd e" and d_dvd_k: "d dvd k" unfolding d_def by auto
have "coprime (e div d) (k div d)"
unfolding d_def using e_pos by (simp add: div_gcd_coprime)
with step coprime_dvd_mult_right_iff d_dvd_e d_dvd_k show ?thesis
by fastforce
qed
then show ?thesis
using ak d_def e_def element_order_dvd fin power_element_order
by (metis gcd_nat.asym gcd_nat.refl)
qed
end
subsection ‹Counting elements of each order in a cyclic group›
context Group
begin
text ‹The elements of order exactly @{term e} in the cyclic group generated by @{term a}
(where @{term a} has order @{term e}) are exactly its generators: the powers @{term "power a k"}
with @{term k} below @{term e} and coprime to it.›
lemma card_order_e_in_cyclic:
assumes fin: "finite G" and aG: "a ∈ G" and ord_a: "element_order a = e"
shows "card {x ∈ cyclic_subgroup a. element_order x = e} = card {k. k < e ∧ gcd e k = 1}"
proof -
have e_pos: "e > 0"
using ord_a element_order_pos[OF fin aG] by simp
have set_eq: "{x ∈ cyclic_subgroup a. element_order x = e}
= power a ` {k. k < e ∧ gcd e k = 1}" (is "?L=?R")
proof
show "?L ⊆ ?R"
proof
fix x assume xc: "x ∈ ?L"
then obtain k where xk: "x = power a k" and kl: "k < e"
unfolding cyclic_subgroup_def ord_a by auto
have "element_order (power a k) = e"
using element_order_power[OF fin aG] ord_a xc xk by blast
then have "gcd e k = 1"
by (simp add: aG div_eq_dividend_iff e_pos element_order_power fin ord_a)
then show "x ∈ ?R" using xk kl by auto
qed
qed (auto simp: cyclic_subgroup_def aG element_order_power fin ord_a)
have "inj_on (power a) {..<e}" using power_inj_on_order[OF fin aG] ord_a by simp
then have inj: "inj_on (power a) {k. k < e ∧ gcd e k = 1}"
by (rule inj_on_subset) (auto simp: lessThan_def)
show "card {x ∈ cyclic_subgroup a. element_order x = e} = card {k. k < e ∧ gcd e k = 1}"
using set_eq inj card_image by auto
qed
end
subsection ‹Counting the Residues Coprime to a Modulus›
text ‹
The cyclicity criterion for a finite group needs two arithmetic facts about the number of
residues below @{term e} coprime to @{term e}: that it is positive, and that summing it over the
divisors of @{term d} recovers @{term d}.
›
lemma coprime_count_pos:
fixes e :: nat
assumes "0 < e" shows "0 < card {k. k < e ∧ gcd e k = 1}"
using Suc_lessI [OF assms] by (fastforce simp: card_gt_0_iff)
text ‹The residues below @{term d} whose greatest common divisor with @{term d} is exactly @{term f}
are the multiples @{term "j * f"} of @{term f} by residues below @{term "d div f"} coprime to it.›
lemma card_gcd_class:
fixes d f :: nat
assumes d: "0 < d" and f: "f dvd d"
shows "card {j. j < d div f ∧ gcd (d div f) j = 1} = card {k. k < d ∧ gcd k d = f}"
proof (rule bij_betw_same_card)
have fpos: "0 < f" using d f by (auto intro: dvd_pos_nat)
have deq: "d div f * f = d" using f by simp
show "bij_betw (λj. j * f) {j. j < d div f ∧ gcd (d div f) j = 1} {k. k < d ∧ gcd k d = f}"
unfolding bij_betw_def
proof
show "inj_on (λj. j * f) {j. j < d div f ∧ gcd (d div f) j = 1}"
using fpos by (simp add: inj_on_def)
next
show "(λj. j * f) ` {j. j < d div f ∧ gcd (d div f) j = 1} = {k. k < d ∧ gcd k d = f}"
proof (intro set_eqI iffI)
fix k assume "k ∈ (λj. j * f) ` {j. j < d div f ∧ gcd (d div f) j = 1}"
then obtain j where j: "j < d div f" "gcd (d div f) j = 1" and k: "k = j * f" by auto
from j(1) fpos have "j * f < d div f * f" by (rule mult_less_mono1)
then have "k < d" using k deq by simp
moreover have "gcd k d = f"
proof -
have "gcd k d = gcd (j * f) (d div f * f)" using k deq by simp
also have "… = gcd (d div f) j * f" by (simp add: gcd_mult_right)
also have "… = f" using j(2) by simp
finally show ?thesis .
qed
ultimately show "k ∈ {k. k < d ∧ gcd k d = f}" by simp
next
fix k assume "k ∈ {k. k < d ∧ gcd k d = f}"
then have k: "k < d" and g: "gcd k d = f" and keq: "k div f * f = k" by auto
have "gcd (d div f) (k div f) * f = f" using g
using deq keq by (metis gcd.commute gcd_mult_distrib_nat mult.commute)
moreover have "k div f < d div f" using k fpos f by (simp add: div_less_iff_less_mult)
ultimately show "k ∈ (λj. j * f) ` {j. j < d div f ∧ gcd (d div f) j = 1}"
using keq fpos by (force simp: image_iff)
qed
qed
qed
text ‹Summing the coprime counts over the divisors of @{term d} recovers @{term d}: the residues
below @{term d} are partitioned by their greatest common divisor with @{term d}.›
theorem coprime_count_divisor_sum:
fixes d :: nat
assumes d: "0 < d"
shows "(∑e | e dvd d. card {k. k < e ∧ gcd e k = 1}) = d"
proof -
have part: "{k. k < d} = (⋃f ∈ {f. f dvd d}. {k. k < d ∧ gcd k d = f})"
by auto
have "d = card {k. k < d}" by simp
also have "… = (∑f | f dvd d. card {k. k < d ∧ gcd k d = f})"
unfolding part using d by (intro card_UN_disjoint) auto
also have "… = (∑f | f dvd d. card {j. j < d div f ∧ gcd (d div f) j = 1})"
using card_gcd_class [OF d] by simp
also have "… = (∑e | e dvd d. card {k. k < e ∧ gcd e k = 1})"
proof (rule sum.reindex_bij_witness [of _ "λe. d div e" "λf. d div f"])
qed (use d div_div_eq_right in auto)
finally show ?thesis by simp
qed
subsection ‹The abstract group criterion for being cyclic›
context Group
begin
text ‹The set of elements of order exactly @{term e} in a finite group.›
text ‹Every element of a finite group has order dividing @{term "card G"}, so the group is
partitioned by order over the divisors of @{term "card G"}.›
lemma card_G_sum_orders:
assumes fin: "finite G"
shows "card G = (∑e | e dvd card G. card {x ∈ G. element_order x = e})"
proof -
have part: "G = (⋃e ∈ {e. e dvd card G}. {x ∈ G. element_order x = e})"
using element_order_dvd_card[OF fin] by auto
have "card G > 0"
using fin card_gt_0_iff unit_closed by blast
then have fin_div: "finite {e. e dvd card G}" by (rule finite_divisors_nat)
have "card G = card (⋃e ∈ {e. e dvd card G}. {x ∈ G. element_order x = e})"
using part by simp
also have "… = (∑e | e dvd card G. card {x ∈ G. element_order x = e})"
using fin by (intro card_UN_disjoint fin_div) auto
finally show ?thesis .
qed
text ‹The root bound: for each positive @{term n}, at most @{term n} elements satisfy ‹x⇧n = 1›.
Under this hypothesis, at most @{term "card {k. k < e ∧ gcd e k = 1}"} elements have order
exactly @{term e}.›
lemma card_order_e_le_coprime_count:
assumes fin: "finite G"
and bound: "⋀n. n > 0 ⟹ card {x ∈ G. power x n = 𝟭} ≤ n"
and e_pos: "e > 0"
shows "card {x ∈ G. element_order x = e} ≤ card {k. k < e ∧ gcd e k = 1}"
proof (cases "{x ∈ G. element_order x = e} = {}")
case True show ?thesis
by (simp add: True)
next
case False
then obtain a where aG: "a ∈ G" and ord_a: "element_order a = e" by auto
have cyc_sub: "cyclic_subgroup a ⊆ {x ∈ G. power x e = 𝟭}"
proof
fix x assume "x ∈ cyclic_subgroup a"
then obtain k where xk: "x = power a k" and "k < e"
unfolding cyclic_subgroup_def ord_a by auto
have "power x e = 𝟭"
using aG fin power_mult ord_a power_element_order power_unit xk by (metis mult.commute)
with xk aG show "x ∈ {x ∈ G. power x e = 𝟭}" by simp
qed
have "card (cyclic_subgroup a) = e"
using card_cyclic_subgroup[OF fin aG] ord_a by simp
with cyc_sub bound[OF e_pos] fin have *: "cyclic_subgroup a = {x ∈ G. power x e = 𝟭}"
by (simp add: card_seteq)
have "{x ∈ G. element_order x = e} = {x ∈ cyclic_subgroup a. element_order x = e}"
by (auto simp: * fin power_element_order)
then show ?thesis
using card_order_e_in_cyclic[OF fin aG ord_a] by simp
qed
text ‹The abstract criterion: a finite group satisfying the root bound is cyclic.›
theorem cyclic_of_root_bound:
assumes fin: "finite G" and ne: "G ≠ {}"
and bound: "⋀n. n > 0 ⟹ card {x ∈ G. power x n = 𝟭} ≤ n"
shows "∃g ∈ G. cyclic_subgroup g = G"
proof -
define d where "d = card G"
have d_pos: "d > 0" unfolding d_def using fin ne by (simp add: card_gt_0_iff)
have sum_orders: "(∑e | e dvd d. card {x ∈ G. element_order x = e}) = d"
unfolding d_def using card_G_sum_orders[OF fin] by simp
have sum_counts: "(∑e | e dvd d. card {k. k < e ∧ gcd e k = 1}) = d"
using coprime_count_divisor_sum [OF d_pos] by simp
have fin_div: "finite {e. e dvd d}"
using d_pos finite_divisors_nat by (metis gr_implies_not0)
have le: "card {x ∈ G. element_order x = e} ≤ card {k. k < e ∧ gcd e k = 1}"
if "e dvd d" for e
using bound card_0_eq card_order_e_le_coprime_count d_def fin that by fastforce
have eq_all: "card {x ∈ G. element_order x = e0} = card {k. k < e0 ∧ gcd e0 k = 1}"
if "e0 dvd d" for e0
proof (rule ccontr)
assume neq: "card {x ∈ G. element_order x = e0} ≠ card {k. k < e0 ∧ gcd e0 k = 1}"
with le that have strict: "card {x ∈ G. element_order x = e0}
< card {k. k < e0 ∧ gcd e0 k = 1}" by force
have "(∑e | e dvd d. card {x ∈ G. element_order x = e})
< (∑e | e dvd d. card {k. k < e ∧ gcd e k = 1})"
by (intro sum_strict_mono_ex1 fin_div) (use that strict le in auto)
with sum_orders sum_counts show False by simp
qed
have "card {x ∈ G. element_order x = d} = card {k. k < d ∧ gcd d k = 1}"
using eq_all by simp
moreover have "card {k. k < d ∧ gcd d k = 1} > 0" using d_pos by (rule coprime_count_pos)
ultimately have "{x ∈ G. element_order x = d} ≠ {}" by (metis card.empty less_irrefl)
then obtain g where gG: "g ∈ G" and gord: "element_order g = d" by auto
have "cyclic_subgroup g = G"
by (simp add: card_cyclic_subgroup card_subset_eq cyclic_subgroup_subset d_def fin gG gord)
with gG show ?thesis by blast
qed
end
subsection ‹The multiplicative group of a field and the root bound›
context Field
begin
text ‹The nonzero elements of the field.›
definition Fstar :: "'a set"
where "Fstar = R - {𝟬}"
lemma Fstar_iff [simp]: "x ∈ Fstar ⟷ x ∈ R ∧ x ≠ 𝟬"
unfolding Fstar_def by auto
lemma one_in_Fstar: "𝟭 ∈ Fstar"
using nontrivial by simp
text ‹The nonzero elements form a group under multiplication.›
theorem Group_Fstar: "Group Fstar (⋅) 𝟭"
proof (intro GroupI one_in_Fstar)
fix a b assume "a ∈ Fstar" "b ∈ Fstar"
then show "a ⋅ b ∈ Fstar"
using local.no_zero_divisors by auto
next
fix u assume "u ∈ Fstar"
then show "∃v ∈ Fstar. u ⋅ v = 𝟭 ∧ v ⋅ u = 𝟭"
using field_inverse nontrivial by fastforce
qed (auto simp: multiplicative.associative)
end
subsection ‹The polynomial root bound, via the polynomial ring›
text ‹The number of ‹n›th roots of unity in a field is at most ‹n›. Rather than reproving a bound on
polynomial roots by hand, we reuse @{thm [source] Field.card_roots_le_degree} from
‹Poly_Ring›: the ‹n›th roots of unity are exactly the roots of the polynomial
‹X⇧n - 1›, which is nonzero of degree ‹n›.›
context Field
begin
text ‹The ring power @{const rpow} of ‹Poly_Ring› agrees with the multiplicative
group power.›
lemma rpow_eq_power: "rpow x n = multiplicative.power x n"
by (induction n) simp_all
text ‹The polynomial ‹X⇧n - 1›, as a coefficient sequence: @{term "- 𝟭"} at 0, @{term 𝟭} at @{term n},
and @{term 𝟬} elsewhere (valid for @{term "n > 0"}).›
definition xn_minus_1 :: "nat ⇒ (nat ⇒ 'a)"
where "xn_minus_1 n ≡ (λi. if i = 0 then - 𝟭 else if i = n then 𝟭 else 𝟬)"
lemma xn_minus_1_closed: "xn_minus_1 n ∈ poly_carrier"
proof (rule poly_carrierI)
have "{i. xn_minus_1 n i ≠ 𝟬} ⊆ {0, n}" by (auto simp: xn_minus_1_def)
then show "finite {i. xn_minus_1 n i ≠ 𝟬}" by (rule finite_subset) simp
show "⋀i. xn_minus_1 n i ∈ R" by (simp add: xn_minus_1_def)
qed
lemma xn_minus_1_coeff: "xn_minus_1 n i ∈ R"
by (simp add: xn_minus_1_def)
lemma degree_xn_minus_1:
assumes n: "n > 0" shows "degree (xn_minus_1 n) = n"
proof (rule le_antisym)
show "degree (xn_minus_1 n) ≤ n"
using degree_le_iff xn_minus_1_closed xn_minus_1_def by auto
then show "n ≤ degree (xn_minus_1 n)"
using coeff_gt_degree le_eq_less_or_eq nontrivial xn_minus_1_closed xn_minus_1_def by fastforce
qed
lemma xn_minus_1_nonzero:
assumes n: "n > 0" shows "xn_minus_1 n ≠ 𝟬⇩P"
by (metis degree_xn_minus_1 degree_zero less_zeroE n)
text ‹Its value at @{term x} is @{term "multiplicative.power x n - 𝟭"}.›
lemma eval_xn_minus_1:
assumes n: "n > 0" and x: "x ∈ R"
shows "eval x (xn_minus_1 n) = multiplicative.power x n + (- 𝟭)"
proof -
have "eval x (xn_minus_1 n) = additive.fincomp (λi. xn_minus_1 n i ⋅ rpow x i) {..n}"
using degree_xn_minus_1 local.eval_def n by force
also have "… = additive.fincomp (λi. xn_minus_1 n i ⋅ rpow x i) {0, n}"
using x
by (intro additive.fincomp_mono_neutral_cong_right) (auto simp: xn_minus_1_def xn_minus_1_coeff)
also have "… = (- 𝟭) + multiplicative.power x n"
using n x by (simp add: xn_minus_1_coeff xn_minus_1_def rpow_eq_power)
also have "… = multiplicative.power x n + (- 𝟭)"
using x by (simp add: additive.commutative)
finally show ?thesis .
qed
text ‹The roots of unity are exactly the roots of ‹X⇧n - 1›.›
lemma card_nth_roots_of_unity:
assumes n: "n > 0"
shows "finite {x ∈ R. multiplicative.power x n = 𝟭}
∧ card {x ∈ R. multiplicative.power x n = 𝟭} ≤ n"
proof -
have "multiplicative.power x n = 𝟭"
if "x ∈ R" and "multiplicative.power x n - 𝟭 = 𝟬" for x
proof -
have "multiplicative.power x n = (multiplicative.power x n + (- 𝟭)) + 𝟭"
using additive.invertible_left_inverse[of 𝟭] ‹x ∈ R› by (simp add: additive.associative)
also have "… = 𝟭" using that by (simp add: additive.associative)
finally show "multiplicative.power x n = 𝟭" .
qed
then have "{x ∈ R. multiplicative.power x n = 𝟭} = {x ∈ R. eval x (xn_minus_1 n) = 𝟬}"
by (auto simp: eval_xn_minus_1 n)
then show ?thesis
using degree_xn_minus_1[OF n] xn_minus_1_closed xn_minus_1_nonzero[OF n] card_roots_le_degree
by force
qed
end
subsection ‹The main theorem›
text ‹The @{term Fstar}-power (multiplicative power in the group of nonzero elements) coincides
with the field's multiplicative power, so the root bound transfers to the group.›
context Field
begin
lemma Fstar_power_eq:
"Monoid.power (⋅) 𝟭 x n = multiplicative.power x n"
by (simp only: Monoid.power_def)
text ‹Any finite subgroup of the multiplicative group of a field is cyclic.›
theorem finite_subgroup_Fstar_cyclic:
assumes sub: "Subgroup H Fstar (⋅) 𝟭" and fin: "finite H"
shows "∃g ∈ H. Group.cyclic_subgroup (⋅) 𝟭 g = H"
proof -
interpret G: Group Fstar "(⋅)" 𝟭 by (rule Group_Fstar)
interpret H: Subgroup H Fstar "(⋅)" 𝟭 by (rule sub)
have HR: "H ⊆ R" using H.subset by (auto simp: Fstar_def)
have bound: "card {x ∈ H. Monoid.power (⋅) 𝟭 x n = 𝟭} ≤ n" if n: "n > 0" for n
proof -
have sub_set: "{x ∈ H. Monoid.power (⋅) 𝟭 x n = 𝟭} ⊆ {x ∈ R. multiplicative.power x n = 𝟭}"
using HR by blast
then show ?thesis
by (metis (no_types, lifting) card_mono card_nth_roots_of_unity[of n] order_trans that)
qed
have ne: "H ≠ {}" using H.sub.unit_closed by auto
show ?thesis
using H.sub.cyclic_of_root_bound[OF fin ne] bound by blast
qed
text ‹In particular, if the whole multiplicative group @{term Fstar} is finite (e.g.\ a finite
field), it is cyclic.›
corollary finite_field_mult_cyclic:
assumes fin: "finite Fstar"
shows "∃g ∈ Fstar. Group.cyclic_subgroup (⋅) 𝟭 g = Fstar"
by (simp add: Group.group_self_subgroup Group_Fstar fin finite_subgroup_Fstar_cyclic)
end
end