(Joint Center)Library MathComp.cyclotomic

(* (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 path div choice.
Require Import fintype tuple finfun bigop prime ssralg poly finset.
Require Import fingroup finalg zmodp cyclic.
Require Import ssrnum ssrint polydiv rat intdiv.
Require Import mxpoly vector falgebra fieldext separable galois algC.

This file provides few basic properties of cyclotomic polynomials. We define: cyclotomic z n == the factorization of the nth cyclotomic polynomial in a ring R in which z is an nth primitive root of unity. 'Phi_n == the nth cyclotomic polynomial in int. This library is quite limited, and should be extended in the future. In particular the irreducibity of 'Phi_n is only stated indirectly, as the fact that its embedding in the algebraics (algC) is the minimal polynomial of an nth primitive root of unity.

Set Implicit Arguments.

Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Section CyclotomicPoly.

Section Ring.

Variable R : ringType.

Definition cyclotomic (z : R) n :=
  \prod_(k < n | coprime k n) ('X - (z ^+ k)%:P).

Lemma cyclotomic_monic z n : cyclotomic z n \is monic.

Lemma size_cyclotomic z n : size (cyclotomic z n) = (totient n).+1.

End Ring.

Lemma separable_Xn_sub_1 (R : idomainType) n :
  n%:R != 0 :> R → @separable_poly R ('X^n - 1).

Section Field.

Variables (F : fieldType) (n : nat) (z : F).
Hypothesis prim_z : n.-primitive_root z.
Let n_gt0 := prim_order_gt0 prim_z.

Lemma root_cyclotomic x : root (cyclotomic z n) x = n.-primitive_root x.

Lemma prod_cyclotomic :
  'X^n - 1 = \prod_(d <- divisors n) cyclotomic (z ^+ (n %/ d)) d.

End Field.

End CyclotomicPoly.

Local Notation ZtoQ := (intr : intrat).
Local Notation ZtoC := (intr : intalgC).
Local Notation QtoC := (ratr : ratalgC).

Local Notation intrp := (map_poly intr).
Local Notation pZtoQ := (map_poly ZtoQ).
Local Notation pZtoC := (map_poly ZtoC).
Local Notation pQtoC := (map_poly ratr).

Local Hint Resolve (@intr_inj [numDomainType of algC]).
Local Notation QtoC_M := (ratr_rmorphism [numFieldType of algC]).

Lemma C_prim_root_exists n : (n > 0)%N{z : algC | n.-primitive_root z}.

(Integral) Cyclotomic polynomials.

Definition Cyclotomic n : {poly int} :=
  let: exist z _ := C_prim_root_exists (ltn0Sn n.-1) in
  map_poly floorC (cyclotomic z n).

Notation "''Phi_' n" := (Cyclotomic n)
  (at level 8, n at level 2, format "''Phi_' n").

Lemma Cyclotomic_monic n : 'Phi_n \is monic.

Lemma Cintr_Cyclotomic n z :
  n.-primitive_root zpZtoC 'Phi_n = cyclotomic z n.

Lemma prod_Cyclotomic n :
  (n > 0)%N\prod_(d <- divisors n) 'Phi_d = 'X^n - 1.

Lemma Cyclotomic0 : 'Phi_0 = 1.

Lemma size_Cyclotomic n : size 'Phi_n = (totient n).+1.

Lemma minCpoly_cyclotomic n z :
  n.-primitive_root zminCpoly z = cyclotomic z n.