Library mathcomp.field.algnum
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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}.
{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_class :=
fun x : algC ⇒ 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.
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_class :=
fun z : algC ⇒ 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.
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.
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 : algC ⇒ 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.
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.