Library mathcomp.solvable.cyclic

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import fintype bigop prime finset fingroup morphism.
From mathcomp Require Import perm automorphism quotient gproduct ssralg.
From mathcomp Require Import 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 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.

Arguments cyclic {gT} A%g.
Arguments generator {gT} A%g a%g.
Arguments expg_invn {gT} A%g k%N.
Arguments cyclicP {gT A}.

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.

Arguments metacyclic {gT} A%g.
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 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.