# Library mathcomp.field.algnum

(* (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 path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg finalg zmodp poly ssrnum ssrint rat.
From mathcomp Require Import polydiv intdiv algC matrix mxalgebra mxpoly.
From mathcomp Require Import vector falgebra fieldext separable galois.
From mathcomp Require Import 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 coefficients. (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_ZtoC : core.

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_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.
Integral spans.
Automorphism extensions.
Extended automorphisms of Q_n.
Algebraic integers.

Definition Aint : {pred algC} := fun xminCpoly 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 : core.

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).
This is Isaacs, Corollary (3.5).
Corollary Aint_subring : subring_closed Aint.
Canonical Aint_opprPred := OpprPred 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 algC} :=
fun zif 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_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 : core.

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 : core.

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).