Library mathcomp.field.algnum

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

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 Hint Resolve (@intr_inj _ : injective ZtoC).

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 Qs algC}
   & {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 Qz rR}) a x :
  f (a *: x) = ratr a × f x.

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

End MoreAlgCaut.

Section NumFieldProj.

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

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 algC algC}) :
    ( x, y, nu (QnC x) = QnC y)
  {nu0 : {lrmorphism Qn Qn} | {morph QnC : x / nu0 x >-> nu x}}.

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

End NumFieldProj.

Lemma restrict_aut_to_normal_num_field (Qn : splittingFieldType rat)
  (QnC : {rmorphism Qn algC})(nu : {rmorphism algC algC}) :
    {nu0 : {lrmorphism Qn Qn} | {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.
Extended automorphisms of Q_n.
Lemma Qn_aut_exists k n :
    coprime k n
  {u : {rmorphism algC algC} | 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 x p \is monic p \is a polyOver Cint x \in Aint.

Lemma Cint_rat_Aint z : z \in Crat z \in Aint z \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)%N n.-unity_root x x \in Aint.

Lemma Aint_prim_root n z : n.-primitive_root z z \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 algC algC}) 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).