- -

Library mathcomp.field.finfield

- -

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

- -

- Additional constructions and results on finite fields. - -

- - FinFieldExtType L == A FinFieldType structure on the carrier of L, - where L IS a fieldExtType F structure for an - F that has a finFieldType structure. This - does not take any existing finType structure - on L; this should not be made canonical. - FinSplittingFieldType F L == A SplittingFieldType F structure on the - carrier of L, where L IS a fieldExtType F for - an F with a finFieldType structure; this - should not be made canonical. - Import FinVector :: Declares canonical default finType, finRing, - etc structures (including FinFieldExtType - above) for abstract vectType, FalgType and - fieldExtType over a finFieldType. This should - be used with caution (e.g., local to a proof) - as the finType so obtained may clash with the - canonical one for standard types like matrix. - PrimeCharType charRp == The carrier of a ringType R such that - charRp : p \in [char R] holds. This type has - canonical ringType, ..., fieldType structures - compatible with those of R, as well as - canonical lmodType 'F_p, ..., algType 'F_p - structures, plus an FalgType structure if R - is a finUnitRingType and a splittingFieldType - struture if R is a finFieldType. - FinSplittingFieldFor nz_p == sigma-pair whose sval is a splittingFieldType - that is the splitting field for p : {poly F} - over F : finFieldType, given nz_p : p != 0. - PrimePowerField pr_p k_gt0 == sigma2-triple whose s2val is a finFieldType - of characteristic p and order m = p ^ k, - given pr_p : prime p and k_gt0 : k > 0. - FinDomainFieldType domR == A finFieldType structure on a finUnitRingType - R, given domR : GRing.IntegralDomain.axiom R. - This is intended to be used inside proofs, - where one cannot declare Canonical instances. - Otherwise one should construct explicitly the - intermediate structures using the ssralg and - finalg constructors, and finDomain_mulrC domR - finDomain_fieldP domR to prove commutativity - and field axioms (the former is Wedderburn's - little theorem). - FinDomainSplittingFieldType domR charRp == A splittingFieldType structure - that repackages the two constructions above. -

- -
-Set Implicit Arguments.
- -
-Import GroupScope GRing.Theory FinRing.Theory.
-Local Open Scope ring_scope.
- -
-Section FinRing.
- -
-Variable R : finRingType.
- -
-Lemma finRing_nontrivial : [set : R ] != 1%g.
- -
-Lemma finRing_gt1 : 1 < #|R |.
- -
-End FinRing.
- -
-Section FinField.
- -
-Variable F : finFieldType.
- -
-Lemma card_finField_unit : #|[set : {unit F }]| = #|F |.-1.
- -
-Definition finField_unit x (nz_x : x != 0) :=
- FinRing.unit F (etrans (unitfE x) nz_x).
- -
-Lemma expf_card x : x ^+ #|F | = x :> F.
- -
-Lemma finField_genPoly : 'X ^#|F | - 'X = \prod_x ('X - x %:P ) :> {poly F }.
- -
-Lemma finCharP : {p | prime p & p \in [char F ]}.
- -
-Lemma finField_is_abelem : is_abelem [set : F ].
- -
-Lemma card_finCharP p n : #|F | = (p ^ n)%N → prime p → p \in [char F ].
- -
-End FinField.
- -
-Section CardVspace.
- -
-Variables (F : finFieldType) (T : finType).
- -
-Section Vector.
- -
-Variable cvT : Vector.class_of F T.
-Let vT := Vector.Pack (Phant F) cvT.
- -
-Lemma card_vspace (V : {vspace vT }) : #|V | = (#|F | ^ \dim V)%N.
- -
-Lemma card_vspacef : #|{: vT }%VS| = #|T |.
- -
-End Vector.
- -
-Variable caT : Falgebra.class_of F T.
-Let aT := Falgebra.Pack (Phant F) caT.
- -
-Lemma card_vspace1 : #|(1%VS : {vspace aT })| = #|F |.
- -
-End CardVspace.
- -
-Lemma VectFinMixin (R : finRingType) (vT : vectType R) : Finite.mixin_of vT.
- -
-

- -

- These instancces are not exported by default because they conflict with - existing finType instances such as matrix_finType or primeChar_finType. -

-Module FinVector.
-Section Interfaces.
- -
-Variable F : finFieldType.
-Implicit Types (vT : vectType F) (aT : FalgType F) (fT : fieldExtType F).
- -
-Canonical vect_finType vT := FinType vT (VectFinMixin vT).
-Canonical Falg_finType aT := FinType aT (VectFinMixin aT).
-Canonical fieldExt_finType fT := FinType fT (VectFinMixin fT).
- -
-Canonical Falg_finRingType aT := [finRingType of aT ].
-Canonical fieldExt_finRingType fT := [finRingType of fT ].
-Canonical fieldExt_finFieldType fT := [finFieldType of fT ].
- -
-Lemma finField_splittingField_axiom fT : SplittingField.axiom fT.
- -
-End Interfaces.
-End FinVector.
- -
-Notation FinFieldExtType := FinVector.fieldExt_finFieldType.
-Notation FinSplittingFieldAxiom := (FinVector.finField_splittingField_axiom _).
-Notation FinSplittingFieldType F L :=
-  (SplittingFieldType F L FinSplittingFieldAxiom).
- -
-Section PrimeChar.
- -
-Variable p : nat.
- -
-Section PrimeCharRing.
- -
-Variable R0 : ringType.
- -
-Definition PrimeCharType of p \in [char R0 ] : predArgType := R0.
- -
-Hypothesis charRp : p \in [char R0 ].
-Implicit Types (a b : 'F_p) (x y : R).
- -
-Canonical primeChar_eqType := [eqType of R ].
-Canonical primeChar_choiceType := [choiceType of R ].
-Canonical primeChar_zmodType := [zmodType of R ].
-Canonical primeChar_ringType := [ringType of R ].
- -
-Definition primeChar_scale a x := a %:R × x.
- -
-Let natrFp n : (inZp n : 'F_p )%:R = n %:R :> R.
- -
-Lemma primeChar_scaleA a b x : a ×p : (b ×p : x ) = (a × b ) ×p : x.
- -
-Lemma primeChar_scale1 : left_id 1 primeChar_scale.
- -
-Lemma primeChar_scaleDr : right_distributive primeChar_scale +%R.
- -
-Lemma primeChar_scaleDl x : {morph primeChar_scale ^~ x : a b / a + b }.
- -
-Definition primeChar_lmodMixin :=
-  LmodMixin primeChar_scaleA primeChar_scale1
-            primeChar_scaleDr primeChar_scaleDl.
-Canonical primeChar_lmodType := LmodType 'F_p R primeChar_lmodMixin.
- -
-Lemma primeChar_scaleAl : GRing.Lalgebra.axiom ( *%R : R → R → R).
- Canonical primeChar_LalgType := LalgType 'F_p R primeChar_scaleAl.
- -
-Lemma primeChar_scaleAr : GRing.Algebra.axiom primeChar_LalgType.
- Canonical primeChar_algType := AlgType 'F_p R primeChar_scaleAr.
- -
-End PrimeCharRing.
- -
- -
-Canonical primeChar_unitRingType (R : unitRingType) charRp :=
-  [unitRingType of type R charRp ].
-Canonical primeChar_unitAlgType (R : unitRingType) charRp :=
-  [unitAlgType 'F_p of type R charRp ].
-Canonical primeChar_comRingType (R : comRingType) charRp :=
-  [comRingType of type R charRp ].
-Canonical primeChar_comUnitRingType (R : comUnitRingType) charRp :=
-  [comUnitRingType of type R charRp ].
-Canonical primeChar_idomainType (R : idomainType) charRp :=
-  [idomainType of type R charRp ].
-Canonical primeChar_fieldType (F : fieldType) charFp :=
-  [fieldType of type F charFp ].
- -
-Section FinRing.
- -
-Variables (R0 : finRingType) (charRp : p \in [char R0 ]).
- -
-Canonical primeChar_finType := [finType of R ].
-Canonical primeChar_finZmodType := [finZmodType of R ].
-Canonical primeChar_baseGroupType := [baseFinGroupType of R for +%R ].
-Canonical primeChar_groupType := [finGroupType of R for +%R ].
-Canonical primeChar_finRingType := [finRingType of R ].
-Canonical primeChar_finLmodType := [finLmodType 'F_p of R ].
-Canonical primeChar_finLalgType := [finLalgType 'F_p of R ].
-Canonical primeChar_finAlgType := [finAlgType 'F_p of R ].
- -
-Let pr_p : prime p.
- -
-Lemma primeChar_abelem : p .-abelem [set : R ].
- -
-Lemma primeChar_pgroup : p .-group [set : R ].
- -
-Lemma order_primeChar x : x != 0 :> R → #[x ]%g = p.
- -
-Let n := logn p #|R |.
- -
-Lemma card_primeChar : #|R | = (p ^ n)%N.
- -
-Lemma primeChar_vectAxiom : Vector.axiom n (primeChar_lmodType charRp).
- -
-Definition primeChar_vectMixin := Vector.Mixin primeChar_vectAxiom.
-Canonical primeChar_vectType := VectType 'F_p R primeChar_vectMixin.
- -
-Lemma primeChar_dimf : \dim {:primeChar_vectType } = n.
- -
-End FinRing.
- -
-Canonical primeChar_finUnitRingType (R : finUnitRingType) charRp :=
-  [finUnitRingType of type R charRp ].
-Canonical primeChar_finUnitAlgType (R : finUnitRingType) charRp :=
-  [finUnitAlgType 'F_p of type R charRp ].
-Canonical primeChar_FalgType (R : finUnitRingType) charRp :=
-  [FalgType 'F_p of type R charRp ].
-Canonical primeChar_finComRingType (R : finComRingType) charRp :=
-  [finComRingType of type R charRp ].
-Canonical primeChar_finComUnitRingType (R : finComUnitRingType) charRp :=
-  [finComUnitRingType of type R charRp ].
-Canonical primeChar_finIdomainType (R : finIdomainType) charRp :=
-  [finIdomainType of type R charRp ].
- -
-Section FinField.
- -
-Variables (F0 : finFieldType) (charFp : p \in [char F0 ]).
- -
-Canonical primeChar_finFieldType := [finFieldType of F ].
-

- -

- We need to use the eta-long version of the constructor here as projections - of the Canonical fieldType of F cannot be computed syntactically. -

-Canonical primeChar_fieldExtType := [fieldExtType 'F_p of F for F0 ].
-Canonical primeChar_splittingFieldType := FinSplittingFieldType 'F_p F.
- -
-End FinField.
- -
-End PrimeChar.
- -
-Section FinSplittingField.
- -
-Variable F : finFieldType.
- -
-

- -

- By card_vspace order K = #|K| for any finType structure on L; however we - do not want to impose the FinVector instance here. -

-Let order (L : vectType F) (K : {vspace L }) := (#|F | ^ \dim K)%N.
- -
-Section FinGalois.
- -
-Variable L : splittingFieldType F.
-Implicit Types (a b : F) (x y : L) (K E : {subfield L }).
- -
-Let galL K : galois K {:L }.
- -
-Fact galLgen K :
-  {alpha | generator 'Gal ({:L } / K ) alpha & ∀ x, alpha x = x ^+ order K }.
- -
-Lemma finField_galois K E : (K ≤ E)%VS → galois K E.
- -
-Lemma finField_galois_generator K E :
-   (K ≤ E)%VS →
- {alpha | generator 'Gal (E / K ) alpha
-        & {in E , ∀ x, alpha x = x ^+ order K }}.
- -
-End FinGalois.
- -
-Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L }) a :
-  (a \in K ) = (a ^+ order K == a ).
- -
-End FinSplittingField.
- -
-Section FinFieldExists.
-

- -

- While he existence of finite splitting fields and of finite fields of - arbitrary prime power order is mathematically straightforward, it is - technically challenging to formalize in Coq. The Coq typechecker performs - poorly for the spme of the deeply nested dependent types used in the - construction, such as polynomials over extensions of extensions of finite - fields. Any conversion in a nested structure parameter incurs a huge - overhead as it is shared across term comparison by call-by-need evalution. - The proof of FinSplittingFieldFor is contrived to mitigate this effect: - the abbreviation map_poly_extField alone divides by 3 the proof checking - time, by reducing the number of occurrences of field(Ext)Type structures - in the subgoals; the succesive, apparently redundant 'suffices' localize - some of the conversions to smaller subgoals, yielding a further 8-fold - time gain. In particular, we construct the splitting field as a subtype - of a recursive construction rather than prove that the latter yields - precisely a splitting field. -

- - The apparently redundant type annotation reduces checking time by 30%. -

-Let map_poly_extField (F : fieldType) (L : fieldExtType F) :=
-  map_poly (in_alg L) : {poly F } → {poly L }.
- -
-Lemma FinSplittingFieldFor (F : finFieldType) (p : {poly F }) :
-  p != 0 → {L : splittingFieldType F | splittingFieldFor 1 p ^%:A {:L }}.
- -
-Lemma PrimePowerField p k (m := (p ^ k)%N) :
-  prime p → 0 < k → {Fm : finFieldType | p \in [char Fm ] & #|Fm | = m }.
- -
-End FinFieldExists.
- -
-Section FinDomain.
- -
-Import ssrnum ssrint algC cyclotomic Num.Theory.
-(* Hide polynomial divisibility. *)
- -
-Variable R : finUnitRingType.
- -
-Hypothesis domR : GRing.IntegralDomain.axiom R.
-Implicit Types x y : R.
- -
-Let lregR x : x != 0 → GRing.lreg x.
- -
-Lemma finDomain_field : GRing.Field.mixin_of R.
- -
-

- -

- This is Witt's proof of Wedderburn's little theorem. -

-Theorem finDomain_mulrC : @commutative R R *%R.
- -
-Definition FinDomainFieldType : finFieldType :=
-  let fin_unit_class := FinRing.UnitRing.class R in
-  let com_class := GRing.ComRing.Class finDomain_mulrC in
-  let com_unit_class := @GRing.ComUnitRing.Class R com_class fin_unit_class in
-  let dom_class := @GRing.IntegralDomain.Class R com_unit_class domR in
-  let field_class := @GRing.Field.Class R dom_class finDomain_field in
-  let finfield_class := @FinRing.Field.Class R field_class fin_unit_class in
-  FinRing.Field.Pack finfield_class.
- -
-Definition FinDomainSplittingFieldType p (charRp : p \in [char R ]) :=
-   let RoverFp := @primeChar_splittingFieldType p FinDomainFieldType charRp in
-   [splittingFieldType 'F_p of R for RoverFp ].
- -
-End FinDomain.
-