# Library mathcomp.field.algnum

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

From HB Require Import structures.
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 poly polydiv ssrnum ssrint archimedean rat.
From mathcomp Require Import finalg zmodp matrix mxalgebra mxpoly vector intdiv.
From mathcomp Require Import falgebra fieldext separable galois algC 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.

Declare Scope algC_scope.
Declare Scope algC_expanded_scope.

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

Local Notation ZtoQ := (intr : int rat).
Local Notation ZtoC := (intr : int algC).
Local Notation QtoC := (ratr : rat algC).

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 Definition intr_inj_ZtoC := (intr_inj : injective ZtoC).
#[local] Hint Resolve intr_inj_ZtoC : core.

Number fields and rational spans.
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 Num.int.

Lemma root_monic_Aint p x :
root p x p \is monic p \is a polyOver Num.int x \in Aint.

Lemma Cint_rat_Aint z : z \in Crat z \in Aint z \in Num.int.

Lemma Aint_Cint : {subset Num.int Aint}.

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

Lemma Aint0 : 0 \in Aint.
Lemma Aint1 : 1 \in Aint.
#[global] 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 Num.nat 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.

This is Isaacs, Theorem (3.4).
This is Isaacs, Corollary (3.5).
Corollary Aint_subring : subring_closed Aint.

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

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.
#[global] 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.
#[global] 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 [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).