- -

Library mathcomp.solvable.cyclic

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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.
- -
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
- -
-

- -

- 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.
- -
-

- -

- 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 -

- -
-Section AutPrime.
- -
-Variable gT : finGroupType.
- -
-Lemma Aut_prime_cycle_cyclic (a : gT) : prime #[a ] → cyclic (Aut <[a ]>).
- -
-Lemma Aut_prime_cyclic (G : {group gT }) : prime #|G | → cyclic (Aut G).
- -
-End AutPrime.
-