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 Jan 25, 2023
1 parent 9449966 commit 837ad43
Show file tree
Hide file tree
Showing 7 changed files with 190 additions and 170 deletions.
80 changes: 38 additions & 42 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 @@ -458,7 +459,7 @@ apply/eqP; rewrite /image_mem (map_comp (fun i => x * w ^+ i)) val_enum_ord.
rewrite -[p]prednK//= mulr1 -[p.-1]prednK//= expr1 !adjoin_cons.
have -> : <<<<E; x>>; x * w>>%VS = <<<<E; w>>; x>>%VS.
apply/eqP; rewrite [X in _ == X]adjoinC eqEsubv/= !Fadjoin_sub//.
by rewrite -(@fpredMl _ _ _ _ x)// ?memv_adjoin//= adjoinC memv_adjoin.
by rewrite -(@fpredMl _ _ x)// ?memv_adjoin//= adjoinC memv_adjoin.
by rewrite rpredM// ?memv_adjoin//= adjoinC memv_adjoin.
rewrite (Fadjoin_seq_idP _)// all_map; apply/allP => i _/=.
by rewrite rpredM ?rpredX//= ?memv_adjoin// adjoinC memv_adjoin.
Expand Down Expand Up @@ -659,7 +660,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 @@ -684,7 +686,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 @@ -721,7 +724,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 @@ -752,7 +756,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 @@ -769,7 +775,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 @@ -780,10 +787,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 @@ -793,7 +800,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 @@ -813,7 +823,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 @@ -903,7 +913,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 @@ -1075,7 +1085,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 @@ -1211,6 +1221,7 @@ Qed.

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 @@ -1271,7 +1282,7 @@ apply: lt_sorted_eq; rewrite ?sorted_roots//.
by rewrite /= andbT -subr_gt0 opprK ?addr_gt0 ?alpha_gt0.
move=> x; rewrite mem_rootsR ?map_poly_eq0// !inE -topredE/= orbC.
rewrite deriv_poly_example /root.
rewrite rmorphB linearZ/= map_polyC/= map_polyXn !pesimp.
rewrite rmorphB /= linearZ map_polyC/= map_polyXn !pesimp.
rewrite -[5%:R]sqr_sqrtr ?ler0n// (exprM _ 2 2) -exprMn (natrX _ 2 2) subr_sqr.
rewrite mulf_eq0 [_ + 2%:R == 0]gt_eqF ?orbF; last first.
by rewrite ltr_spaddr ?ltr0n// mulr_ge0 ?sqrtr_ge0// exprn_even_ge0.
Expand All @@ -1297,7 +1308,7 @@ rewrite -big_filter (perm_big (map algRval (rootsR pR))); last first.
rewrite map_poly_comp/=.
apply/andP/mapP => [[xR xroot]|[y + ->]].
exists (in_algR xR); rewrite // mem_rootsR// -topredE/=.
by rewrite -(mapf_root algRval_rmorphism)/=.
by rewrite -(mapf_root [rmorphism of algRval])/=.
rewrite mem_rootsR// -[y \in _]topredE/=.
by split; [apply/algRvalP|rewrite mapf_root].
apply/eqP; rewrite sum1_size size_map eqn_leq.
Expand Down Expand Up @@ -1356,25 +1367,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 @@ -1384,12 +1385,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 @@ -1416,14 +1412,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 @@ -1554,7 +1548,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 @@ -1576,7 +1572,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
70 changes: 24 additions & 46 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,37 +16,23 @@ 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 _ := [SubChoice_isSubIntegralDomain of algR by <:].
HB.instance Definition _ := [SubIntegralDomain_isSubField 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.
Canonical algRval_rmorphism := RMorphism algRval_is_rmorphism.
Lemma algRval_is_additive : additive algRval. Proof. by []. Qed.
Lemma algRval_is_multiplicative : multiplicative algRval. Proof. by []. Qed.
HB.instance Definition _ :=
GRing.isAdditive.Build [zmodType of algR] [zmodType of algC] algRval
algRval_is_additive.
HB.instance Definition _ :=
GRing.isMultiplicative.Build [ringType of algR] [ringType of algC] algRval
algRval_is_multiplicative.

Definition algR_norm (x : algR) : algR := in_algR (normr_real (val x)).
Lemma algR_ler_norm_add x y : algR_norm (x + y) <= (algR_norm x + algR_norm y).
Expand All @@ -58,8 +45,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 +58,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.isNumRing.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 +73,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 +183,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 +248,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.
28 changes: 20 additions & 8 deletions theories/xmathcomp/char0.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_algebra all_field.

Set Implicit Arguments.
Expand Down Expand Up @@ -45,16 +46,12 @@ Hypothesis charF0 : has_char0 F.

Local Notation ratrF := (char0_ratr charF0).

Fact char0_ratr_is_rmorphism : rmorphism ratrF.
Fact char0_ratr_is_additive : additive ratrF.
Proof.
rewrite /char0_ratr.
have injZtoQ: @injective rat int intr by apply: intr_inj.
have nz_den x: (denq x)%:~R != 0 :> F by rewrite char0_intr_eq0 // denq_eq0.
do 2?split; rewrite /ratr ?divr1 // => x y; last first.
rewrite mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA.
do 2!apply: canRL (mulfK (nz_den _)) _; rewrite -!rmorphM; congr _%:~R.
apply: injZtoQ; rewrite !rmorphM [x * y]lock /= !numqE -lock.
by rewrite -!mulrA mulrA mulrCA -!mulrA (mulrCA y).
rewrite /ratr ?divr1 // => x y.
apply: (canLR (mulfK (nz_den _))); apply: (mulIf (nz_den x)).
rewrite mulrAC mulrBl divfK ?nz_den // mulrAC -!rmorphM.
apply: (mulIf (nz_den y)); rewrite mulrAC mulrBl divfK ?nz_den //.
Expand All @@ -63,8 +60,23 @@ rewrite !(rmorphM, rmorphB) [_ - _]lock /= -lock !numqE.
by rewrite (mulrAC y) -!mulrBl -mulrA mulrAC !mulrA.
Qed.

Canonical char0_ratr_additive := Additive char0_ratr_is_rmorphism.
Canonical char0_ratr_rmorphism := RMorphism char0_ratr_is_rmorphism.
Fact char0_ratr_is_multiplicative : multiplicative ratrF.
Proof.
rewrite /char0_ratr.
have injZtoQ: @injective rat int intr by apply: intr_inj.
have nz_den x: (denq x)%:~R != 0 :> F by rewrite char0_intr_eq0 // denq_eq0.
split; rewrite /ratr ?divr1 // => x y.
rewrite mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA.
do 2!apply: canRL (mulfK (nz_den _)) _; rewrite -!rmorphM; congr _%:~R.
apply: injZtoQ; rewrite !rmorphM [x * y]lock /= !numqE -lock.
by rewrite -!mulrA mulrA mulrCA -!mulrA (mulrCA y).
Qed.

HB.instance Definition _ := GRing.isAdditive.Build [zmodType of rat] F ratrF
char0_ratr_is_additive.
HB.instance Definition _ :=
GRing.isMultiplicative.Build [ringType of rat] F ratrF
char0_ratr_is_multiplicative.

End Char0MorphismsField.

Expand Down
Loading

0 comments on commit 837ad43

Please sign in to comment.