Library mathcomp.solvable.cyclic
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Properties of cyclic groups.
Definitions:
Defined in fingroup.v:
< [x]> == the cycle (cyclic group) generated by x.
# [x] == the order of x, i.e., the cardinal of < [x]>.
Defined in prime.v:
totient n == Euler's totient function
Definitions in this file:
cyclic G <=> G is a cyclic group.
metacyclic G <=> G is a metacyclic group (i.e., a cyclic extension of a
cyclic group).
generator G x <=> x is a generator of the (cyclic) group G.
Zpm x == the isomorphism mapping the additive group of integers
mod # [x] to the cyclic group < [x]>.
cyclem x n == the endomorphism y |-> y ^+ n of < [x]>.
Zp_unitm x == the isomorphism mapping the multiplicative group of the
units of the ring of integers mod # [x] to the group of
automorphisms of < [x]> (i.e., Aut < [x]>).
Zp_unitm x maps u to cyclem x u.
eltm dvd_y_x == the smallest morphism (with domain < [x]>) mapping x to
y, given a proof dvd_y_x : # [y] %| # [x].
expg_invn G k == if coprime #|G| k, the inverse of exponent k in G.
Basic results for these notions, plus the classical result that any finite
group isomorphic to a subgroup of a field is cyclic, hence that Aut G is
cyclic when G is of prime order.
Set Implicit Arguments.
Import GroupScope GRing.Theory.
Cyclic groups.
Section Cyclic.
Variable gT : finGroupType.
Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}).
Definition cyclic A := [∃ x, A == <[x]>].
Lemma cyclicP A : reflect (∃ x, A = <[x]>) (cyclic A).
Lemma cycle_cyclic x : cyclic <[x]>.
Lemma cyclic1 : cyclic [1 gT].
Isomorphism with the additive group
Section Zpm.
Variable a : gT.
Definition Zpm (i : 'Z_#[a]) := a ^+ i.
Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x × y}}.
Canonical Zpm_morphism := Morphism ZpmM.
Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>.
Lemma injm_Zpm : 'injm Zpm.
Lemma eq_expg_mod_order m n : (a ^+ m == a ^+ n) = (m == n %[mod #[a]]).
Lemma Zp_isom : isom (Zp #[a]) <[a]> Zpm.
Lemma Zp_isog : isog (Zp #[a]) <[a]>.
End Zpm.
Central and direct product of cycles
Lemma cyclic_abelian A : cyclic A → abelian A.
Lemma cycleMsub a b :
commute a b → coprime #[a] #[b] → <[a]> \subset <[a × b]>.
Lemma cycleM a b :
commute a b → coprime #[a] #[b] → <[a × b]> = <[a]> × <[b]>.
Lemma cyclicM A B :
cyclic A → cyclic B → B \subset 'C(A) → coprime #|A| #|B| →
cyclic (A × B).
Lemma cyclicY K H :
cyclic K → cyclic H → H \subset 'C(K) → coprime #|K| #|H| →
cyclic (K <*> H).
Order properties
Lemma order_dvdn a n : #[a] %| n = (a ^+ n == 1).
Lemma order_inf a n : a ^+ n.+1 == 1 → #[a] ≤ n.+1.
Lemma order_dvdG G a : a \in G → #[a] %| #|G|.
Lemma expg_cardG G a : a \in G → a ^+ #|G| = 1.
Lemma expg_znat G x k : x \in G → x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k.
Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in G → x ^+ (- k)%R = x ^- k.
Lemma nt_gen_prime G x : prime #|G| → x \in G^# → G :=: <[x]>.
Lemma nt_prime_order p x : prime p → x ^+ p = 1 → x != 1 → #[x] = p.
Lemma orderXdvd a n : #[a ^+ n] %| #[a].
Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[a] n.
Lemma orderXdiv a n : n %| #[a] → #[a ^+ n] = #[a] %/ n.
Lemma orderXexp p m n x : #[x] = (p ^ n)%N → #[x ^+ (p ^ m)] = (p ^ (n - m))%N.
Lemma orderXpfactor p k n x :
#[x ^+ (p ^ k)] = n → prime p → p %| n → #[x] = (p ^ k × n)%N.
Lemma orderXprime p n x :
#[x ^+ p] = n → prime p → p %| n → #[x] = (p × n)%N.
Lemma orderXpnat m n x : #[x ^+ m] = n → \pi(n).-nat m → #[x] = (m × n)%N.
Lemma orderM a b :
commute a b → coprime #[a] #[b] → #[a × b] = (#[a] × #[b])%N.
Definition expg_invn A k := (egcdn k #|A|).1.
Lemma expgK G k :
coprime #|G| k → {in G, cancel (expgn^~ k) (expgn^~ (expg_invn G k))}.
Lemma cyclic_dprod K H G :
K \x H = G → cyclic K → cyclic H → cyclic G = coprime #|K| #|H| .
Generator
Definition generator (A : {set gT}) a := A == <[a]>.
Lemma generator_cycle a : generator <[a]> a.
Lemma cycle_generator a x : generator <[a]> x → x \in <[a]>.
Lemma generator_order a b : generator <[a]> b → #[a] = #[b].
End Cyclic.
Implicit Arguments cyclicP [gT A].
Euler's theorem
Theorem Euler_exp_totient a n : coprime a n → a ^ totient n = 1 %[mod n].
Section Eltm.
Variables (aT rT : finGroupType) (x : aT) (y : rT).
Definition eltm of #[y] %| #[x] := fun x_i ⇒ y ^+ invm (injm_Zpm x) x_i.
Hypothesis dvd_y_x : #[y] %| #[x].
Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
Lemma eltm_id : eltm dvd_y_x x = y.
Lemma eltmM : {in <[x]> &, {morph eltm dvd_y_x : x_i x_j / x_i × x_j}}.
Canonical eltm_morphism := Morphism eltmM.
Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>.
Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>.
Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]).
End Eltm.
Section CycleSubGroup.
Variable gT : finGroupType.
Section Eltm.
Variables (aT rT : finGroupType) (x : aT) (y : rT).
Definition eltm of #[y] %| #[x] := fun x_i ⇒ y ^+ invm (injm_Zpm x) x_i.
Hypothesis dvd_y_x : #[y] %| #[x].
Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
Lemma eltm_id : eltm dvd_y_x x = y.
Lemma eltmM : {in <[x]> &, {morph eltm dvd_y_x : x_i x_j / x_i × x_j}}.
Canonical eltm_morphism := Morphism eltmM.
Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>.
Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>.
Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]).
End Eltm.
Section CycleSubGroup.
Variable gT : finGroupType.
Gorenstein, 1.3.1 (i)
Lemma cycle_sub_group (a : gT) m :
m %| #[a] →
[set H : {group gT} | H \subset <[a]> & #|H| == m]
= [set <[a ^+ (#[a] %/ m)]>%G].
Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> → H \char <[a]>.
End CycleSubGroup.
m %| #[a] →
[set H : {group gT} | H \subset <[a]> & #|H| == m]
= [set <[a ^+ (#[a] %/ m)]>%G].
Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> → H \char <[a]>.
End CycleSubGroup.
Reflected boolean property and morphic image, injection, bijection
Section MorphicImage.
Variables aT rT : finGroupType.
Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT).
Hypothesis Dx : x \in D.
Lemma morph_order : #[f x] %| #[x].
Lemma morph_generator A : generator A x → generator (f @* A) (f x).
End MorphicImage.
Section CyclicProps.
Variables gT : finGroupType.
Implicit Types (aT rT : finGroupType) (G H K : {group gT}).
Lemma cyclicS G H : H \subset G → cyclic G → cyclic H.
Lemma cyclicJ G x : cyclic (G :^ x) = cyclic G.
Lemma eq_subG_cyclic G H K :
cyclic G → H \subset G → K \subset G → (H :==: K) = (#|H| == #|K|).
Lemma cardSg_cyclic G H K :
cyclic G → H \subset G → K \subset G → (#|H| %| #|K|) = (H \subset K).
Lemma sub_cyclic_char G H : cyclic G → (H \char G) = (H \subset G).
Lemma morphim_cyclic rT G H (f : {morphism G >-> rT}) :
cyclic H → cyclic (f @* H).
Lemma quotient_cycle x H : x \in 'N(H) → <[x]> / H = <[coset H x]>.
Lemma quotient_cyclic G H : cyclic G → cyclic (G / H).
Lemma quotient_generator x G H :
x \in 'N(H) → generator G x → generator (G / H) (coset H x).
Lemma prime_cyclic G : prime #|G| → cyclic G.
Lemma dvdn_prime_cyclic G p : prime p → #|G| %| p → cyclic G.
Lemma cyclic_small G : #|G| ≤ 3 → cyclic G.
End CyclicProps.
Section IsoCyclic.
Variables gT rT : finGroupType.
Implicit Types (G H : {group gT}) (M : {group rT}).
Lemma injm_cyclic G H (f : {morphism G >-> rT}) :
'injm f → H \subset G → cyclic (f @* H) = cyclic H.
Lemma isog_cyclic G M : G \isog M → cyclic G = cyclic M.
Lemma isog_cyclic_card G M : cyclic G → isog G M = cyclic M && (#|M| == #|G|).
Lemma injm_generator G H (f : {morphism G >-> rT}) x :
'injm f → x \in G → H \subset G →
generator (f @* H) (f x) = generator H x.
End IsoCyclic.
Metacyclic groups.
Section Metacyclic.
Variable gT : finGroupType.
Implicit Types (A : {set gT}) (G H : {group gT}).
Definition metacyclic A :=
[∃ H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]].
Lemma metacyclicP A :
reflect (∃ H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)])
(metacyclic A).
Lemma metacyclic1 : metacyclic 1.
Lemma cyclic_metacyclic A : cyclic A → metacyclic A.
Lemma metacyclicS G H : H \subset G → metacyclic G → metacyclic H.
End Metacyclic.
Implicit Arguments metacyclicP [gT A].
Variable gT : finGroupType.
Implicit Types (A : {set gT}) (G H : {group gT}).
Definition metacyclic A :=
[∃ H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]].
Lemma metacyclicP A :
reflect (∃ H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)])
(metacyclic A).
Lemma metacyclic1 : metacyclic 1.
Lemma cyclic_metacyclic A : cyclic A → metacyclic A.
Lemma metacyclicS G H : H \subset G → metacyclic G → metacyclic H.
End Metacyclic.
Implicit Arguments metacyclicP [gT A].
Automorphisms of cyclic groups.
Section CyclicAutomorphism.
Variable gT : finGroupType.
Section CycleAutomorphism.
Variable a : gT.
Section CycleMorphism.
Variable n : nat.
Definition cyclem of gT := fun x : gT ⇒ x ^+ n.
Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x × y}}.
Canonical cyclem_morphism := Morphism cyclemM.
End CycleMorphism.
Section ZpUnitMorphism.
Variable u : {unit 'Z_#[a]}.
Lemma injm_cyclem : 'injm (cyclem (val u) a).
Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>.
Definition Zp_unitm := aut injm_cyclem im_cyclem.
End ZpUnitMorphism.
Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u × v}}.
Canonical Zp_unit_morphism := Morphism Zp_unitmM.
Lemma injm_Zp_unitm : 'injm Zp_unitm.
Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.
Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>.
Lemma Zp_unit_isom : isom (units_Zp #[a]) (Aut <[a]>) Zp_unitm.
Lemma Zp_unit_isog : isog (units_Zp #[a]) (Aut <[a]>).
Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a].
Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.
Lemma Aut_cycle_abelian : abelian (Aut <[a]>).
End CycleAutomorphism.
Variable G : {group gT}.
Lemma Aut_cyclic_abelian : cyclic G → abelian (Aut G).
Lemma card_Aut_cyclic : cyclic G → #|Aut G| = totient #|G|.
Lemma sum_ncycle_totient :
\sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| × totient d = #|G|.
End CyclicAutomorphism.
Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.
Section FieldMulCyclic.
Variable gT : finGroupType.
Section CycleAutomorphism.
Variable a : gT.
Section CycleMorphism.
Variable n : nat.
Definition cyclem of gT := fun x : gT ⇒ x ^+ n.
Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x × y}}.
Canonical cyclem_morphism := Morphism cyclemM.
End CycleMorphism.
Section ZpUnitMorphism.
Variable u : {unit 'Z_#[a]}.
Lemma injm_cyclem : 'injm (cyclem (val u) a).
Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>.
Definition Zp_unitm := aut injm_cyclem im_cyclem.
End ZpUnitMorphism.
Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u × v}}.
Canonical Zp_unit_morphism := Morphism Zp_unitmM.
Lemma injm_Zp_unitm : 'injm Zp_unitm.
Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.
Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>.
Lemma Zp_unit_isom : isom (units_Zp #[a]) (Aut <[a]>) Zp_unitm.
Lemma Zp_unit_isog : isog (units_Zp #[a]) (Aut <[a]>).
Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a].
Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.
Lemma Aut_cycle_abelian : abelian (Aut <[a]>).
End CycleAutomorphism.
Variable G : {group gT}.
Lemma Aut_cyclic_abelian : cyclic G → abelian (Aut G).
Lemma card_Aut_cyclic : cyclic G → #|Aut G| = totient #|G|.
Lemma sum_ncycle_totient :
\sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| × totient d = #|G|.
End CyclicAutomorphism.
Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.
Section FieldMulCyclic.
A classic application to finite multiplicative subgroups of fields.
Import GRing.Theory.
Variables (gT : finGroupType) (G : {group gT}).
Lemma order_inj_cyclic :
{in G &, ∀ x y, #[x] = #[y] → <[x]> = <[y]>} → cyclic G.
Lemma div_ring_mul_group_cyclic (R : unitRingType) (f : gT → R) :
f 1 = 1%R → {in G &, {morph f : u v / u × v >-> (u × v)%R}} →
{in G^#, ∀ x, f x - 1 \in GRing.unit}%R →
abelian G → cyclic G.
Lemma field_mul_group_cyclic (F : fieldType) (f : gT → F) :
{in G &, {morph f : u v / u × v >-> (u × v)%R}} →
{in G, ∀ x, f x = 1%R ↔ x = 1} →
cyclic G.
End FieldMulCyclic.
Lemma field_unit_group_cyclic (F : finFieldType) (G : {group {unit F}}) :
cyclic G.
Section PrimitiveRoots.
Open Scope ring_scope.
Import GRing.Theory.
Lemma has_prim_root (F : fieldType) (n : nat) (rs : seq F) :
n > 0 → all n.-unity_root rs → uniq rs → size rs ≥ n →
has n.-primitive_root rs.
End PrimitiveRoots.
Cycles of prime order