Library cyclic

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
 Properties of cyclic groups                                        
Definitions:                                                        
Defined in groups.v:                                                
  <[x]>         == the cycle (cyclic group) generated by x          
  #[x]          == the order of x, i.e., the cardinal of <[x]>.     
Defined in phi.v:                                                   
  phi n         == Euler's totient function                         
In this file:                                                       
  cyclic G      <=> G is a cyclic group.                            
  generator G x <=> x is a generator of the (cyclic) group G.       
  Zpm x         == the isomorphism between the additive group of    
                   integers mod #[x], and the group <[x]>           
  cyclem x n    == the endomorphism y |-> y ^+ n of <[x]>           
  Zp_unitm x    == the isomorphism from the multiplicative group of 
                   the units of the ring of integers mod #[x], with 
                   the group Aut <[x]> of automorphisms of <[x]>.   
                   (Zp_unitm x map u to cyclem x u)                 
Basic results for these notions, plus the classical result that     
any finite group isomorphic to a subggroup of a field is cycle,     
and the corollary that Aut G is cyclic when G is of prime order.    

Import Prenex Implicits.

Import GroupScope.

 Cyclic groups.                                                     

Section Cyclic.

Variable gT : finGroupType.
Implicit Types a x y : gT.
Implicit Types A B : {set gT}.
Implicit Types G H : {group gT}.

Definition cyclic A := existsb x, A == <[x]>.

Lemma cyclicP : forall A, reflect (exists x, A = <[x]>) (cyclic A).

Lemma cycle_cyclic : forall x, cyclic <[x]>.

Lemma cyclic1 : cyclic [1 gT].

Isomorphism with the additive group                                 

Section Zpm.

Variable a : gT.

Definition Zpm (i : 'I_#[a]) := a ^+ i.

Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x * y}}.

Canonical Structure Zpm_morphism := Morphism ZpmM.

Lemma morphim_Zpm : Zpm @* Zp #[a] = <[a]>.

Lemma Zpm_inj : injective Zpm.

Lemma injm_Zpm : 'injm Zpm.

Lemma eq_expg_mod_order : forall 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]>.

Lemma cycle_decomp : forall b,
  b \in <[a]> -> {m : nat | m < #[a] & a ^+ m = b}.

End Zpm.

       Central and direct product of cycles                         

Lemma cents_cycle : forall a b, commute a b -> <[a]> \subset 'C(<[b]>).

Lemma cycle_abelian : forall a, abelian <[a]>.

Lemma cyclic_abelian : forall A, cyclic A -> abelian A.

Lemma cycleMsub : forall a b,
  commute a b -> coprime #[a] #[b] -> <[a]> \subset <[a * b]>.

Lemma cycleM : forall a b,
  commute a b -> coprime #[a] #[b] -> <[a * b]> = <[a]> * <[b]>.

       Order properties                                             

Lemma order_dvdn : forall a n, (#[a] %| n) = (a ^+ n == 1).

Lemma order_inf : forall a n, a ^+ n.+1 == 1 -> #[a] <= n.+1.

Lemma order_eq1 : forall a, (#[a] == 1%N) = (a == 1).

Lemma cycle_eq1 : forall a, (<[a]> == 1) = (a == 1).

Lemma order_dvdG : forall (G : {group gT}) a, a \in G -> #[a] %| #|G|.

Lemma orderXdvd : forall a n, #[a ^+ n] %| #[a].

Lemma orderXgcd : forall a n, #[a ^+ n] = #[a] %/ gcdn #[a] n.

Lemma orderXdiv : forall a n, n %| #[a] -> #[a ^+ n] = #[a] %/ n.

Lemma orderM : forall a b : gT,
  commute a b -> coprime #[a] #[b] -> #[a * b] = (#[a] * #[b])%N.

       Generator                                                    

Definition generator (A : {set gT}) a := A == <[a]>.

Lemma generator_cycle : forall a, generator <[a]> a.

Lemma cycle_generator : forall a x, generator <[a]> x -> x \in <[a]>.

Lemma generator_order : forall a b,
  generator <[a]> b -> #[a] = #[b].

End Cyclic.

Euler's theorem 

Theorem Euler: forall a n, coprime a n -> a ^ phi n = 1 %[mod n].

Section CyclicSubGroup.

Variable gT : finGroupType.

 G. 1.3.1 (i) 

Lemma cycle_sub_group : forall (a : gT) m, m %| #[a] ->
  [set H : {group gT} | (H \subset <[a]>) && (#|H| == m)]
     = [set <[a ^+ (#[a] %/ m)]>%G].

Lemma cycle_subgroup_char : forall a (H : {group gT}),
  H \subset <[a]> -> H \char <[a]>.

End CyclicSubGroup.

 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 morphim_cycle : f @* <[x]> = <[f x]>.

Lemma morph_order : #[f x] %| #[x].

Lemma morph_generator : forall A, generator A x -> generator (f @* A) (f x).

End MorphicImage.

Section CyclicProps.

Variables gT : finGroupType.
Implicit Types G H K : {group gT}.
Implicit Types aT rT : finGroupType.

Lemma cyclicS : forall G H, H \subset G -> cyclic G -> cyclic H.

Lemma cyclicJ: forall G x, cyclic (G :^ x) = cyclic G.

Lemma morphim_cyclic : forall rT G H (f : {morphism G >-> rT}),
  cyclic H -> cyclic (f @* H).

Lemma quotient_cycle : forall x H, x \in 'N(H) -> <[x]> / H = <[coset H x]>.

Lemma quotient_cyclic : forall G H, cyclic G -> cyclic (G / H).

Lemma quotient_generator : forall x G H,
  x \in 'N(H) -> generator G x -> generator (G / H) (coset H x).

Lemma prime_cyclic : forall G, prime #|G| -> cyclic G.

Lemma cyclic_small : forall G, #|G| <= 3 -> cyclic G.

End CyclicProps.

Section IsoCyclic.

Variables gT rT : finGroupType.
Implicit Types G H : {group gT}.
Implicit Types M : {group rT}.

Lemma injm_cyclic : forall G H (f : {morphism G >-> rT}),
  'injm f -> H \subset G -> cyclic (f @* H) = cyclic H.

Lemma isog_cyclic :forall G M, G \isog M -> cyclic G = cyclic M.

Lemma isog_cyclic_card : forall G M,
  cyclic G -> isog G M = cyclic M && (#|M| == #|G|).

Lemma injm_generator : forall 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.

      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 Structure cyclem_morphism := Morphism cyclemM.

End CycleMorphism.

Section ZpUnitMorphism.

Variable u : Zp_unit #[a].

Lemma injm_cyclem : 'injm (cyclem u a).

Lemma cyclem_dom : cyclem u a @* <[a]> = <[a]>.

Definition Zp_unitm := aut injm_cyclem cyclem_dom.

End ZpUnitMorphism.

Lemma Zp_unitmM : {in Zp_units #[a] &, {morph Zp_unitm : u v / u * v}}.

Canonical Structure Zp_unit_morphism := Morphism Zp_unitmM.

Lemma injm_Zp_unitm : 'injm Zp_unitm.

Lemma generator_coprime : forall m, generator <[a]> (a ^+ m) = coprime #[a] m.

Lemma morphim_Zp_unitm : Zp_unitm @* Zp_units #[a] = Aut <[a]>.

Lemma Zp_unit_isom : isom (Zp_units #[a]) (Aut <[a]>) Zp_unitm.

Lemma Zp_unit_isog : isog (Zp_units #[a]) (Aut <[a]>).

Lemma card_Aut_cycle : #|Aut <[a]>| = phi #[a].

Lemma phi_gen : phi #[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| = phi #|G|.

Lemma sum_ncycle_phi :
  \sum_(d < #|G|.+1) #|[set <[x]> | x <- G, #[x] == d]| * phi d = #|G|.

End CyclicAutomorphism.

Lemma sum_phi_dvd : forall n, \sum_(d < n.+1 | d %| n) phi 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 &, forall x y, #[x] = #[y] -> <[x]> = <[y]>} -> cyclic G.

Lemma div_ring_mul_group_cyclic : forall (R : unitRingType) (f : gT -> R),
    f 1 = 1%R -> {in G &, {morph f : u v / u * v >-> (u * v)%R}} ->
    {in G^#, forall x, GRing.unit (f x - 1)%R} ->
  abelian G -> cyclic G.

Lemma field_mul_group_cyclic : forall (F : fieldType) (f : gT -> F),
    {in G &, {morph f : u v / u * v >-> (u * v)%R}} ->
    {in G, forall x, f x = 1%R <-> x = 1} ->
  cyclic G.

End FieldMulCyclic.

 Cycles of prime order                                              

Section AutPrime.

Variable gT : finGroupType.

Lemma Aut_prime_cycle_cyclic : forall a : gT, prime #[a] -> cyclic (Aut <[a]>).

Lemma Aut_prime_cyclic : forall G : {group gT}, prime #|G| -> cyclic (Aut G).

End AutPrime.