Theory Cyclic_Group
section ‹Cyclic groups›
theory Cyclic_Group imports
"HOL-Algebra.Coset"
begin
record 'a cyclic_group = "'a monoid" +
generator :: 'a (‹❙gı›)
locale cyclic_group = group G
for G :: "('a, 'b) cyclic_group_scheme" (structure)
+
assumes generator_closed [intro, simp]: "generator G ∈ carrier G"
and generator: "carrier G ⊆ range (λn :: nat. generator G [^]⇘G⇙ n)"
begin
lemma generatorE [elim?]:
assumes "x ∈ carrier G"
obtains n :: nat where "x = generator G [^] n"
using generator assms by auto
lemma inj_on_generator: "inj_on (([^]) ❙g) {..<order G}"
proof(rule inj_onI)
fix n m
assume "n ∈ {..<order G}" "m ∈ {..<order G}"
hence n: "n < order G" and m: "m < order G" by simp_all
moreover
assume "❙g [^] n = ❙g [^] m"
ultimately show "n = m"
proof(induction n m rule: linorder_wlog)
case sym thus ?case by simp
next
case (le n m)
let ?d = "m - n"
have "❙g [^] (int m - int n) = ❙g [^] int m ⊗ inv (❙g [^] int n)"
by(simp add: int_pow_diff)
also have "❙g [^] int m = ❙g [^] int n" by(simp add: le.prems int_pow_int)
also have "… ⊗ inv (❙g [^] (int n)) = 𝟭" by simp
finally have "❙g [^] ?d = 𝟭"
using le.prems(3) pow_eq_div2 by force
{ assume "n < m"
have "carrier G ⊆ (λn. ❙g [^] n) ` {..<?d}"
proof
fix x
assume "x ∈ carrier G"
then obtain k :: nat where "x = ❙g [^] k" ..
also have "… = (❙g [^] ?d) [^] (k div ?d) ⊗ ❙g [^] (k mod ?d)"
by(simp add: nat_pow_pow nat_pow_mult div_mult_mod_eq)
also have "… = ❙g [^] (k mod ?d)"
using ‹❙g [^] ?d = 𝟭› by simp
finally show "x ∈ (λn. ❙g [^] n) ` {..<?d}" using ‹n < m› by auto
qed
hence "order G ≤ card ((λn. ❙g [^] n) ` {..<?d})"
by(simp add: order_def card_mono)
also have "… ≤ card {..<?d}" by(rule card_image_le) simp
also have "… < order G" using ‹m < order G› by simp
finally have False by simp }
with ‹n ≤ m› show "n = m" by(auto simp add: order.order_iff_strict)
qed
qed
lemma finite_carrier: "finite (carrier G)"
proof -
from generator obtain n :: nat where "❙g [^] n = inv ❙g"
by(metis generatorE generator_closed inv_closed)
then have g1: "❙g [^] (Suc n) = 𝟭"
by auto
have mod: "❙g [^] m = ❙g [^] (m mod Suc n)" for m
proof -
obtain k where "m mod Suc n + Suc n * k = m"
using mod_mult_div_eq by blast
then have "❙g [^] m = ❙g [^] (m mod Suc n + Suc n * k)" by simp
also have "… = ❙g [^] (m mod Suc n)"
unfolding nat_pow_mult[symmetric, OF generator_closed] nat_pow_pow[symmetric, OF generator_closed] g1
by simp
finally show ?thesis .
qed
have "❙g [^] x ∈ ([^]) ❙g ` {..<Suc n}" for x :: nat by (subst mod) auto
then have "range (([^]) ❙g :: nat ⇒ _) ⊆ (([^]) ❙g) ` {..<Suc n}" by auto
then have "finite (range (([^]) ❙g :: nat ⇒ _))" by(rule finite_surj[rotated]) simp
with generator show ?thesis by(rule finite_subset)
qed
lemma carrier_conv_generator: "carrier G = (λn. ❙g [^] n) ` {..<order G}"
proof -
have "(λn. ❙g [^] n) ` {..<order G} ⊆ carrier G" by auto
moreover have "card ((λn. ❙g [^] n) ` {..<order G}) ≥ order G"
using inj_on_generator by(simp add: card_image)
ultimately show ?thesis using finite_carrier
unfolding order_def by(rule card_seteq[symmetric, rotated])
qed
lemma bij_betw_generator_carrier:
"bij_betw (λn :: nat. ❙g [^] n) {..<order G} (carrier G)"
by (simp add: carrier_conv_generator inj_on_generator inj_on_imp_bij_betw)
lemma order_gt_0: "order G > 0"
using order_gt_0_iff_finite by(simp add: finite_carrier)
end
lemma (in monoid) order_in_range_Suc: "order G ∈ range Suc ⟷ finite (carrier G)"
by(cases "order G")(auto simp add: order_def carrier_not_empty intro: card_ge_0_finite)
end