Library mathcomp.field.finfield

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype div tuple bigop prime finset fingroup.
From mathcomp Require Import ssralg poly polydiv morphism action finalg zmodp.
From mathcomp Require Import cyclic center pgroup abelian matrix mxpoly vector.
From mathcomp Require Import falgebra fieldext separable galois.
From mathcomp Require ssrnum ssrint algC cyclotomic.

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.

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 the 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 some 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 }.
Local Notation "p ^%:A" := (map_poly_extField _ p)
  (at level 2, format "p ^%:A") : ring_scope.

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 order ssrnum ssrint algC cyclotomic Order.TTheory Num.Theory.
Local Infix "%|" := dvdn. (* 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.