Library mathcomp.field.finfield
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 countalg.
From mathcomp Require Import finalg zmodp cyclic center pgroup abelian matrix.
From mathcomp Require Import mxpoly vector falgebra fieldext separable galois.
From mathcomp Require ssrnum ssrint algC cyclotomic.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 countalg.
From mathcomp Require Import finalg zmodp cyclic center pgroup abelian matrix.
From mathcomp Require Import mxpoly vector 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 F T.
Let vT := Vector.Pack cvT.
Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N.
Lemma card_vspacef : #|{: vT}%VS| = #|T|.
End Vector.
Variable caT : Falgebra F T.
Let aT := Falgebra.Pack caT.
Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|.
End CardVspace.
Definition finvect_type (vT : Type) : predArgType := vT.
Section FinVector.
Variables (R : finRingType) (vT : vectType R).
End FinVector.
Section FinFieldExt.
Variables (F : finFieldType) (fT : fieldExtType F).
Lemma ffT_splitting_subproof :
SplittingField.axiom [the fieldExtType _ of ffT].
End FinFieldExt.
Definition FinSplittingFieldType (F : finFieldType) (fT : fieldExtType F) :=
HB.pack_for (splittingFieldType F) fT (SplittingField.on (finvect_type fT)).
Definition FinFieldExtType (F : finFieldType) (fT : fieldExtType F) :=
HB.pack_for finFieldType (FinSplittingFieldType fT) (FinRing.Field.on (finvect_type fT)).
Arguments FinSplittingFieldType : clear implicits.
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).
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}.
Lemma primeChar_scaleAl (a : 'F_p) (u v : R) : a *: (u × v) = (a *: u) × v.
Lemma primeChar_scaleAr (a : 'F_p) (x y : R) : a *: (x × y) = x × (a *: y).
End PrimeCharRing.
TODO: automatize parameter inference to do all of these
Section FinRing.
Variables (R0 : finRingType) (charRp : p \in [char R0]).
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 : {v2r : R → 'rV_n | linear v2r & bijective v2r}.
Lemma primeChar_dimf : \dim {: [vectType [ringType of 'F_p] of R]} = n.
End FinRing.
Section FinField.
Variables (F0 : finFieldType) (charFp : p \in [char F0]).
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.
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}.
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.
(* Hide polynomial divisibility. *)
Variable R : finUnitRingType.
Hypothesis domR : GRing.integral_domain_axiom R.
Implicit Types x y : R.
Let lregR x : x != 0 → GRing.lreg x.
Lemma finDomain_field : GRing.field_axiom R.
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 order ssrnum ssrint algC cyclotomic Order.TTheory Num.Theory.
(* Hide polynomial divisibility. *)
Variable R : finUnitRingType.
Hypothesis domR : GRing.integral_domain_axiom R.
Implicit Types x y : R.
Let lregR x : x != 0 → GRing.lreg x.
Lemma finDomain_field : GRing.field_axiom R.
This is Witt's proof of Wedderburn's little theorem.
Theorem finDomain_mulrC : @commutative R R *%R.
Definition FinDomainFieldType : finFieldType :=
let cC := GRing.Ring_hasCommutativeMul.Build R finDomain_mulrC in
let cR : comUnitRingType := HB.pack R cC in
let iC := GRing.ComUnitRing_isIntegral.Build cR domR in
let iR : finIntegralDomainType := HB.pack cR iC in
let fC := GRing.UnitRing_isField.Build iR finDomain_field in
HB.pack iR fC.
Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) :=
let RoverFp := [splittingFieldType _ of
@PrimeCharType p FinDomainFieldType charRp] in
[splittingFieldType [fieldType of 'F_p] of R for RoverFp].
End FinDomain.
Definition FinDomainFieldType : finFieldType :=
let cC := GRing.Ring_hasCommutativeMul.Build R finDomain_mulrC in
let cR : comUnitRingType := HB.pack R cC in
let iC := GRing.ComUnitRing_isIntegral.Build cR domR in
let iR : finIntegralDomainType := HB.pack cR iC in
let fC := GRing.UnitRing_isField.Build iR finDomain_field in
HB.pack iR fC.
Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) :=
let RoverFp := [splittingFieldType _ of
@PrimeCharType p FinDomainFieldType charRp] in
[splittingFieldType [fieldType of 'F_p] of R for RoverFp].
End FinDomain.