Skip to content

Commit c16d2b0

Browse files
proux01proux01
authored
Merge pull request math-comp#1281 from math-comp/ssralg-doc
Fix the header documentation of ssralg.v
2 parents f8506ef + e9cdaad commit c16d2b0

File tree

1 file changed

+87
-75
lines changed

1 file changed

+87
-75
lines changed

‎mathcomp/algebra/ssralg.v

+87-75
Original file line numberDiff line numberDiff line change
@@ -98,22 +98,29 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
9898
(* *)
9999
(* Morphisms between the above structures (see below for details): *)
100100
(* *)
101-
(* {additive U -> V} == semi additive (resp. additive) functions between *)
102-
(* nmodType (resp. zmodType) instances U and V. This *)
103-
(* is a notation for the HB type Additive.type U V *)
104-
(* {rmorphism R -> S} == semi ring (resp. ring) morphism between *)
105-
(* semiRingType (resp. ringType) instances R and S. *)
106-
(* notation for RMorphism.type R S *)
107-
(* GRing.Scale.law R V == scaling morphism : R -> V -> V *)
108-
(* The HB class is called GRing.Scale.Law. *)
109-
(* {linear U -> V} == linear functions : U -> V, notation for *)
110-
(* @Linear.type R U V s where the base ring R and *)
111-
(* the scaling map s are inferred from the L-module *)
112-
(* structure of U and V *)
113-
(* {lrmorphism A -> B} == linear ring morphisms, i.e., algebra morphisms *)
114-
(* notation for @LRMorphism.type R A B s where the *)
115-
(* base ring R and scaling map s are inferred from *)
116-
(* L-algebra structures of A and B *)
101+
(* {additive U -> V} == semi additive (resp. additive) functions between*)
102+
(* nmodType (resp. zmodType) instances U and V. *)
103+
(* The HB class is called Additive. *)
104+
(* {rmorphism R -> S} == semi ring (resp. ring) morphism between *)
105+
(* semiRingType (resp. ringType) instances R and S.*)
106+
(* The HB class is called RMorphism. *)
107+
(* {linear U -> V | s} == linear functions of type U -> V, where U is a *)
108+
(* left module over a ring R, V is a Z-module, and *)
109+
(* s is a scaling operator of type R -> V -> V. *)
110+
(* The HB class is called Linear. *)
111+
(* {lrmorphism A -> B | s} == linear ring morphisms of type A -> B, where A *)
112+
(* is a left algebra over a ring R, B is a ring, *)
113+
(* and s is a scaling operator of type R -> B -> B.*)
114+
(* The HB class is called LRMorphism. *)
115+
(* *)
116+
(* -> The scaling operator s above should be one of *:%R, *%R, or a *)
117+
(* combination nu \; *:%R or nu \; *%R with a ring morphism nu; otherwise *)
118+
(* some of the theory (e.g., the linearZ rule) will not apply. To enable *)
119+
(* the overloading of the scaling operator, we use the following *)
120+
(* structures: *)
121+
(* *)
122+
(* GRing.Scale.law R V == scaling morphisms of type R -> V -> V *)
123+
(* The HB class is called Scale.Law. *)
117124
(* *)
118125
(* Closedness predicates for the algebraic structures: *)
119126
(* *)
@@ -149,7 +156,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
149156
(* The HB class is called DivalgClosed. *)
150157
(* *)
151158
(* Canonical properties of the algebraic structures: *)
152-
(* * NmodType (additive abelian monoids): *)
159+
(* * Nmodule (additive abelian monoids): *)
153160
(* 0 == the zero (additive identity) of a Nmodule *)
154161
(* x + y == the sum of x and y (in a Nmodule) *)
155162
(* x *+ n == n times x, with n in nat (non-negative), i.e., *)
@@ -165,7 +172,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
165172
(* base type is a nmodType and whose predicate's is *)
166173
(* a nmodClosed *)
167174
(* *)
168-
(* * ZmodType (additive abelian groups): *)
175+
(* * Zmodule (additive abelian groups): *)
169176
(* - x == the opposite (additive inverse) of x *)
170177
(* x - y == the difference of x and y; this is only notation *)
171178
(* for x + (- y) *)
@@ -179,23 +186,23 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
179186
(* is a zmodClosed *)
180187
(* *)
181188
(* * SemiRing (non-commutative semirings): *)
182-
(* R^c == the converse Ring for R: R^c is convertible to R *)
183-
(* but when R has a canonical ringType structure *)
184-
(* R^c has the converse one: if x y : R^c, then *)
185-
(* x * y = (y : R) * (x : R) *)
186-
(* 1 == the multiplicative identity element of a Ring *)
187-
(* n%:R == the ring image of an n in nat; this is just *)
189+
(* R^c == the converse (semi)ring for R: R^c is convertible*)
190+
(* to R but when R has a canonical (semi)RingType *)
191+
(* structure R^c has the converse one: *)
192+
(* if x y : R^c, then x * y = (y : R) * (x : R) *)
193+
(* 1 == the multiplicative identity element of a semiring*)
194+
(* n%:R == the semiring image of an n in nat; this is just *)
188195
(* notation for 1 *+ n, so 1%:R is convertible to 1 *)
189196
(* and 2%:R to 1 + 1 *)
190197
(* <number> == <number>%:R with <number> a sequence of digits *)
191-
(* x * y == the ring product of x and y *)
192-
(* \prod_<range> e == iterated product for a ring (cf bigop.v) *)
198+
(* x * y == the semiring product of x and y *)
199+
(* \prod_<range> e == iterated product for a semiring (cf bigop.v) *)
193200
(* x ^+ n == x to the nth power with n in nat (non-negative), *)
194201
(* i.e., x * (x * .. (x * x)..) (n factors); x ^+ 1 *)
195202
(* is thus convertible to x, and x ^+ 2 to x * x *)
196203
(* GRing.comm x y <-> x and y commute, i.e., x * y = y * x *)
197204
(* GRing.lreg x <-> x if left-regular, i.e., *%R x is injective *)
198-
(* GRing.rreg x <-> x if right-regular, i.e., *%R x is injective *)
205+
(* GRing.rreg x <-> x if right-regular, i.e., *%R^~ x is injective *)
199206
(* [char R] == the characteristic of R, defined as the set of *)
200207
(* prime numbers p such that p%:R = 0 in R *)
201208
(* The set [char R] has at most one element, and is *)
@@ -329,7 +336,6 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
329336
(* is simply notation for k *: 1 *)
330337
(* subalg_closed S <-> collective predicate S is closed under lalgType *)
331338
(* operations (1, a *: u + v and u * v in S) *)
332-
(* [lalgMixin of V by <:] == mixin axiom for a subType of an lalgType *)
333339
(* [SubRing_SubLmodule_isSubLalgebra of V by <:] == *)
334340
(* [SubChoice_isSubLalgebra of V by <:] == mixin axiom for a subType of an *)
335341
(* lalgType *)
@@ -362,6 +368,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
362368
(* canonical nmodType instances *)
363369
(* When both U and V have zmodType instances, it is *)
364370
(* an additive function. *)
371+
(* := GRing.Additive.type U V *)
365372
(* *)
366373
(* * RMorphism (semiring or ring morphisms): *)
367374
(* multiplicative f <-> f of type R -> S is multiplicative, i.e., f *)
@@ -372,6 +379,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
372379
(* R and S must have semiRingType instances *)
373380
(* When both R and S have ringType instances, it is *)
374381
(* a ring morphism. *)
382+
(* := GRing.RMorphism.type R S *)
375383
(* *)
376384
(* -> If R and S are UnitRings the f also maps units to units and inverses *)
377385
(* of units to inverses; if R is a field then f is a field isomorphism *)
@@ -385,42 +393,47 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
385393
(* /= every time one switched from additive to multiplicative rules. *)
386394
(* *)
387395
(* * Linear (linear functions): *)
396+
(* scalable_for s f <-> f of type U -> V is scalable for the scaling *)
397+
(* operator s of type R -> V -> V, i.e., *)
398+
(* f morphs a *: _ to s a _; R, U, and V must be a *)
399+
(* ringType, an lmodType R, and a zmodType, *)
400+
(* respectively. *)
401+
(* := forall a, {morph f : u / a *: u >-> s a u} *)
388402
(* scalable f <-> f of type U -> V is scalable, i.e., f morphs *)
389-
(* scaling on U to scaling on V, a *: _ to a *: _ *)
390-
(* U and V must both have lmodType R structures, *)
391-
(* for the same ringType R. *)
392-
(* scalable_for s f <-> f is scalable for scaling operator s, i.e., *)
393-
(* f morphs a *: _ to s a _; the range of f only *)
394-
(* need to be a zmodType *)
395-
(* The scaling operator s should be one of *:%R *)
396-
(* (see scalable, above), *%R or a combination *)
397-
(* nu \; *%R or nu \; *:%R with nu : {rmorphism _}; *)
398-
(* otherwise some of the theory (e.g., the linearZ *)
399-
(* rule) will not apply. *)
400-
(* linear f <-> f of type U -> V is linear, i.e., f morphs *)
401-
(* linear combinations a *: u + v in U to similar *)
402-
(* linear combinations in V; U and V must both have *)
403-
(* lmodType R structures, for the same ringType R *)
404-
(* := forall a, {morph f: u v / a *: u + v} *)
403+
(* scaling on U to scaling on V, a *: _ to a *: _; *)
404+
(* U and V must be an lmodType R for the same *)
405+
(* ringType R. *)
406+
(* := scalable_for *:%R f *)
407+
(* linear_for s f <-> f of type U -> V is linear for s of type *)
408+
(* R -> V -> V, i.e., *)
409+
(* f (a *: u + v) = s a (f u) + f v; *)
410+
(* R, U, and V must be a ringType, an lmodType R, *)
411+
(* and a zmodType, respectively. *)
412+
(* linear f <-> f of type U -> V is linear, i.e., *)
413+
(* f (f *: u + v) = a *: f u + f v; *)
414+
(* U and V must be lmodType R for the same *)
415+
(* ringType R. *)
416+
(* := linear_for *:%R f *)
405417
(* scalar f <-> f of type U -> R is a scalar function, i.e., *)
406-
(* f (a *: u + v) = a * f u + f v *)
407-
(* linear_for s f <-> f is linear for the scaling operator s, i.e., *)
408-
(* f (a *: u + v) = s a (f u) + f v *)
409-
(* The range of f only needs to be a zmodType, but *)
410-
(* s MUST be of the form described in the *)
411-
(* scalable_for paragraph above for this predicate *)
412-
(* to type check. *)
413-
(* lmorphism f <-> f is both additive and scalable *)
414-
(* This is in fact equivalent to linear f, although *)
415-
(* somewhat less convenient to prove. *)
416-
(* lmorphism_for s f <-> f is both additive and scalable for s *)
417-
(* {linear U -> V} == the interface type for linear functions, i.e., a *)
418-
(* Structure that encapsulates the linear property *)
419-
(* for functions f : U -> V; both U and V must have *)
420-
(* lmodType R structures, for the same R *)
421-
(* {scalar U} == the interface type for scalar functions, of type *)
422-
(* U -> R where U has an lmodType R structure *)
423-
(* {linear U -> V | s} == the interface type for functions linear for s *)
418+
(* f (a *: u + v) = a * f u + f v; *)
419+
(* R and U must be a ringType and an lmodType R, *)
420+
(* respectively. *)
421+
(* := linear_for *%R f *)
422+
(* {linear U -> V | s} == the interface type for functions linear for the *)
423+
(* scaling operator s of type R -> V -> V, i.e., a *)
424+
(* structure that encapsulates two properties *)
425+
(* semi_additive f and scalable_for s f for *)
426+
(* functions f : U -> V; R, U, and V must be a *)
427+
(* ringType, an lmodType R, and a zmodType, *)
428+
(* respectively *)
429+
(* := @GRing.Linear.type R U V s *)
430+
(* {linear U -> V} == the interface type for linear functions, of type *)
431+
(* U -> V where both U and V must be lmodType R for *)
432+
(* the same ringType R *)
433+
(* := {linear U -> V | *:%R} *)
434+
(* {scalar U} == the interface type for scalar functions of type *)
435+
(* U -> R where U must be an lmodType R *)
436+
(* := {linear U -> V | *%R} *)
424437
(* (a *: u)%Rlin == transient forms that simplify to a *: u, a * u, *)
425438
(* (a * u)%Rlin nu a *: u, and nu a * u, respectively, and are *)
426439
(* (a *:^nu u)%Rlin created by rewriting with the linearZ lemma *)
@@ -444,19 +457,18 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
444457
(* parameter of linearZ is a proper sub-interface of {linear fUV | s}. *)
445458
(* *)
446459
(* * LRMorphism (linear ring morphisms, i.e., algebra morphisms): *)
447-
(* lrmorphism f <-> f of type A -> B is a linear Ring (Algebra) *)
448-
(* morphism: f is both additive, multiplicative and *)
449-
(* scalable; A and B must both have lalgType R *)
450-
(* canonical structures, for the same ringType R *)
451-
(* lrmorphism_for s f <-> f a linear Ring morphism for the scaling *)
452-
(* operator s: f is additive, multiplicative and *)
453-
(* scalable for s; A must be an lalgType R, but B *)
454-
(* only needs to have a ringType structure *)
455-
(* {lrmorphism A -> B} == the interface type for linear morphisms, i.e., a *)
456-
(* Structure that encapsulates the lrmorphism *)
457-
(* property for functions f : A -> B; both A and B *)
458-
(* must have lalgType R structures, for the same R *)
459-
(* {lrmorphism A -> B | s} == the interface type for morphisms linear for s *)
460+
(* {lrmorphism A -> B | s} == the interface type for ring morphisms linear *)
461+
(* for the scaling operator s of type R -> B -> B, *)
462+
(* i.e., the join of ring morphisms *)
463+
(* {rmorphism A -> B} and linear functions *)
464+
(* {linear A -> B | s}; R, A, and B must be a *)
465+
(* ringType, an lalgType R, and a ringType, *)
466+
(* respectively *)
467+
(* := @GRing.LRMorphism.type R A B s *)
468+
(* {lrmorphism A -> B} == the interface type for algebra morphisms, where *)
469+
(* A and B must be lalgType R for the same ringType *)
470+
(* R *)
471+
(* := {lrmorphism A -> B | *:%R} *)
460472
(* -> Linear and rmorphism properties do not need to be specialized for *)
461473
(* as we supply inheritance join instances in both directions. *)
462474
(* Finally we supply some helper notation for morphisms: *)

0 commit comments

Comments
 (0)