(Joint Center)Library MathComp.algnum

(* (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 finalg zmodp poly.
Require Import ssrnum ssrint rat polydiv intdiv algC matrix mxalgebra mxpoly.
Require Import vector falgebra fieldext separable galois cyclotomic.

This file provides a few basic results and constructions in algebraic number theory, that are used in the character theory library. Most of these could be generalized to a more abstract setting. Note that the type of abstract number fields is simply extFieldType rat. We define here: x \in Crat_span X <=> x is a Q-linear combination of elements of X : seq algC. x \in Cint_span X <=> x is a Z-linear combination of elements of X : seq algC. x \in Aint <=> x : algC is an algebraic integer, i.e., the (monic) polynomial of x over Q has integer coeficients. (e %| a)%A <=> e divides a with respect to algebraic integers, (e %| a)%Ax i.e., a is in the algebraic integer ideal generated by e. This is is notation for a \in dvdA e, where dvdv is the (collective) predicate for the Aint ideal generated by e. As in the (e %| a)%C notation e and a can be coerced to algC from nat or int. The (e %| a)%Ax display form is a workaround for design limitations of the Coq Notation facilities. (a == b % [mod e])%A, (a != b % [mod e])%A <=> a is equal (resp. not equal) to b mod e, i.e., a and b belong to the same e * Aint class. We do not force a, b and e to be algebraic integers. # [x]%C == the multiplicative order of x, i.e., the n such that x is an nth primitive root of unity, or 0 if x is not a root of unity. In addition several lemmas prove the (constructive) existence of number fields and of automorphisms of algC.

Set Implicit Arguments.

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

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 _ : injective ZtoC).
Local Notation QtoCm := [rmorphism of QtoC].

Number fields and rational spans.
Lemma algC_PET (s : seq algC) :
  {z | a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i
     & ps, s = [seq (pQtoC p).[z] | p <- ps]}.

Canonical subfx_unitAlgType (F L : fieldType) iota (z : L) p :=
  Eval hnf in [unitAlgType F of subFExtend iota z p].

Lemma num_field_exists (s : seq algC) :
  {Qs : fieldExtType rat & {QsC : {rmorphism QsalgC}
   & {s1 : seq Qs | map QsC s1 = s & <<1 & s1>>%VS = fullv}}}.

Definition in_Crat_span s x :=
   a : rat ^ size s, x = \sum_i QtoC (a i) × s`_i.

Fact Crat_span_subproof s x : decidable (in_Crat_span s x).

Definition Crat_span s : pred algC := Crat_span_subproof s.
Lemma Crat_spanP s x : reflect (in_Crat_span s x) (x \in Crat_span s).
Fact Crat_span_key s : pred_key (Crat_span s).
Canonical Crat_span_keyed s := KeyedPred (Crat_span_key s).

Lemma mem_Crat_span s : {subset s Crat_span s}.

Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s).
Canonical Crat_span_opprPred s := OpprPred (Crat_span_zmod_closed s).
Canonical Crat_span_addrPred s := AddrPred (Crat_span_zmod_closed s).
Canonical Crat_span_zmodPred s := ZmodPred (Crat_span_zmod_closed s).

Section MoreAlgCaut.

Implicit Type rR : unitRingType.

Lemma alg_num_field (Qz : fieldExtType rat) a : a%:A = ratr a :> Qz.

Lemma rmorphZ_num (Qz : fieldExtType rat) rR (f : {rmorphism QzrR}) a x :
  f (a *: x) = ratr a × f x.

Lemma fmorph_numZ (Qz1 Qz2 : fieldExtType rat) (f : {rmorphism Qz1Qz2}) :
  scalable f.
Definition NumLRmorphism Qz1 Qz2 f := AddLRMorphism (@fmorph_numZ Qz1 Qz2 f).

End MoreAlgCaut.

Section NumFieldProj.

Variables (Qn : fieldExtType rat) (QnC : {rmorphism QnalgC}).

Lemma Crat_spanZ b a : {in Crat_span b, x, ratr a × x \in Crat_span b}.

Lemma Crat_spanM b : {in Crat & Crat_span b, a x, a × x \in Crat_span b}.

In principle CtoQn could be taken to be additive and Q-linear, but this would require a limit construction.
Lemma num_field_proj : {CtoQn | CtoQn 0 = 0 & cancel QnC CtoQn}.

Lemma restrict_aut_to_num_field (nu : {rmorphism algCalgC}) :
    ( x, y, nu (QnC x) = QnC y) →
  {nu0 : {lrmorphism QnQn} | {morph QnC : x / nu0 x >-> nu x}}.

Lemma map_Qnum_poly (nu : {rmorphism algCalgC}) p :
  p \in polyOver 1%VSmap_poly (nu \o QnC) p = (map_poly QnC p).

End NumFieldProj.

Lemma restrict_aut_to_normal_num_field (Qn : splittingFieldType rat)
  (QnC : {rmorphism QnalgC})(nu : {rmorphism algCalgC}) :
    {nu0 : {lrmorphism QnQn} | {morph QnC : x / nu0 x >-> nu x}}.

Integral spans.

Lemma dec_Cint_span (V : vectType algC) m (s : m.-tuple V) v :
  decidable (inIntSpan s v).

Definition Cint_span (s : seq algC) : pred algC :=
  fun xdec_Cint_span (in_tuple [seq \row_(i < 1) y | y <- s]) (\row_i x).
Fact Cint_span_key s : pred_key (Cint_span s).
Canonical Cint_span_keyed s := KeyedPred (Cint_span_key s).

Lemma Cint_spanP n (s : n.-tuple algC) x :
  reflect (inIntSpan s x) (x \in Cint_span s).

Lemma mem_Cint_span s : {subset s Cint_span s}.

Lemma Cint_span_zmod_closed s : zmod_closed (Cint_span s).
Canonical Cint_span_opprPred s := OpprPred (Cint_span_zmod_closed s).
Canonical Cint_span_addrPred s := AddrPred (Cint_span_zmod_closed s).
Canonical Cint_span_zmodPred s := ZmodPred (Cint_span_zmod_closed s).

Automorphism extensions.
Lemma extend_algC_subfield_aut (Qs : fieldExtType rat)
  (QsC : {rmorphism QsalgC}) (phi : {rmorphism QsQs}) :
  {nu : {rmorphism algCalgC} | {morph QsC : x / phi x >-> nu x}}.

Extended automorphisms of Q_n.
Lemma Qn_aut_exists k n :
    coprime k n
  {u : {rmorphism algCalgC} | z, z ^+ n = 1 → u z = z ^+ k}.

Algebraic integers.

Definition Aint : pred_class :=
  fun x : algCminCpoly x \is a polyOver Cint.
Fact Aint_key : pred_key Aint.
Canonical Aint_keyed := KeyedPred Aint_key.

Lemma root_monic_Aint p x :
  root p xp \is monicp \is a polyOver Cintx \in Aint.

Lemma Cint_rat_Aint z : z \in Cratz \in Aintz \in Cint.

Lemma Aint_Cint : {subset Cint Aint}.

Lemma Aint_int x : x%:~R \in Aint.

Lemma Aint0 : 0 \in Aint.
Lemma Aint1 : 1 \in Aint.
Hint Resolve Aint0 Aint1.

Lemma Aint_unity_root n x : (n > 0)%Nn.-unity_root xx \in Aint.

Lemma Aint_prim_root n z : n.-primitive_root zz \in Aint.

Lemma Aint_Cnat : {subset Cnat Aint}.

This is Isaacs, Lemma (3.3)
Lemma Aint_subring_exists (X : seq algC) :
    {subset X Aint}
  {S : pred algC &
     (*a*) subring_closed S
   (*b*) {subset X S}
   & (*c*) {Y : {n : nat & n.-tuple algC} &
                {subset tagged Y S}
              & x, reflect (inIntSpan (tagged Y) x) (x \in S)}}.

Section AlgIntSubring.

Import DefaultKeying GRing.DefaultPred perm.

This is Isaacs, Theorem (3.4).
Theorem fin_Csubring_Aint S n (Y : n.-tuple algC) :
     mulr_closed S → ( x, reflect (inIntSpan Y x) (x \in S)) →
  {subset S Aint}.

This is Isaacs, Corollary (3.5).
Corollary Aint_subring : subring_closed Aint.
Canonical Aint_opprPred := OpprPred Aint_subring.
Canonical Aint_addrPred := AddrPred Aint_subring.
Canonical Aint_mulrPred := MulrPred Aint_subring.
Canonical Aint_zmodPred := ZmodPred Aint_subring.
Canonical Aint_semiringPred := SemiringPred Aint_subring.
Canonical Aint_smulrPred := SmulrPred Aint_subring.
Canonical Aint_subringPred := SubringPred Aint_subring.

End AlgIntSubring.

Lemma Aint_aut (nu : {rmorphism algCalgC}) x :
  (nu x \in Aint) = (x \in Aint).

Definition dvdA (e : Algebraics.divisor) : pred_class :=
  fun z : algCif e == 0 then z == 0 else z / e \in Aint.
Fact dvdA_key e : pred_key (dvdA e).
Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
Delimit Scope algC_scope with A.
Delimit Scope algC_expanded_scope with Ax.
Notation "e %| x" := (x \in dvdA e) : algC_expanded_scope.
Notation "e %| x" := (@in_mem Algebraics.divisor x (mem (dvdA e))) : algC_scope.

Fact dvdA_zmod_closed e : zmod_closed (dvdA e).
Canonical dvdA_opprPred e := OpprPred (dvdA_zmod_closed e).
Canonical dvdA_addrPred e := AddrPred (dvdA_zmod_closed e).
Canonical dvdA_zmodPred e := ZmodPred (dvdA_zmod_closed e).

Definition eqAmod (e x y : Algebraics.divisor) := (e %| x - y)%A.
Notation "x == y %[mod e ]" := (eqAmod e x y) : algC_scope.
Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope.

Lemma eqAmod_refl e x : (x == x %[mod e])%A.
Hint Resolve eqAmod_refl.

Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A.

Lemma eqAmod_trans e y x z :
  (x == y %[mod e]y == z %[mod e]x == z %[mod e])%A.

Lemma eqAmod_transl e x y z :
  (x == y %[mod e])%A → (x == z %[mod e])%A = (y == z %[mod e])%A.

Lemma eqAmod_transr e x y z :
  (x == y %[mod e])%A → (z == x %[mod e])%A = (z == y %[mod e])%A.

Lemma eqAmod0 e x : (x == 0 %[mod e])%A = (e %| x)%A.

Lemma eqAmodN e x y : (- x == y %[mod e])%A = (x == - y %[mod e])%A.

Lemma eqAmodDr e x y z : (y + x == z + x %[mod e])%A = (y == z %[mod e])%A.

Lemma eqAmodDl e x y z : (x + y == x + z %[mod e])%A = (y == z %[mod e])%A.

Lemma eqAmodD e x1 x2 y1 y2 :
  (x1 == x2 %[mod e]y1 == y2 %[mod e]x1 + y1 == x2 + y2 %[mod e])%A.

Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
Hint Resolve eqAmodm0.

Lemma eqAmodMr e :
  {in Aint, z x y, x == y %[mod e]x × z == y × z %[mod e]}%A.

Lemma eqAmodMl e :
  {in Aint, z x y, x == y %[mod e]z × x == z × y %[mod e]}%A.

Lemma eqAmodMl0 e : {in Aint, x, x × e == 0 %[mod e]}%A.

Lemma eqAmodMr0 e : {in Aint, x, e × x == 0 %[mod e]}%A.

Lemma eqAmod_addl_mul e : {in Aint, x y, x × e + y == y %[mod e]}%A.

Lemma eqAmodM e : {in Aint &, x1 y2 x2 y1,
  x1 == x2 %[mod e]y1 == y2 %[mod e]x1 × y1 == x2 × y2 %[mod e]}%A.

Lemma eqAmod_rat :
  {in Crat & &, e m n, (m == n %[mod e])%A = (m == n %[mod e])%C}.

Lemma eqAmod0_rat : {in Crat &, e n, (n == 0 %[mod e])%A = (e %| n)%C}.

Lemma eqAmod_nat (e m n : nat) : (m == n %[mod e])%A = (m == n %[mod e])%N.

Lemma eqAmod0_nat (e m : nat) : (m == 0 %[mod e])%A = (e %| m)%N.

Multiplicative order.

Definition orderC x :=
  let p := minCpoly x in
  oapp val 0%N [pick n : 'I_(2 × size p ^ 2) | p == intrp 'Phi_n].

Notation "#[ x ]" := (orderC x) : C_scope.

Lemma exp_orderC x : x ^+ #[x]%C = 1.

Lemma dvdn_orderC x n : (#[x]%C %| n)%N = (x ^+ n == 1).