Skip to content

Commit

Permalink
Port to hierarchy builder
Browse files Browse the repository at this point in the history
  • Loading branch information
@proux01
proux01 committed May 19, 2022
1 parent 0fe5e08 commit 6832d38
Show file tree
Hide file tree
Showing 5 changed files with 91 additions and 104 deletions.
74 changes: 35 additions & 39 deletions theories/abel.v
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
From mathcomp Require Import all_solvable all_field polyrcf.
From Abel Require Import various classic_ext map_gal algR.
Expand Down Expand Up @@ -657,7 +658,8 @@ apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0).
exists rs => //; suff <- : limg iota = 1%VS by [].
apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v.
by move=> /memv_imgP[u _ ->]; rewrite iotaF/= rpredZ// rpred1.
pose S := SplittingFieldType F L splitL.
pose sM := FieldExt_IsSplittingField.Build F L splitL.
pose S : splittingFieldType F := HB.pack L sM.
exists S, rs; split => //=; first by rewrite -(eq_map_poly iotaF).
by apply: (sol_p S rs); rewrite -(eq_map_poly iotaF).
move=> L rs prs; apply: sol_p => -[M [rs' [prs']]].
Expand All @@ -682,7 +684,8 @@ have splitK : splittingFieldFor 1 (p ^^ in_alg K) fullv.
by rewrite lfunE subvsP.
have sfK : SplittingField.axiom K.
by exists (p ^^ in_alg K) => //; apply/polyOver1P; exists p.
pose S := SplittingFieldType F K sfK.
pose sM := FieldExt_IsSplittingField.Build F K sfK.
pose S : splittingFieldType F := HB.pack K sM.
have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by [].
have splitM : splittingFieldFor 1 (p ^^ in_alg M) <<1 & rs'>> by exists rs'.
have splitL : splittingFieldFor 1 (p ^^ in_alg L) <<1 & rs>> by exists rs.
Expand Down Expand Up @@ -719,7 +722,8 @@ have splitL : SplittingField.axiom L.
exists rs => //; suff <- : limg f = 1%VS by [].
apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v.
by move=> /memv_imgP[u _ ->]; rewrite fF/= rpredZ// rpred1.
pose S := SplittingFieldType F L splitL.
pose sM := FieldExt_IsSplittingField.Build F L splitL.
pose S : splittingFieldType F := HB.pack L sM.
pose d := \dim <<1 & (rs : seq S)>>.
have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F.
by have /charf0P-> := charF0; rewrite -lt0n adim_gt0.
Expand Down Expand Up @@ -750,7 +754,9 @@ have prs : p ^^ in_alg L %= \prod_(z <- rs) ('X - z%:P).
by rewrite (eq_map_poly (fmorph_eq_rat _)).
have splitL : SplittingField.axiom L.
by exists (p ^^ in_alg L); [by apply/polyOver1P; exists p | exists rs].
pose S := SplittingFieldType rat L splitL.
pose Frat := [the fieldType of rat : Type].
pose sM := FieldExt_IsSplittingField.Build Frat L splitL.
pose S : splittingFieldType Frat := HB.pack L sM.
pose d := \dim <<1 & (rs : seq S)>>.
have d_gt0 : (d > 0)%N by rewrite adim_gt0.
have [ralg ralg_prim] := C_prim_root_exists d_gt0.
Expand All @@ -767,7 +773,8 @@ have splitL' : SplittingField.axiom L'.
have [us cycloE usw] := splitting_Fadjoin_cyclotomic 1%AS w_prim.
exists (us ++ rs'); last by rewrite adjoin_cat usw -adjoin_cons.
by rewrite big_cat/= (eqp_trans (eqp_mulr _ cycloE))// eqp_mull//.
pose S' := SplittingFieldType rat L' splitL'.
pose sM' := FieldExt_IsSplittingField.Build Frat L' splitL'.
pose S' : splittingFieldType Frat := HB.pack L' sM'.
have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by exists rs.
have splitS' : splittingFieldFor 1 (p ^^ in_alg S') <<1 & rs'>> by exists rs'.
have [f /= imgf] := splitting_ahom splitS splitS'.
Expand All @@ -778,10 +785,10 @@ Qed.
Lemma splitting_num_field (p : {poly rat}) :
{L : splittingFieldType rat & { LtoC : {rmorphism L -> algC} |
(p != 0 -> splittingFieldFor 1 (p ^^ in_alg L) {:L})
/\ (p = 0 -> L = [splittingFieldType rat of rat^o]) }}.
/\ (p = 0 -> L = [the splittingFieldType rat of rat^o]) }}.
Proof.
have [->|p_neq0] := eqVneq p 0.
by exists [splittingFieldType rat of rat^o], [rmorphism of ratr]; split.
by exists [the splittingFieldType rat of rat^o], [rmorphism of ratr]; split.
have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)).
have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P).
by rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx// lead_coef_eq0 map_poly_eq0.
Expand All @@ -791,7 +798,10 @@ have splitL' : splittingFieldFor 1 (p ^^ in_alg L') {: L'}%AS.
by rewrite -map_poly_comp map_prod_XsubC rs'E (eq_map_poly (fmorph_eq_rat _)).
have splitaxL' : SplittingField.axiom L'.
by exists (p ^^ in_alg L'); first by apply/polyOver1P; exists p.
exists (SplittingFieldType rat L' splitaxL'), L'toC; split => //.
pose Frat := [the fieldType of rat : Type].
pose sM' := FieldExt_IsSplittingField.Build Frat L' splitaxL'.
pose S' : splittingFieldType Frat := HB.pack L' sM'.
exists S', L'toC; split => //.
by move=> p_eq0; rewrite p_eq0 eqxx in p_neq0.
Qed.

Expand All @@ -811,7 +821,7 @@ Qed.
Definition numfield (p : {poly rat}) : splittingFieldType rat :=
projT1 (splitting_num_field p).

Lemma numfield0 : numfield 0 = [splittingFieldType rat of rat^o].
Lemma numfield0 : numfield 0 = [the splittingFieldType rat of rat^o].
Proof. by rewrite /numfield; case: splitting_num_field => //= ? [? [_ ->]]. Qed.

Definition numfield_inC (p : {poly rat}) :
Expand Down Expand Up @@ -901,7 +911,7 @@ Qed.
Let rp'_uniq : uniq rp'.
Proof.
rewrite -separable_prod_XsubC -(eqp_separable ratr_p').
rewrite -char0_ratrE separable_map.
rewrite -char0_ratrE separable_map separable_poly.unlock.
apply/coprimepP => d; have [sp_gt1 eqp] := p_irr => /eqp.
rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1).
move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv.
Expand Down Expand Up @@ -1073,7 +1083,7 @@ Lemma gal_perm_cycle_order : #[(gal_perm gal_cycle)]%g = d.
Proof. by rewrite order_injm ?gal_cycle_order ?injm_gal_perm ?gal1. Qed.

Definition conjL : {lrmorphism L -> L} :=
projT1 (restrict_aut_to_normal_num_field iota conjC).
projT1 (restrict_aut_to_normal_num_field iota Num.conj_op).

Definition iotaJ : {morph iota : x / conjL x >-> x^*} :=
projT2 (restrict_aut_to_normal_num_field _ _).
Expand Down Expand Up @@ -1209,6 +1219,7 @@ Hint Resolve irreducible_example : core.

Lemma separable_example : separable_poly poly_example.
Proof.
rewrite separable_poly.unlock.
apply/coprimepP => q /(irredp_XsubCP irreducible_example) [//| eqq].
have size_deriv_example : size poly_example^`() = 5%N.
rewrite !derivCE addr0 alg_polyC -scaler_nat addr0.
Expand Down Expand Up @@ -1354,25 +1365,15 @@ Definition decode_const (n : nat) : const :=
match n with 0 => Zero | 1 => One | n.+2 => URoot n end.
Lemma code_constK : cancel encode_const decode_const.
Proof. by case. Qed.
Definition const_eqMixin := CanEqMixin code_constK.
Canonical const_eqType := EqType const const_eqMixin.
Definition const_choiceMixin := CanChoiceMixin code_constK.
Canonical const_choiceType := ChoiceType const const_choiceMixin.
Definition const_countMixin := CanCountMixin code_constK.
Canonical const_countType := CountType const const_countMixin.
HB.instance Definition _ := Countable.copy const (can_type code_constK).

Definition encode_binOp (c : binOp) : bool :=
match c with Add => false | Mul => true end.
Definition decode_binOp (b : bool) : binOp :=
match b with false => Add | _ => Mul end.
Lemma code_binOpK : cancel encode_binOp decode_binOp.
Proof. by case. Qed.
Definition binOp_eqMixin := CanEqMixin code_binOpK.
Canonical binOp_eqType := EqType binOp binOp_eqMixin.
Definition binOp_choiceMixin := CanChoiceMixin code_binOpK.
Canonical binOp_choiceType := ChoiceType binOp binOp_choiceMixin.
Definition binOp_countMixin := CanCountMixin code_binOpK.
Canonical binOp_countType := CountType binOp binOp_countMixin.
HB.instance Definition _ := Countable.copy binOp (can_type code_binOpK).

Definition encode_unOp (c : unOp) : nat + nat :=
match c with Opp => inl _ 0%N | Inv => inl _ 1%N
Expand All @@ -1382,12 +1383,7 @@ Definition decode_unOp (n : nat + nat) : unOp :=
| inl n.+2 => Exp n | inr n => Root n end.
Lemma code_unOpK : cancel encode_unOp decode_unOp.
Proof. by case. Qed.
Definition unOp_eqMixin := CanEqMixin code_unOpK.
Canonical unOp_eqType := EqType unOp unOp_eqMixin.
Definition unOp_choiceMixin := CanChoiceMixin code_unOpK.
Canonical unOp_choiceType := ChoiceType unOp unOp_choiceMixin.
Definition unOp_countMixin := CanCountMixin code_unOpK.
Canonical unOp_countType := CountType unOp unOp_countMixin.
HB.instance Definition _ := Countable.copy unOp (can_type code_unOpK).

Fixpoint encode_algT F (f : algterm F) : GenTree.tree (F + const) :=
let T_ isbin := if isbin then binOp else unOp in
Expand All @@ -1414,14 +1410,12 @@ Lemma code_algTK F : cancel (@encode_algT F) (@decode_algT F).
Proof.
by elim => // [u f IHf|b f IHf f' IHf']/=; rewrite pickleK -lock ?IHf ?IHf'.
Qed.
Definition algT_eqMixin (F : eqType) := CanEqMixin (@code_algTK F).
Canonical algT_eqType (F : eqType) := EqType (algterm F) (@algT_eqMixin F).
Definition algT_choiceMixin (F : choiceType) := CanChoiceMixin (@code_algTK F).
Canonical algT_choiceType (F : choiceType) :=
ChoiceType (algterm F) (@algT_choiceMixin F).
Definition algT_countMixin (F : countType) := CanCountMixin (@code_algTK F).
Canonical algT_countType (F : countType) :=
CountType (algterm F) (@algT_countMixin F).
HB.instance Definition _ (F : eqType) := Equality.copy (algterm F)
(can_type (@code_algTK F)).
HB.instance Definition _ (F : choiceType) := Choice.copy (algterm F)
(can_type (@code_algTK F)).
HB.instance Definition _ (F : countType) := Countable.copy (algterm F)
(can_type (@code_algTK F)).

Declare Scope algT_scope.
Delimit Scope algT_scope with algT.
Expand Down Expand Up @@ -1551,7 +1545,9 @@ have mprs : mp ^^ in_alg L %= \prod_(z <- rsmp) ('X - z%:P).
by rewrite -char0_ratrE// (eq_map_poly (fmorph_eq_rat _)) eqpxx.
have splitL : SplittingField.axiom L.
by exists (mp ^^ in_alg L); [apply/polyOver1P; exists mp | exists rsmp].
pose S := SplittingFieldType rat L splitL.
pose Frat := [the fieldType of rat : Type].
pose sM := FieldExt_IsSplittingField.Build Frat L splitL.
pose S : splittingFieldType Frat := HB.pack L sM.
have algsW: {subset rsalg <= algs}.
move=> x; rewrite -fsE => /mapP[{x}f ffs ->].
apply/flattenP; exists (subeval ratr f); rewrite ?map_f//.
Expand All @@ -1573,7 +1569,7 @@ rewrite {p p_neq0 mkalg pE prs rsmp iota_rs mprs rsf rs rsE mp
suff: forall (L : splittingFieldType rat) (iota : {rmorphism L -> algC}) als,
map iota als = algs -> radical.-ext 1%VS <<1 & als>>%VS.
by move=> /(_ S iota als alsE).
move=> {}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE.
move=> {sM}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE.
elim: fs => [|f fs IHfs]//= in rsalg fsE als alsE *.
case: als => []// in alsE *.
by rewrite Fadjoin_nil; apply: rext_refl.
Expand Down
63 changes: 20 additions & 43 deletions theories/xmathcomp/algR.v
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
From mathcomp Require Import all_solvable all_field.
From Abel Require Import various.
Expand All @@ -15,33 +16,18 @@ Local Notation "p ^^ f" := (map_poly f p)

Record algR := in_algR {algRval : algC; algRvalP : algRval \is Num.real}.

Canonical algR_subType := [subType for algRval].
Definition algR_eqMixin := [eqMixin of algR by <:].
Canonical algR_eqType := EqType algR algR_eqMixin.
Definition algR_choiceMixin := [choiceMixin of algR by <:].
Canonical algR_choiceType := ChoiceType algR algR_choiceMixin.
Definition algR_countMixin := [countMixin of algR by <:].
Canonical algR_countType := CountType algR algR_countMixin.
Definition algR_zmodMixin := [zmodMixin of algR by <:].
Canonical algR_zmodType := ZmodType algR algR_zmodMixin.
Definition algR_ringMixin := [ringMixin of algR by <:].
Canonical algR_ringType := RingType algR algR_ringMixin.
Definition algR_comRingMixin := [comRingMixin of algR by <:].
Canonical algR_comRingType := ComRingType algR algR_comRingMixin.
Definition algR_unitRingMixin := [unitRingMixin of algR by <:].
Canonical algR_unitRingType := UnitRingType algR algR_unitRingMixin.
Canonical algR_comUnitRingType := [comUnitRingType of algR].
Definition algR_idomainMixin := [idomainMixin of algR by <:].
Canonical algR_idomainType := IdomainType algR algR_idomainMixin.
Definition algR_fieldMixin := [fieldMixin of algR by <:].
Canonical algR_fieldType := FieldType algR algR_fieldMixin.
Definition algR_porderMixin := [porderMixin of algR by <:].
Canonical algR_porderType := POrderType ring_display algR algR_porderMixin.
Lemma total_algR : totalPOrderMixin [porderType of algR].
HB.instance Definition _ := [IsSUB for algRval].
HB.instance Definition _ := [Countable of algR by <:].
HB.instance Definition _ := [zmodMixin of algR by <:].
HB.instance Definition _ := [ringMixin of algR by <:].
HB.instance Definition _ := [comRingMixin of algR by <:].
HB.instance Definition _ := [unitRingMixin of algR by <:].
HB.instance Definition _ := [idomainMixin of algR by <:].
HB.instance Definition _ := [fieldMixin of algR by <:].
HB.instance Definition _ := [POrder of algR by <:].
Lemma total_algR : total (<=%O : rel [porderType of algR]).
Proof. by move=> x y; apply/real_leVge/valP/valP. Qed.
Canonical algR_latticeType := LatticeType algR total_algR.
Canonical algR_distrLatticeType := DistrLatticeType algR total_algR.
Canonical algR_orderType := OrderType algR total_algR.
HB.instance Definition _ := Order.POrder_IsTotal.Build _ algR total_algR.

Lemma algRval_is_rmorphism : rmorphism algRval. Proof. by []. Qed.
Canonical algRval_additive := Additive algRval_is_rmorphism.
Expand All @@ -58,8 +44,6 @@ Lemma algR_normrN x : algR_norm (- x) = algR_norm x.
Proof. by apply/val_inj; apply: normrN. Qed.

Section Num.
Definition algR_normedMixin :=
Num.NormedMixin algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN.

Section withz.
Let z : algR := 0.
Expand All @@ -73,18 +57,10 @@ Lemma algR_ler_def (x y : algR) : (x <= y) = (algR_norm (y - x) == y - x).
Proof. by apply: ler_def. Qed.
End withz.

Let algR_ring := (GRing.Ring.Pack (GRing.ComRing.base
(GRing.ComUnitRing.base (GRing.IntegralDomain.base
(GRing.IntegralDomain.class [idomainType of algR]))))).
Definition algR_numMixin : @Num.mixin_of algR_ring _ _ :=
@Num.Mixin _ _ algR_normedMixin
algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def.

Canonical algR_numDomainType := NumDomainType algR algR_numMixin.
Canonical algR_normedZmodType := NormedZmodType algR algR algR_normedMixin.
Canonical algR_numFieldType := [numFieldType of algR].
Canonical algR_realDomainType := [realDomainType of algR].
Canonical algR_realFieldType := [realFieldType of algR].
HB.instance Definition _ := Num.Zmodule_IsNormed.Build _ algR
algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN.
HB.instance Definition _ := Num.IsNumDomain.Build _ algR
algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def.
End Num.

Definition algR_archiFieldMixin : Num.archimedean_axiom [numDomainType of algR].
Expand All @@ -96,7 +72,8 @@ set n := floorC _; have [n_lt0|n_ge0] := ltP n 0.
move=> x_lt; exists (`|(n + 1)%R|%N); apply: lt_le_trans x_lt _.
by rewrite /= rmorphMn/= pmulrn gez0_abs// addr_ge0.
Qed.
Canonical algR_archiFieldType := ArchiFieldType algR algR_archiFieldMixin.
HB.instance Definition _ := Num.RealField_IsArchimedean.Build algR
algR_archiFieldMixin.

Definition algRpfactor (x : algC) : {poly algR} :=
if x \is Num.real =P true is ReflectT xR then 'X - (in_algR xR)%:P else
Expand Down Expand Up @@ -205,7 +182,7 @@ elim: n r => // n IHn [|x r]/= in p pr *.
rewrite ltnS => r_lt.
have xJxr : x^* \in x :: r.
rewrite -root_prod_XsubC -pr.
have /eq_map_poly-> : algRval =1 conjC \o algRval.
have /eq_map_poly-> : algRval =1 Num.conj_op \o algRval.
by move=> a /=; rewrite (CrealP (algRvalP _)).
by rewrite map_poly_comp mapf_root pr root_prod_XsubC mem_head.
have xJr : (x \isn't Num.real) ==> (x^* \in r) by rewrite implyNb CrealE.
Expand Down Expand Up @@ -270,4 +247,4 @@ move=> /andP[xR rsabR] /andP[axb arsb] prsab.
exists (in_algR xR) => //=.
by rewrite -(mapf_root [rmorphism of algRval])//= prsab rootM root_XsubC eqxx.
Qed.
Canonical algR_rcfType := RcfType algR algR_rcfMixin.
HB.instance Definition _ := Num.RealField_IsClosed.Build algR algR_rcfMixin.
9 changes: 7 additions & 2 deletions theories/xmathcomp/classic_ext.v
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
From mathcomp Require Import all_solvable all_field.
From Abel Require Import various cyclotomic_ext.
Expand Down Expand Up @@ -164,7 +165,9 @@ Proof.
move=> /(@classic_cycloExt _ L).
apply/classic_bind => -[M [w [iota wfull wprim]]]; apply/classicW.
suff splitM : SplittingField.axiom M.
by exists (SplittingFieldType F0 M splitM), w, iota.
pose mM := FieldExt_IsSplittingField.Build F0 M splitM.
pose mT : splittingFieldType F0 := HB.pack M mM.
by exists mT, w, iota.
apply: (@SplittingFieldExt _ L ('Phi_n ^^ intr) _ iota).
rewrite -map_poly_comp (eq_map_poly (rmorph_int _)) -wfull.
by rewrite (Phi_cyclotomic wprim); apply: splitting_Fadjoin_cyclotomic.
Expand All @@ -181,7 +184,9 @@ move=> nN0; suff: classically { L' : fieldExtType F & { w : L' &
have splitL : SplittingField.axiom L.
exists (cyclotomic w n); rewrite ?cyclotomic_over// -wfull.
exact: splitting_Fadjoin_cyclotomic.
by exists (SplittingFieldType F L splitL), w.
pose lM := FieldExt_IsSplittingField.Build F L splitL.
pose lT : splittingFieldType F := HB.pack L lM.
by exists lT, w.
pose Fo := [splittingFieldType F of F^o].
apply: classic_bind (@classic_cycloExt _ Fo n nN0).
case=> [L [w [iota wfull wprim]]]; apply/classicW.
Expand Down
14 changes: 9 additions & 5 deletions theories/xmathcomp/map_gal.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -672,7 +672,7 @@ Implicit Types (K E F : {subfield L}).
Lemma separable_aimgr E F s : s \in kAEndf E ->
separable E (s @: F) = separable E F.
Proof.
rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -(separable_aimg _ _ s).
rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -[RHS](separable_aimg _ _ s).
suff /eq_in_limg->: {in E, s =1 \1%VF} by rewrite lim1g.
by move=> x xE; rewrite lfunE/= s_id.
Qed.
Expand Down Expand Up @@ -773,7 +773,8 @@ Lemma solvable_ext_refl E : solvable_ext E E.
Proof.
by apply/solvable_extP; exists E; rewrite subvv galois_refl/= galvv solvable1.
Qed.
Hint Resolve solvable_ext_refl : core.
Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) =>
(apply: solvable_ext_refl) : core.

Lemma sub_solvable_ext F K E :
(E <= F)%VS -> solvable_ext K F -> solvable_ext K E.
Expand Down Expand Up @@ -837,10 +838,13 @@ Qed.

End normalClosure.

Hint Resolve normalClosureSl : core.
Hint Resolve normalClosureSr : core.
Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) =>
(apply: normalClosureSl) : core.
Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) =>
(apply: normalClosureSr) : core.
Hint Resolve normalClosure_normal : core.
Hint Resolve solvable_ext_refl : core.
Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) =>
(apply: solvable_ext_refl) : core.

Lemma aimg_normalClosure (F0 : fieldType) (L L' : splittingFieldType F0)
(iota : 'AHom(L, L')) (K E : {subfield L}) :
Expand Down
Loading

0 comments on commit 6832d38

Please sign in to comment.