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.
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] 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]}.
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).
Lemma mem_Crat_span s : {subset s ≤ Crat_span s}.
Fact Crat_span_zmod_closed s : zmod_closed (Crat_span 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.
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}.
{z | ∃ a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i
& ∃ ps, s = [seq (pQtoC p).[z] | p <- ps]}.
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).
Lemma mem_Crat_span s : {subset s ≤ Crat_span s}.
Fact Crat_span_zmod_closed s : zmod_closed (Crat_span 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.
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}}.
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 x ⇒ dec_Cint_span (in_tuple [seq \row_(i < 1) y | y <- s]) (\row_i x).
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).
Automorphism extensions.
Lemma extend_algC_subfield_aut (Qs : fieldExtType rat)
(QsC : {rmorphism Qs → algC}) (phi : {rmorphism Qs → Qs}) :
{nu : {rmorphism algC → algC} | {morph QsC : x / phi x >-> nu x}}.
(QsC : {rmorphism Qs → algC}) (phi : {rmorphism Qs → Qs}) :
{nu : {rmorphism algC → algC} | {morph QsC : x / phi x >-> nu x}}.
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}.
coprime k n →
{u : {rmorphism algC → algC} | ∀ z, z ^+ n = 1 → u z = z ^+ k}.
Algebraic integers.
Definition Aint : {pred algC} := fun x ⇒ minCpoly 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.
{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).
Theorem fin_Csubring_Aint S n (Y : n.-tuple algC) :
mulr_closed S → (∀ x, reflect (inIntSpan Y x) (x \in S)) →
{subset S ≤ Aint}.
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.
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 z ⇒ if 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.
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 z ⇒ if 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.