Merge pull request math-comp#1280 from hivert/morph-notations

Cleanup doc + standardize ssralg morphism notations

Author: CohenCyril

mathcomp/algebra/mxpoly.v

@@ -494,7 +494,7 @@ have bij_phi: bijective phi.
   by case: leqP => // P_le_k; rewrite nth_default ?mxE.
 pose phiaM := GRing.isAdditive.Build _ _ phi phi_is_additive.
 pose phimM := GRing.isMultiplicative.Build _ _ phi phi_is_multiplicative.
-pose phiRM : GRing.RMorphism.type _ _ := HB.pack phi phiaM phimM.
+pose phiRM : {rmorphism _ -> _} := HB.pack phi phiaM phimM.
 exists phiRM; split=> // [p | A]; apply/polyP=> k; apply/matrixP=> i j.
   by rewrite coef_phi coef_map !mxE coefMn.
 by rewrite coef_phi !mxE !coefC; case k; last rewrite /= mxE.

mathcomp/algebra/rat.v

@@ -839,7 +839,7 @@ Lemma rat_linear U V (f : U -> V) : additive f -> scalable f.
 Proof.
 move=> fB a u.
 pose aM := GRing.isAdditive.Build U V f fB.
-pose phi : GRing.Additive.type U V := HB.pack f aM.
+pose phi : {additive U -> V} := HB.pack f aM.
 rewrite -[f]/(phi : _ -> _) -{2}[a]divq_num_den mulrC -scalerA.
 apply: canRL (scalerK _) _; first by rewrite intr_eq0 denq_neq0.
 rewrite 2!scaler_int -3!raddfMz /=.

mathcomp/algebra/ssralg.v

@@ -96,16 +96,24 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
 (*                            such that val is a ring morphism                *)
 (*                            The HB class is called SubField.                *)
 (*                                                                            *)
-(* Morphisms between the above structures:                                    *)
+(* Morphisms between the above structures (see below for details):            *)
 (*                                                                            *)
-(*     Additive.type U V == semi additive (resp. additive) functions between  *)
-(*                          nmodType (resp. zmodType) instances U and V       *)
-(*    RMorphism.type R S == semi ring (resp. ring) morphism between           *)
-(*                          semiRingType (resp. ringType) instances R and S   *)
+(*     {additive U -> V} == semi additive (resp. additive) functions between  *)
+(*                          nmodType (resp. zmodType) instances U and V. This *)
+(*                          is a notation for the HB type Additive.type U V   *)
+(*    {rmorphism R -> S} == semi ring (resp. ring) morphism between           *)
+(*                          semiRingType (resp. ringType) instances R and S.  *)
+(*                          notation for RMorphism.type R S                   *)
 (*   GRing.Scale.law R V == scaling morphism : R -> V -> V                    *)
 (*                          The HB class is called GRing.Scale.Law.           *)
-(*     Linear.type R U V == linear functions : U -> V                         *)
-(* LRMorphism.type R A B == linear ring morphisms, i.e., algebra morphisms    *)
+(*     {linear U -> V}   == linear functions : U -> V, notation for           *)
+(*                          @Linear.type R U V s where the base ring R and    *)
+(*                          the scaling map s are inferred from the L-module  *)
+(*                          structure of U and V                              *)
+(*   {lrmorphism A -> B} == linear ring morphisms, i.e., algebra morphisms    *)
+(*                          notation for @LRMorphism.type R A B s where the   *)
+(*                          base ring R and scaling map s are inferred from   *)
+(*                          L-algebra structures of A and B                   *)
 (*                                                                            *)
 (* Closedness predicates for the algebraic structures:                        *)
 (*                                                                            *)
@@ -141,7 +149,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
 (*                  The HB class is called DivalgClosed.                      *)
 (*                                                                            *)
 (* Canonical properties of the algebraic structures:                          *)
-(*  * nmodType (additive abelian monoids):                                    *)
+(*  * NmodType (additive abelian monoids):                                    *)
 (*                     0 == the zero (additive identity) of a Nmodule         *)
 (*                 x + y == the sum of x and y (in a Nmodule)                 *)
 (*                x *+ n == n times x, with n in nat (non-negative), i.e.,    *)
@@ -157,7 +165,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
 (*                          base type is a nmodType and whose predicate's is  *)
 (*                          a nmodClosed                                      *)
 (*                                                                            *)
-(*  * zmodType (additive abelian groups):                                     *)
+(*  * ZmodType (additive abelian groups):                                     *)
 (*                   - x == the opposite (additive inverse) of x              *)
 (*                 x - y == the difference of x and y; this is only notation  *)
 (*                          for x + (- y)                                     *)

mathcomp/field/algebraics_fundamentals.v

@@ -610,7 +610,7 @@ have some_realC: realC.
       exact: can2_rmorphism (inj_can_sym QfK (fmorph_inj _)) QfK.
     pose faM := GRing.isAdditive.Build _ _ _ fA.
     pose fmM := GRing.isMultiplicative.Build _ _ _ fM.
-    pose fRM : GRing.RMorphism.type _ _ := HB.pack f faM fmM.
+    pose fRM : {rmorphism _ -> _} := HB.pack f faM fmM.
     by exists 0, rat; exact: fRM.
   have /Fadjoin1_polyP/sig_eqW[q]: x \in <<1; 0>>%VS by rewrite -sQof2 rmorph0.
   by exists q.[0]; rewrite -horner_map rmorph0.
@@ -886,7 +886,7 @@ have conjM : multiplicative conj.
   by rewrite /conj -/n1 -(rmorph1 (ofQ (z_ n1))) /conj_ ofQ_K !rmorph1.
 have conjaM := GRing.isAdditive.Build _ _ _ conjA.
 have conjmM := GRing.isMultiplicative.Build _ _ _ conjM.
-pose conjRM : GRing.RMorphism.type _ _ := HB.pack conj conjaM conjmM.
+pose conjRM : {rmorphism _ -> _} := HB.pack conj conjaM conjmM.
 exists conjRM => [z | /(_ i)/eqP/idPn[]] /=.
   by have [n [/conjE-> /(conjK (n_ z))->]] := maxn3 (n_ (conj z)) (n_ z) 0.
 rewrite /conj/conj_ cj_i rmorphN inQ_K // eq_sym -addr_eq0 -mulr2n -mulr_natl.

mathcomp/field/algnum.v

@@ -218,7 +218,7 @@ have nu0m : multiplicative nu0.
   by rewrite !rmorphM /= !QnC_nu0.
 pose nu0aM := GRing.isAdditive.Build Qn Qn nu0 nu0a.
 pose nu0mM := GRing.isMultiplicative.Build Qn Qn nu0 nu0m.
-pose nu0RM : GRing.RMorphism.type _ _ := HB.pack nu0 nu0aM nu0mM.
+pose nu0RM : {rmorphism _ -> _} := HB.pack nu0 nu0aM nu0mM.
 pose nu0lM := GRing.isScalable.Build rat Qn Qn *:%R nu0 (fmorph_numZ nu0RM).
 pose nu0LRM : {lrmorphism _ -> _} := HB.pack nu0 nu0aM nu0mM nu0lM.
 by exists nu0LRM.
@@ -496,7 +496,7 @@ have pzn_zk0: root (map_poly \1%VF (minPoly 1 zn)) (zn ^+ k).
 have phim : multiplicative phi.
   by apply/kHom_lrmorphism; rewrite -genQn span_seq1 /= kHomExtendP.
 pose phimM := GRing.isMultiplicative.Build _ _ phi phim.
-pose phiRM : GRing.RMorphism.type _ _ := HB.pack (fun_of_lfun phi) phimM.
+pose phiRM : {rmorphism _ -> _} := HB.pack (fun_of_lfun phi) phimM.
 have [nu Dnu] := extend_algC_subfield_aut QnC phiRM.
 exists nu => _ /(prim_rootP prim_z)[i ->].
 rewrite rmorphXn /= exprAC -Dz -Dnu /= -{1}[zn]hornerX /phi.

mathcomp/field/closed_field.v

@@ -882,7 +882,7 @@ have EtoKMul i : multiplicative (EtoK i : E i -> Kfield).
   by split=> [x y|]; rewrite ?EtoK_M ?EtoK_1.
 pose EtoKMa i := GRing.isAdditive.Build _ _ _ (EtoKAdd i).
 pose EtoKMm i := GRing.isMultiplicative.Build _ _ _ (EtoKMul i).
-pose EtoKM i : GRing.RMorphism.type _ _ :=
+pose EtoKM i : {rmorphism _ -> _} :=
   HB.pack (EtoK i : E i -> Kfield) (EtoKMa i) (EtoKMm i).
 have EtoK_E: EtoK _ = EtoKM _ by [].
 have toEtoKp := @eq_map_poly _ Kring _ _(toEtoK _ _ _).

mathcomp/field/galois.v

@@ -278,7 +278,7 @@ Lemma kAutf_lker0 K f : kHom K {:L} f -> lker f == 0%VS.
 Proof.
 move/(kHomSl (sub1v _))/kHom_lrmorphism=> fM.
 pose fmM := GRing.isMultiplicative.Build _ _ _ fM.
-pose fRM : GRing.RMorphism.type _ _ := HB.pack (fun_of_lfun f) fmM.
+pose fRM : {rmorphism _ -> _} := HB.pack (fun_of_lfun f) fmM.
 by apply/lker0P; apply: (fmorph_inj fRM).
 Qed.
 
@@ -496,7 +496,7 @@ rewrite -DhomEz; apply/kAHomP => _ /Fadjoin_polyP[q Eq ->].
 have homLfj: kHom E {:L} fj := comp_kHom (inv_kHomf homLfi) homLf.
 have /kHom_lrmorphism fjM := kHomSl (sub1v _) homLfj.
 pose fjmM := GRing.isMultiplicative.Build _ _ _ fjM.
-pose fjRM : GRing.RMorphism.type _ _ := HB.pack (fun_of_lfun fj) fjmM.
+pose fjRM : {rmorphism _ -> _} := HB.pack (fun_of_lfun fj) fjmM.
 rewrite -[fj _](horner_map fjRM) (kHom_poly_id homLfj) //=.
 by rewrite (@lfunE _ _ L) /= Dfz -fi_z lker0_lfunK.
 Qed.