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.
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.
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]}.
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}.
{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}}.
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).
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 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 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.
{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}.
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 algC} :=
fun z ⇒ if 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 : 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.
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 algC} :=
fun z ⇒ if 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 : 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.