- -

Library mathcomp.field.algnum

- -

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

- -

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

- -

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

- -

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

- -

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

- -

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

- -

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

- -

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

- -

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