(Joint Center)Library MathComp.cyclic

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype bigop.
Require Import prime finset fingroup morphism perm automorphism quotient.
Require Import gproduct ssralg 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.

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

Lemma cycleMsub a b :
  commute a bcoprime #[a] #[b]<[a]> \subset <[a × b]>.

Lemma cycleM a b :
  commute a bcoprime #[a] #[b]<[a × b]> = <[a]> × <[b]>.

Lemma cyclicM A B :
    cyclic Acyclic BB \subset 'C(A)coprime #|A| #|B|
  cyclic (A × B).

Lemma cyclicY K H :
    cyclic Kcyclic HH \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 Ga ^+ #|G| = 1.

Lemma expg_znat G x k : x \in Gx ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k.

Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in Gx ^+ (- k)%R = x ^- k.

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

Lemma nt_prime_order p x : prime px ^+ 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)] = nprime pp %| n#[x] = (p ^ k × n)%N.

Lemma orderXprime p n x :
  #[x ^+ p] = nprime pp %| 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 bcoprime #[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 = Gcyclic Kcyclic Hcyclic 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]> xx \in <[a]>.

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

End Cyclic.

Implicit Arguments cyclicP [gT A].

Euler's theorem
Theorem Euler_exp_totient a n : coprime a na ^ 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 xgenerator (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 Gcyclic Gcyclic H.

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

Lemma eq_subG_cyclic G H K :
  cyclic GH \subset GK \subset G(H :==: K) = (#|H| == #|K|).

Lemma cardSg_cyclic G H K :
  cyclic GH \subset GK \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 Hcyclic (f @* H).

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

Lemma quotient_cyclic G H : cyclic Gcyclic (G / H).

Lemma quotient_generator x G H :
  x \in 'N(H)generator G xgenerator (G / H) (coset H x).

Lemma prime_cyclic G : prime #|G|cyclic G.

Lemma dvdn_prime_cyclic G p : prime p#|G| %| pcyclic 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 fH \subset Gcyclic (f @* H) = cyclic H.

Lemma isog_cyclic G M : G \isog Mcyclic G = cyclic M.

Lemma isog_cyclic_card G M : cyclic Gisog G M = cyclic M && (#|M| == #|G|).

Lemma injm_generator G H (f : {morphism G >-> rT}) x :
    'injm fx \in GH \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 Ametacyclic A.

Lemma metacyclicS G H : H \subset Gmetacyclic Gmetacyclic 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 : 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 Gabelian (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 : gTR) :
    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 Gcyclic G.

Lemma field_mul_group_cyclic (F : fieldType) (f : gTF) :
    {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 rsuniq rssize 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.