Library mathcomp.solvable.cyclic
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice div.
From mathcomp Require Import fintype bigop prime finset fingroup morphism.
From mathcomp Require Import perm automorphism quotient gproduct ssralg.
From mathcomp Require Import finalg zmodp poly.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice div.
From mathcomp Require Import fintype bigop prime finset fingroup morphism.
From mathcomp Require Import perm automorphism quotient gproduct ssralg.
From mathcomp Require Import finalg zmodp poly.
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.
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.
Arguments cyclic {gT} A%g.
Arguments generator {gT} A%g a%g.
Arguments expg_invn {gT} A%g k%N.
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.
Arguments metacyclic {gT} A%g.
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.
Arguments metacyclic {gT} A%g.
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.
Lemma units_Zp_cyclic p : prime p → cyclic (units_Zp p).
Section PrimitiveRoots.
Open Scope ring_scope.
Import GRing.Theory.
This subproof has been extracted out of [has_prim_root] for performance reasons.
See github PR #1059 for further documentation and investigation on this problem.
Lemma has_prim_root_subproof (F : fieldType) (n : nat) (rs : seq F)
(n_gt0 : n > 0)
(rsn1 : all n.-unity_root rs)
(Urs : uniq rs)
(sz_rs : size rs = n)
(r := fun s ⇒ val (s : seq_sub rs))
(rn1 : ∀ x : seq_sub rs, r x ^+ n = 1)
(prim_r : ∀ z : F, z ^+ n = 1 → z \in rs)
(r' := (fun s (e : s ^+ n = 1) ⇒ {| ssval := s; ssvalP := prim_r s e |})
: ∀ s : F, s ^+ n = 1 → seq_sub rs)
(sG_1 := r' 1 (expr1n F n) : seq_sub rs)
(sG_VP : ∀ s : seq_sub rs, r s ^+ n.-1 ^+ n = 1)
(sG_MP : ∀ s s0 : seq_sub rs, (r s × r s0) ^+ n = 1)
(sG_V := (fun s : seq_sub rs ⇒ r' (r s ^+ n.-1) (sG_VP s))
: seq_sub rs → seq_sub rs)
(sG_M := (fun s s0 : seq_sub rs ⇒ r' (r s × r s0) (sG_MP s s0))
: seq_sub rs → seq_sub rs → seq_sub rs)
(sG_Ag : associative sG_M)
(sG_1g : left_id sG_1 sG_M)
(sG_Vg : left_inverse sG_1 sG_V sG_M) :
has n.-primitive_root rs.
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.
(n_gt0 : n > 0)
(rsn1 : all n.-unity_root rs)
(Urs : uniq rs)
(sz_rs : size rs = n)
(r := fun s ⇒ val (s : seq_sub rs))
(rn1 : ∀ x : seq_sub rs, r x ^+ n = 1)
(prim_r : ∀ z : F, z ^+ n = 1 → z \in rs)
(r' := (fun s (e : s ^+ n = 1) ⇒ {| ssval := s; ssvalP := prim_r s e |})
: ∀ s : F, s ^+ n = 1 → seq_sub rs)
(sG_1 := r' 1 (expr1n F n) : seq_sub rs)
(sG_VP : ∀ s : seq_sub rs, r s ^+ n.-1 ^+ n = 1)
(sG_MP : ∀ s s0 : seq_sub rs, (r s × r s0) ^+ n = 1)
(sG_V := (fun s : seq_sub rs ⇒ r' (r s ^+ n.-1) (sG_VP s))
: seq_sub rs → seq_sub rs)
(sG_M := (fun s s0 : seq_sub rs ⇒ r' (r s × r s0) (sG_MP s s0))
: seq_sub rs → seq_sub rs → seq_sub rs)
(sG_Ag : associative sG_M)
(sG_1g : left_id sG_1 sG_M)
(sG_Vg : left_inverse sG_1 sG_V sG_M) :
has n.-primitive_root rs.
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