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
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
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_iy ^+ 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 : gTx ^+ 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