(Joint Center)Library finfield

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
Require Import fintype bigop finset prime fingroup ssralg finalg cyclic abelian.
Require Import tuple finfun choice matrix vector falgebra fieldext separable.
Require Import pgroup poly polydiv galois morphism mxabelem zmodp.

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.

Set Implicit Arguments.

Open Local Scope group_scope.
Open Local Scope ring_scope.
Import GRing.Theory.
Import FinRing.Theory.

Section FinRing.

Variable R : finRingType.

GG: Coq v8.3 fails to unify FinGroup.arg_sort _ with FinRing.sort R here because it expands the latter rather than FinGroup.arg_sort, which would expose the FinGroup.sort projection, thereby enabling canonical structure expansion. We should check whether the improved heuristics in Coq 8.4 have resolved this issue.
Lemma finRing_nontrivial : [set: R] != 1%g.

GG: same issue here.
Lemma finRing_gt1 : 1 < #|R|.

End FinRing.

Section FinField.

Variable F : finFieldType.

Lemma card_finField_unit : #|[set: {unit F}]| = #|F|.-1.

Fact finField_unit_subproof x : x != 0 :> Fx \is a GRing.unit.

Definition finField_unit x nz_x :=
  FinRing.unit F (@finField_unit_subproof 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)%Nprime pp \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 T.

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

Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|.

End CardVspace.

Lemma VectFinMixin (R : finRingType) (vT : vectType R) : Finite.mixin_of vT.

These instacnces 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].
Local Notation R := (PrimeCharType charRp).
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.
Local Infix "*p:" := primeChar_scale (at level 40).

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

Local Notation type := @PrimeCharType.

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]).
Local Notation R := (type _ charRp).

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

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]).
Local Notation F := (type _ charFp).

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