Library cyclic

  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:                                                        
           phi 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].                
   expgn_inv 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.                                           


Import GroupScope GRing.Theory.

  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 : 'Z_#[a]) := a ^+ i.

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

Canonical Structure Zpm_morphism := Morphism ZpmM.

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

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

End Zpm.

        Central and direct product of cycles                         

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_dvdG : forall G a, a \in G -> #[a] %| #|G|.

Lemma expgn_znat : forall G x k, x \in G -> x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k.

Lemma expgn_zneg : forall G x (k : 'Z_(#|G|)), x \in G -> x ^+ (- k)%R = x ^- k.

Lemma nt_gen_prime : forall G x, prime #|G| -> x \in G^# -> G :=: <[x]>.

Lemma nt_prime_order : forall p x, prime p -> x ^+ p = 1 -> x != 1 -> #[x] = p.

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 orderXexp : forall p m n x,
  #[x] = (p ^ n)%N -> #[x ^+ (p ^ m)] = (p ^ (n - m))%N.

Lemma orderXpfactor : forall p k n x,
  #[x ^+ (p ^ k)] = n -> prime p -> p %| n -> #[x] = (p ^ k * n)%N.

Lemma orderXprime : forall p n x,
  #[x ^+ p] = n -> prime p -> p %| n -> #[x] = (p * n)%N.

Lemma orderXpnat : forall m n x,
  #[x ^+ m] = n -> \pi(n).-nat m -> #[x] = (m * n)%N.

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

Definition expgn_inv A k := (egcdn k #|A|).1.

Lemma expgnK : forall G k,
  coprime #|G| k -> {in G, cancel (expgn^~ k) (expgn^~ (expgn_inv G k))}.

        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.

Implicit Arguments cyclicP [gT A].

 Euler's theorem 
Theorem Euler : forall a n, coprime a n -> a ^ phi 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 : forall 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 Structure 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 : 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 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 : 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 eq_subG_cyclic : forall G H K,
  cyclic G -> H \subset G -> K \subset G -> (H :==: K) = (#|H| == #|K|).

Lemma cardSg_cyclic : forall G H K,
  cyclic G -> H \subset G -> K \subset G -> (#|H| %| #|K|) = (H \subset K).

Lemma sub_cyclic_char : forall G H, cyclic G -> (H \char G) = (H \subset 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 dvdn_prime_cyclic : forall G p, prime p -> #|G| %| p -> 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.

 Metacyclic groups. 
Section Metacyclic.

Variable gT : finGroupType.
Implicit Type A : {set gT}.
Implicit Types G H : {group gT}.

Definition metacyclic A :=
  existsb H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)].

Lemma metacyclicP : forall A,
  reflect (exists H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)])
          (metacyclic A).

Lemma metacyclic1 : metacyclic 1.

Lemma cyclic_metacyclic : forall A, cyclic A -> metacyclic A.

Lemma metacyclicN : forall G H, metacyclic G -> H <| 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 Structure 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 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 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]>| = 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.

Section PrimitiveRoots.

Open Scope ring_scope.
Import GRing.Theory.

Lemma has_prim_root : forall (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 : forall a : gT, prime #[a] -> cyclic (Aut <[a]>).

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

End AutPrime.