Module mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras
From HB Require Import structures.From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
From mathcomp Require Import choice fintype finfun bigop prime binomial.
From mathcomp Require Import nmodule.
Ring-like structures
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
Reference: Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence
Rideau, Packaging mathematical structures, TPHOLs 2009
This file defines the following algebraic structures:
pzSemiRingType == non-commutative semi rings
(NModule with a multiplication)
The HB class is called PzSemiRing.
nzSemiRingType == non-commutative non-trivial semi rings
(NModule with a multiplication)
The HB class is called NzSemiRing.
comPzSemiRingType == commutative semi rings
The HB class is called ComPzSemiRing.
comNzSemiRingType == commutative non-trivial semi rings
The HB class is called ComNzSemiRing.
pzRingType == non-commutative rings
(semi rings with an opposite)
The HB class is called PzRing.
nzRingType == non-commutative non-trivial rings
(semi rings with an opposite)
The HB class is called NzRing.
comPzRingType == commutative rings
The HB class is called ComPzRing.
comNzRingType == commutative non-trivial rings
The HB class is called ComNzRing.
lSemiModType R == semimodule with left multiplication by external scalars
in the semiring R
The HB class is called LSemiModule.
lmodType R == module with left multiplication by external scalars
in the pzRing R
The HB class is called Lmodule.
pzLSemiAlgType R == left semialgebra, semiring with scaling that
associates on the left
The HB class is called PzLSemiAlgebra.
nzLSemiAlgType R == non-trivial left semialgebra
The HB class is called NzLSemiAlgebra.
pzLalgType R == left algebra, ring with scaling that associates on the
left
The HB class is called PzLalgebra.
nzLalgType R == non-trivial left algebra
The HB class is called NzLalgebra.
pzSemiAlgType R == semialgebra, semiring with scaling that associates both
left and right
The HB class is called PzSemiAlgebra.
nzSemiAlgType R == non-trivial semialgebra
The HB class is called NzSemiAlgebra.
pzAlgType R == algebra, ring with scaling that associates both left
and right
The HB class is called PzAlgebra.
nzAlgType R == non-trivial algebra
The HB class is called NzAlgebra.
comPzSemiAlgType R == commutative pzSemiAlgType
The HB class is called ComPzSemiAlgebra.
comNzSemiAlgType R == commutative nzSemiAlgType
The HB class is called ComNzSemiAlgebra.
comPzAlgType R == commutative pzAlgType
The HB class is called ComPzAlgebra.
comNzAlgType R == commutative nzAlgType
The HB class is called ComNzAlgebra.
and their joins with subType:
subPzSemiRingType R P == join of pzSemiRingType and
subType (P : pred R) such that val is a
semiring morphism
The HB class is called SubPzSemiRing.
subNzSemiRingType R P == join of nzSemiRingType and
subType (P : pred R) such that val is a
semiring morphism
The HB class is called SubNzSemiRing.
(*subComPzSemiRingType R P == join of comPzSemiRingType and
subType (P : pred R) such that val is a morphism
The HB class is called SubComPzSemiRing.
(*subComNzSemiRingType R P == join of comNzSemiRingType and
subType (P : pred R) such that val is a morphism
The HB class is called SubComNzSemiRing.
subPzRingType R P == join of pzRingType and subType (P : pred R)
such that val is a morphism
The HB class is called SubPzRing.
subComPzRingType R P == join of comPzRingType and subType (P : pred R)
such that val is a morphism
The HB class is called SubComPzRing.
subNzRingType R P == join of nzRingType and subType (P : pred R)
such that val is a morphism
The HB class is called SubNzRing.
subComNzRingType R P == join of comNzRingType and subType (P : pred R)
such that val is a morphism
The HB class is called SubComNzRing.
subLSemiModType R V P == join of lSemiModType and subType (P : pred V)
such that val is scalable
The HB class is called SubLSemiModule.
subLmodType R V P == join of lmodType and subType (P : pred V)
such that val is scalable
The HB class is called SubLmodule.
subPzLSemiAlgType R V P == join of pzLSemiAlgType and subType (P : pred V)
such that val is linear
The HB class is called SubPzLSemiAlgebra.
subNzLSemiAlgType R V P == join of nzLSemiAlgType and subType (P : pred V)
such that val is linear
The HB class is called SubNzLSemiAlgebra.
subPzLalgType R V P == join of pzLalgType and subType (P : pred V)
such that val is linear
The HB class is called SubPzLalgebra.
subNzLalgType R V P == join of nzLalgType and subType (P : pred V)
such that val is linear
The HB class is called SubNzLalgebra.
subPzSemiAlgType R V P == join of pzSemiAlgType and subType (P : pred V)
such that val is linear
The HB class is called SubPzSemiAlgebra.
subNzSemiAlgType R V P == join of nzSemiAlgType and subType (P : pred V)
such that val is linear
The HB class is called SubNzSemiAlgebra.
subPzAlgType R V P == join of pzAlgType and subType (P : pred V)
such that val is linear
The HB class is called SubPzAlgebra.
subNzAlgType R V P == join of nzAlgType and subType (P : pred V)
such that val is linear
The HB class is called SubNzAlgebra.
Morphisms between the above structures (see below for details):
{rmorphism R -> S} == semi ring (resp. ring) morphism between
pzSemiRingType (resp. pzRingType) instances
R and S.
The HB class is called RMorphism.
{linear U -> V | s} == semilinear (resp. linear) functions of type
U -> V, where U is a left semimodule (resp.
left module) over semiring (resp. ring) R, V is
an N-module (resp. Z-module), and s is a scaling
operator (detailed below) of type R -> V -> V.
The HB class is called Linear.
{lrmorphism A -> B | s} == semialgebra (resp. algebra) morphisms of type
A -> B, where A is a left semialgebra
(resp. left algebra) over semiring (resp. ring)
R, B is an semiring (resp. ring), and s is a
scaling operator (detailed below) of type
R -> B -> B.
The HB class is called LRMorphism.
-> The scaling operator s above should be one of *:%R, *%R, or a
combination nu \; *:%R or nu \; *%R with a semiring morphism nu;
otherwise some of the theory (e.g., the linearZ rule) will not apply.
To enable the overloading of the scaling operator, we use the following
structures:
GRing.Scale.preLaw R V == scaling morphisms of type R -> V -> V
The HB class is called Scale.PreLaw.
GRing.Scale.semiLaw R V == scaling morphisms of type R -> V -> V
The HB class is called Scale.SemiLaw.
GRing.Scale.law R V == scaling morphisms of type R -> V -> V
The HB class is called Scale.Law.
Closedness predicates for the algebraic structures:
mulr2Closed R == predicate closed under multiplication on
R : pzSemiRingType
The HB class is called Mul2Closed.
mulrClosed R == predicate closed under multiplication and for 1
The HB class is called MulClosed.
semiring2Closed R == predicate closed under addition and multiplication
The HB class is called Semiring2Closed.
semiringClosed R == predicate closed under semiring operations
The HB class is called SemiringClosed.
smulClosed R == predicate closed under multiplication and for -1
The HB class is called SmulClosed.
subringClosed R == predicate closed under ring operations
The HB class is called SubringClosed.
submodClosed R == predicate closed under lSemiModType operations
The HB class is called SubmodClosed.
subalgClosed R == predicate closed under pzLSemiAlgType operations
The HB class is called SubalgClosed.
The rpred* lemmas ensure that the set S remains stable under the specified
operations, provided the corresponding closedness predicate is satisfied.
This stability is crucial for constructing and reasoning about
substructures within algebraic hierarchies. For example:
- rpredZ: Concludes a *: v \in S if v \in S and S is scalerClosed.
Canonical properties of the algebraic structures:
* PzSemiRing (non-commutative semirings):
R^c == the converse (semi)ring for R: R^c is convertible
to R but when R has a canonical (semi)ring
structure R^c has the converse one:
if x y : R^c, then x * y = (y : R) * (x : R)
1 == the multiplicative identity element of a semiring
n%:R == the semiring image of an n in nat; this is just
notation for 1 *+ n, so 1%:R is convertible to 1
and 2%:R to 1 + 1
<number> == <number>%:R with <number> a sequence of digits
x * y == the semiring product of x and y
\prod_<range> e == iterated product for a semiring (cf bigop.v)
x ^+ n == x to the nth power with n in nat (non-negative),
i.e., x * (x * .. (x * x)..) (n factors); x ^+ 1
is thus convertible to x, and x ^+ 2 to x * x
GRing.comm x y <-> x and y commute, i.e., x * y = y * x
GRing.lreg x <-> x if left-regular, i.e., *%R x is injective
GRing.rreg x <-> x if right-regular, i.e., *%R^~ x is injective
[pchar R] == the characteristic of R, defined as the set of
prime numbers p such that p%:R = 0 in R
The set [pchar R] has at most one element, and is
implemented as a pred_nat collective predicate
(see prime.v); thus the statement p \in [pchar R]
can be read as `R has characteristic p', while
[pchar R] =i pred0 means `R has characteristic 0'
when R is a field.
pFrobenius_aut chRp == the Frobenius automorphism mapping x in R to
x ^+ p, where chRp : p \in [pchar R] is a proof
that R has (non-zero) characteristic p
mulr_closed S <-> collective predicate S is closed under finite
products (1 and x * y in S for x, y in S)
semiring_closed S <-> collective predicate S is closed under semiring
operations (0, 1, x + y and x * y in S)
[SubNmodule_isSubPzSemiRing of R by <:] == pzSemiRingType mixin for a
subNmodType whose base type is a pzSemiRingType
and whose predicate is a mulrClosed
[SubChoice_isSubPzSemiRing of R by <:] == pzSemiRingType mixin for a
subType whose base type is a pzSemiRingType and
whose predicate is a semiringClosed
* NzSemiRing (non-commutative non-trivial semirings):
[SubNmodule_isSubNzSemiRing of R by <:] == nzSemiRingType mixin for a
subNmodType whose base type is a nzSemiRingType
and whose predicate is a mulrClosed
[SubChoice_isSubNzSemiRing of R by <:] == nzSemiRingType mixin for a
subType whose base type is a nzSemiRingType and
whose predicate is a semiringClosed
* PzRing (non-commutative rings):
GRing.sign R b := (-1) ^+ b in R : pzRingType, with b : bool
This is a parsing-only helper notation, to be
used for defining more specific instances.
smulr_closed S <-> collective predicate S is closed under products
and opposite (-1 and x * y in S for x, y in S)
subring_closed S <-> collective predicate S is closed under ring
operations (1, x - y and x * y in S)
[SubChoice_isSubPzRing of R by <:] == pzRingType mixin for a subType whose
base type is a pzRingType and whose predicate is
a subringClosed
* NzRing (non-commutative non-trivial rings):
[SubChoice_isSubNzRing of R by <:] == nzRingType mixin for a subType whose
base type is a nzRingType and whose predicate is
a subringClosed
* ComPzSemiRing (commutative PzSemiRings):
[SubChoice_isSubComPzSemiRing of R by <:] == comPzSemiRingType mixin for a
subType whose base type is a comPzSemiRingType
and whose predicate is a semiringClosed
* ComNzSemiRing (commutative NzSemiRings):
[SubChoice_isSubComNzSemiRing of R by <:] == comNzSemiRingType mixin for a
subType whose base type is a comNzSemiRingType
and whose predicate is a semiringClosed
* ComPzRing (commutative PzRings):
[SubChoice_isSubComPzRing of R by <:] == comPzRingType mixin for a
subType whose base type is a comPzRingType and
whose predicate is a subringClosed
* ComNzRing (commutative NzRings):
[SubChoice_isSubComNzRing of R by <:] == comNzRingType mixin for a
subType whose base type is a comNzRingType and
whose predicate is a subringClosed
* LSemiModule (semimodule with left multiplication by external scalars).
a *: v == v scaled by a, when v is in an LSemiModule V and
a is in the scalar semiring of V
scaler_closed S <-> collective predicate S is closed under scaling
subsemimod_closed S <-> collective predicate S is closed under
lSemiModType operations (0, +%R, and *:%R)
[SubNmodule_isSubLSemiModule of V by <:] ==
[SubChoice_isSubLSemiModule of V by <:] == mixin axiom for a subType of an
lSemiModType
* Lmodule (module with left multiplication by external scalars).
linear_closed S <-> collective predicate S is closed under linear
combinations (a *: u + v in S when u, v in S)
submod_closed S <-> collective predicate S is closed under lmodType
operations (0 and a *: u + v in S)
[SubChoice_isSubLmodule of V by <:] == mixin axiom for a subType of an
lmodType
* PzLSemiAlgebra
(left semialgebra, semiring with scaling that associates on the left):
R^o == the regular (semi)algebra of R: R^o is
convertible to R, but when R has a (semi)ring
structure then R^o extends it to a left
(semi)algebra structure by letting R act on
itself: if x : R and y : R^o then
x *: y = x * (y : R)
k%:A == the image of the scalar k in a left semialgebra;
this is simply notation for k *: 1
subsemialg_closed S <-> collective predicate S is closed under
lSemiAlgType operations
(0, 1, +%R, *%R, and *:%R)
[SubSemiRing_SubLSemiModule_isSubLSemiAlgebra of V by <:]
[SubChoice_isSubPzLSemiAlgebra of V by <:] == mixin axiom for a subType of
a pzLSemiAlgType
* PzLalgebra
(left algebra, ring with scaling that associates on the left):
subalg_closed S <-> collective predicate S is closed under
pzLalgType operations
(1, a *: u + v and u * v in S)
[SubRing_SubLmodule_isSubLalgebra of V by <:] ==
[SubChoice_isSubPzLalgebra of V by <:] == mixin axiom for a subType of a
pzLalgType
* PzSemiAlgebra
(semiring with scaling that associates both left and right):
[SubLSemiAlgebra_isSubSemiAlgebra of V by <:] ==
[SubChoice_isSubPzSemiAlgebra of V by <:] == mixin axiom for a subType of
a pzSemiAlgType
* PzAlgebra (ring with scaling that associates both left and right):
[SubChoice_isSubPzAlgebra of V by <:] == mixin axiom for a subType of a
pzAlgType
In addition to this structure hierarchy, we also develop a separate,
parallel hierarchy for morphisms linking these structures:
* RMorphism (semiring or ring morphisms):
monoid_morphism f <-> f of type R -> S is a multiplicative monoid
morphism, i.e., f maps 1 and * in R to 1 and *
in S, respectively. R and S must have canonical
pzSemiRingType instances.
{rmorphism R -> S} == the interface type for semiring morphisms; both
R and S must have pzSemiRingType instances
When both R and S have pzRingType instances, it
is a ring morphism.
:= GRing.RMorphism.type R S
-> If R and S are UnitRings the f also maps units to units and inverses
of units to inverses; if R is a field then f is a field isomorphism
between R and its image.
-> Additive properties (raddf_suffix, see below) are duplicated and
specialised for RMorphism (as rmorph_suffix). This allows more
precise rewriting and cleaner chaining: although raddf lemmas will
recognize RMorphism functions, the converse will not hold (we cannot
add reverse inheritance rules because of incomplete backtracking in
the Canonical Projection unification), so one would have to insert a
/= every time one switched from additive to multiplicative rules.
* Linear (semilinear or linear functions):
scalable_for s f <-> f of type U -> V is scalable for the scaling
operator s of type R -> V -> V, i.e.,
f morphs a *: _ to s a _; R, U, and V must be a
pzSemiRingType, an lSemiModType R, and an
nmodType, respectively.
:= forall a, {morph f : u / a *: u >-> s a u}
scalable f <-> f of type U -> V is scalable, i.e., f morphs
scaling on U to scaling on V, a *: _ to a *: _;
U and V must be lSemiModType R for the same
pzSemiRingType R.
:= scalable_for *:%R f
semilinear_for s f <-> f of type U -> V is semilinear for s of type
R -> V -> V , i.e., f morphs a *: _ and addition
on U to s a _ and addition on V, respectively;
R, U, and V must be a pzSemiRingType, an
lSemiModType R and an nmodType, respectively.
:= scalable_for s f * {morph f : x y / x + y}
semilinear f <-> f of type U -> V is semilinear, i.e., f morphs
scaling and addition on U to scaling and
addition on V, respectively; U and V must be
lSemiModType R for the same pzSemiRingType R.
:= semilinear_for *:% f
semiscalar f <-> f of type U -> R is a semiscalar function,
i.e., f morphs scaling and addition on U to
multiplication and addition on R; R and U must
be a pzSemiRingType and an lSemiModType R,
respectively.
:= semilinear_for *%R f
linear_for s f <-> f of type U -> V is linear for s of type
R -> V -> V, i.e.,
f (a *: u + v) = s a (f u) + f v;
R, U, and V must be a pzRingType, an lmodType R,
and a zmodType, respectively.
linear f <-> f of type U -> V is linear, i.e.,
f (f *: u + v) = a *: f u + f v;
U and V must be lmodType R for the same
pzRingType R.
:= linear_for *:%R f
scalar f <-> f of type U -> R is a scalar function, i.e.,
f (a *: u + v) = a * f u + f v;
R and U must be a pzRingType and an lmodType R,
respectively.
:= linear_for *%R f
{linear U -> V | s} == the interface type for functions (semi)linear
for the scaling operator s of type R -> V -> V,
i.e., a structure that encapsulates two
properties semi_additive f and scalable_for s f
for functions f : U -> V; R, U, and V must be a
pzSemiRingType, an lSemiModType R, and an
nmodType, respectively.
{linear U -> V} == the interface type for (semi)linear functions,
of type U -> V where both U and V must be
lSemiModType R for the same pzSemiRingType R
:= {linear U -> V | *:%R}
{scalar U} == the interface type for (semi)scalar functions,
of type U -> R where U must be an lSemiModType R
:= {linear U -> R | *%R}
(a *: u)%Rlin == transient forms that simplify to a *: u, a * u,
(a * u)%Rlin nu a *: u, and nu a * u, respectively, and are
(a *:^nu u)%Rlin created by rewriting with the linearZ lemma
(a *^nu u)%Rlin The forms allows the RHS of linearZ to be matched
reliably, using the GRing.Scale.law structure.
-> Similarly to semiring morphisms, semiadditive properties are
specialized for semilinear functions.
-> Although {scalar U} is convertible to {linear U -> R^o}, it does not
actually use R^o, so that rewriting preserves the canonical structure
of the range of scalar functions.
-> The generic linearZ lemma uses a set of bespoke interface structures to
ensure that both left-to-right and right-to-left rewriting work even in
the presence of scaling functions that simplify non-trivially (e.g.,
idfun \; *%R). Because most of the canonical instances and projections
are coercions the machinery will be mostly invisible (with only the
{linear ...} structure and %Rlin notations showing), but users should
beware that in (a *: f u)%Rlin, a actually occurs in the f u subterm.
-> The simpler linearZ_LR, or more specialized linearZZ and scalarZ rules
should be used instead of linearZ if there are complexity issues, as
well as for explicit forward and backward application, as the main
parameter of linearZ is a proper sub-interface of {linear U -> V | s}.
* LRMorphism (semialgebra or algebra morphisms):
{lrmorphism A -> B | s} == the interface type for semiring (resp. ring)
morphisms semilinear (resp. linear) for the
scaling operator s of type R -> B -> B, i.e.,
the join of semiring (resp. ring) morphisms
{rmorphism A -> B} and semilinear (resp. linear)
functions {linear A -> B | s}; R, A, and B must
be a pzSemiRingType (resp. pzRingType), an
lSemiAlgType R (resp. lalgType R), and a
pzSemiRingType (resp. pzRingType), respectively
{lrmorphism A -> B} == the interface type for semialgebra (resp.
algebra) morphisms, where A and B must be
lSemiAlgType R (resp. lalgType R) for the same
pzSemiRingType (resp. pzRingType) R
:= {lrmorphism A -> B | *:%R}
-> Linear and rmorphism properties do not need to be specialized for
as we supply inheritance join instances in both directions.
Finally we supply some helper notation for morphisms:
x^f == the image of x under some morphism
This notation is only reserved (not defined)
here; it is bound locally in sections where some
morphism is used heavily (e.g., the container
morphism in the parametricity sections of poly
and matrix, or the Frobenius section here)
\0 == the constant null function, which has a
canonical linear structure, and simplifies on
application (see ssrfun.v)
f \+ g == the additive composition of f and g, i.e., the
function x |-> f x + g x; f \+ g is canonically
linear when f and g are, and simplifies on
application (see ssrfun.v)
f \- g == the function x |-> f x - g x, canonically
linear when f and g are, and simplifies on
application
\- g == the function x |-> - f x, canonically linear
when f is, and simplifies on application
k \*: f == the function x |-> k *: f x, which is
canonically linear when f is and simplifies on
application (this is a shorter alternative to
*:%R k \o f)
GRing.in_alg A == the ring morphism that injects R into A, where A
has an lalgType R structure; GRing.in_alg A k
simplifies to k%:A
a \*o f == the function x |-> a * f x, canonically linear
when f is and its codomain is an algType
and which simplifies on application
a \o* f == the function x |-> f x * a, canonically linear
when f is and its codomain is an lalgType
and which simplifies on application
f \* g == the function x |-> f x * g x; f \* g
simplifies on application
* Module layout, the notation scopes, and the naming convention
The following remarks apply to divalg.v and decfield.v, besides algebra.v.
The lemmas are contained in two modules: GRing and GRing.Theory. The
GRing module SHOULD NOT be imported and gives only qualified access to
definitions and lemmas, e.g., GRing.mul and GRing.mul0r. The GRing.Theory
submodule can be imported to obtain unqualified access to the lemmas and
some definitions, e.g., monoid_morphism.
The notations are defined in ring_scope (delimiter %R), except that the
notations for types, e.g., {rmorphism R -> S} and functions, e.g., *%R,
are respectively defined in type_scope and function_scope.
This library also extends the conventional suffixes described in library
ssrbool.v with the following:
0 -- ring 0, as in addr0 : x + 0 = x
1 -- ring 1, as in mulr1 : x * 1 = x
D -- ring addition, as in linearD : f (u + v) = f u + f v
B -- ring subtraction, as in opprB : - (x - y) = y - x
M -- ring multiplication, as in invfM : (x * y)^-1 = x^-1 * y^-1
Mn -- ring by nat multiplication, as in raddfMn : f (x *+ n) = f x *+ n
N -- ring opposite, as in mulNr : (- x) * y = - (x * y)
V -- ring inverse, as in mulVr : x^-1 * x = 1
X -- ring exponentiation, as in rmorphXn : f (x ^+ n) = f x ^+ n
Z -- (left) module scaling, as in linearZ : f (a *: v) = s *: f v
The operator suffixes D, B, M and X are also used for the corresponding
operations on nat, as in natrX : (m ^ n)%:R = m%:R ^+ n. For the binary
power operator, a trailing "n" suffix is used to indicate the operator
suffix applies to the left-hand ring argument, as in
expr1n : 1 ^+ n = 1 vs. expr1 : x ^+ 1 = x.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Reserved Notation "+%R".
Reserved Notation "-%R".
Reserved Notation "*%R" (format " *%R").
Reserved Notation "*:%R" (format " *:%R").
Reserved Notation "n %:R" (left associativity, format "n %:R").
Reserved Notation "k %:A" (left associativity, format "k %:A").
Reserved Notation "[ 'pchar' F ]" (format "[ 'pchar' F ]").
Reserved Notation "[ 'char' F ]" (format "[ 'char' F ]").
Reserved Notation "x %:T" (left associativity, format "x %:T").
Reserved Notation "''X_' i" (at level 8, i at level 2, format "''X_' i").
Reserved Notation "''exists' ''X_' i , f"
(at level 199, i at level 2, right associativity,
format "'[hv' ''exists' ''X_' i , '/ ' f ']'").
Reserved Notation "''forall' ''X_' i , f"
(at level 199, i at level 2, right associativity,
format "'[hv' ''forall' ''X_' i , '/ ' f ']'").
Reserved Notation "x ^f" (left associativity, format "x ^f").
Reserved Notation "\0".
Reserved Notation "f \+ g" (at level 50, left associativity).
Reserved Notation "f \- g" (at level 50, left associativity).
Reserved Notation "\- f" (at level 35, f at level 35).
Reserved Notation "a \*o f" (at level 40).
Reserved Notation "a \o* f" (at level 40).
Reserved Notation "a \*: f" (at level 40).
Reserved Notation "f \* g" (at level 40, left associativity).
Reserved Notation "'{' 'additive' U '->' V '}'"
(U at level 98, V at level 99, format "{ 'additive' U -> V }").
Reserved Notation "'{' 'rmorphism' U '->' V '}'"
(U at level 98, V at level 99, format "{ 'rmorphism' U -> V }").
Reserved Notation "'{' 'lrmorphism' U '->' V '|' s '}'"
(U at level 98, V at level 99, format "{ 'lrmorphism' U -> V | s }").
Reserved Notation "'{' 'lrmorphism' U '->' V '}'"
(U at level 98, V at level 99, format "{ 'lrmorphism' U -> V }").
Reserved Notation "'{' 'linear' U '->' V '|' s '}'"
(U at level 98, V at level 99, format "{ 'linear' U -> V | s }").
Reserved Notation "'{' 'linear' U '->' V '}'"
(U at level 98, V at level 99,
format "{ 'linear' U -> V }").
Reserved Notation "'{' 'scalar' U '}'" (format "{ 'scalar' U }").
Reserved Notation "R ^c" (format "R ^c").
Reserved Notation "R ^o" (format "R ^o").
Module Export Dummy.
Module GRing := Algebra.
End Dummy.
Module Import GRing.
Export Algebra.
Import Monoid.Theory.
HB.mixin Record Nmodule_isPzSemiRing R & Nmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul +%R;
mulrDr : right_distributive mul +%R;
mul0r : left_zero zero mul;
mulr0 : right_zero zero mul;
}.
#[short(type="pzSemiRingType")]
HB.structure Definition PzSemiRing :=
{ R of Nmodule_isPzSemiRing R & Nmodule R }.
HB.factory Record isPzSemiRing R & Choice R := {
zero : R;
add : R -> R -> R;
one : R;
mul : R -> R -> R;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
mul0r : left_zero zero mul;
mulr0 : right_zero zero mul;
}.
HB.builders Context R & isPzSemiRing R.
HB.instance Definition _ := @isNmodule.Build R
zero add addrA addrC add0r.
HB.instance Definition _ := @Nmodule_isPzSemiRing.Build R
one mul mulrA mul1r mulr1 mulrDl mulrDr mul0r mulr0.
HB.end.
Module PzSemiRingExports.
Bind Scope ring_scope with PzSemiRing.sort.
End PzSemiRingExports.
HB.export PzSemiRingExports.
HB.mixin Record PzSemiRing_isNonZero R & PzSemiRing R := {
oner_neq0 : @one R != 0
}.
#[short(type="nzSemiRingType")]
HB.structure Definition NzSemiRing :=
{ R of PzSemiRing_isNonZero R & PzSemiRing R }.
HB.factory Record Nmodule_isNzSemiRing R & Nmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul +%R;
mulrDr : right_distributive mul +%R;
mul0r : left_zero zero mul;
mulr0 : right_zero zero mul;
oner_neq0 : one != 0
}.
HB.builders Context R & Nmodule_isNzSemiRing R.
HB.instance Definition _ :=
Nmodule_isPzSemiRing.Build R mulrA mul1r mulr1 mulrDl mulrDr mul0r mulr0.
HB.instance Definition _ := PzSemiRing_isNonZero.Build R oner_neq0.
HB.end.
HB.factory Record isNzSemiRing R & Choice R := {
zero : R;
add : R -> R -> R;
one : R;
mul : R -> R -> R;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
mul0r : left_zero zero mul;
mulr0 : right_zero zero mul;
oner_neq0 : one != zero
}.
HB.builders Context R & isNzSemiRing R.
HB.instance Definition _ := @isNmodule.Build R
zero add addrA addrC add0r.
HB.instance Definition _ := @Nmodule_isNzSemiRing.Build R
one mul mulrA mul1r mulr1 mulrDl mulrDr mul0r mulr0 oner_neq0.
HB.end.
Module NzSemiRingExports.
Bind Scope ring_scope with NzSemiRing.sort.
End NzSemiRingExports.
HB.export NzSemiRingExports.
Definition exp R x n := iterop n (@mul R) x (@one R).
Arguments exp : simpl never.
Definition comm R x y := @mul R x y = mul y x.
Definition lreg R x := injective (@mul R x).
Definition rreg R x := injective ((@mul R)^~ x).
Local Notation "1" := (@one _) : ring_scope.
Local Notation "n %:R" := (1 *+ n) : ring_scope.
Local Notation "*%R" := (@mul _) : function_scope.
Local Notation "x * y" := (mul x y) : ring_scope.
Local Notation "x ^+ n" := (exp x n) : ring_scope.
Local Notation "\prod_ ( i <- r | P ) F" := (\big[*%R/1]_(i <- r | P) F).
Local Notation "\prod_ ( i | P ) F" := (\big[*%R/1]_(i | P) F).
Local Notation "\prod_ ( i 'in' A ) F" := (\big[*%R/1]_(i in A) F).
Local Notation "\prod_ ( m <= i < n ) F" := (\big[*%R/1%R]_(m <= i < n) F%R).
Definition pchar (R : nzSemiRingType) : nat_pred :=
[pred p | prime p & p%:R == 0 :> R].
Local Notation has_pchar0 L := (pchar L =i pred0).
Definition converse R : Type := R.
Local Notation "R ^c" := (converse R) : type_scope.
Section PzSemiRingTheory.
Variable R : pzSemiRingType.
Implicit Types x y : R.
#[export]
HB.instance Definition _ := Monoid.isLaw.Build R 1 *%R mulrA mul1r mulr1.
#[export]
HB.instance Definition _ := Monoid.isMulLaw.Build R 0 *%R mul0r mulr0.
#[export]
HB.instance Definition _ := Monoid.isAddLaw.Build R *%R +%R mulrDl mulrDr.
Lemma mulr_suml I r P (F : I -> R) x :
(\sum_(i <- r | P i) F i) * x = \sum_(i <- r | P i) F i * x.
Proof.
Lemma mulr_sumr I r P (F : I -> R) x :
x * (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x * F i.
Proof.
Lemma mulrnAl x y n : (x *+ n) * y = (x * y) *+ n.
Lemma mulrnAr x y n : x * (y *+ n) = (x * y) *+ n.
Lemma mulr_natl x n : n%:R * x = x *+ n.
Lemma mulr_natr x n : x * n%:R = x *+ n.
Lemma natrD m n : (m + n)%:R = m%:R + n%:R :> R
Proof.
Proof.
Proof.
Definition natr_sum := big_morph (natmul 1) natrD (mulr0n 1).
Lemma natrM m n : (m * n)%:R = m%:R * n%:R :> R.
Lemma expr0 x : x ^+ 0 = 1
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma exprS x n : x ^+ n.+1 = x * x ^+ n.
Proof.
Lemma expr0n n : 0 ^+ n = (n == 0%N)%:R :> R.
Lemma expr1n n : 1 ^+ n = 1 :> R.
Lemma exprD x m n : x ^+ (m + n) = x ^+ m * x ^+ n.
Lemma exprSr x n : x ^+ n.+1 = x ^+ n * x.
Lemma expr_sum x (I : Type) (s : seq I) (P : pred I) F :
x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ F i :> R.
Lemma commr_sym x y : comm x y -> comm y x
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma commr0 x : comm x 0.
Lemma commr1 x : comm x 1.
Lemma commrD x y z : comm x y -> comm x z -> comm x (y + z).
Lemma commr_sum (I : Type) (s : seq I) (P : pred I) (F : I -> R) x :
(forall i, P i -> comm x (F i)) -> comm x (\sum_(i <- s | P i) F i).
Lemma commrMn x y n : comm x y -> comm x (y *+ n).
Lemma commrM x y z : comm x y -> comm x z -> comm x (y * z).
Lemma commr_prod (I : Type) (s : seq I) (P : pred I) (F : I -> R) x :
(forall i, P i -> comm x (F i)) -> comm x (\prod_(i <- s | P i) F i).
Lemma commr_nat x n : comm x n%:R
Lemma commrX x y n : comm x y -> comm x (y ^+ n).
Lemma exprMn_comm x y n : comm x y -> (x * y) ^+ n = x ^+ n * y ^+ n.
Proof.
Lemma exprMn_n x m n : (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.
Proof.
Lemma exprM x m n : x ^+ (m * n) = x ^+ m ^+ n.
Proof.
Lemma exprAC x m n : (x ^+ m) ^+ n = (x ^+ n) ^+ m.
Lemma expr_mod n x i : x ^+ n = 1 -> x ^+ (i %% n) = x ^+ i.
Lemma expr_dvd n x i : x ^+ n = 1 -> n %| i -> x ^+ i = 1.
Lemma natrX n k : (n ^ k)%:R = n%:R ^+ k :> R.
Lemma mulrI_eq0 x y : lreg x -> (x * y == 0) = (y == 0).
Lemma lreg1 : lreg (1 : R).
Proof.
Lemma lregM x y : lreg x -> lreg y -> lreg (x * y).
Proof.
Lemma lregMl (a b: R) : lreg (a * b) -> lreg b.
Proof.
Lemma rregMr (a b: R) : rreg (a * b) -> rreg a.
Proof.
Lemma lregX x n : lreg x -> lreg (x ^+ n).
Lemma iter_mulr n x y : iter n ( *%R x) y = x ^+ n * y.
Lemma iter_mulr_1 n x : iter n ( *%R x) 1 = x ^+ n.
Lemma prodr_const (I : finType) (A : pred I) x : \prod_(i in A) x = x ^+ #|A|.
Lemma prodr_const_nat n m x : \prod_(n <= i < m) x = x ^+ (m - n).
Proof.
Lemma prodrXr x I r P (F : I -> nat) :
\prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).
Lemma prodrM_comm {I : eqType} r (P : pred I) (F G : I -> R) :
(forall i j, P i -> P j -> comm (F i) (G j)) ->
\prod_(i <- r | P i) (F i * G i) =
\prod_(i <- r | P i) F i * \prod_(i <- r | P i) G i.
Proof.
Lemma prodrMl_comm {I : finType} (A : pred I) (x : R) F :
(forall i, A i -> comm x (F i)) ->
\prod_(i in A) (x * F i) = x ^+ #|A| * \prod_(i in A) F i.
Proof.
Lemma prodrMr_comm {I : finType} (A : pred I) (x : R) F :
(forall i, A i -> comm x (F i)) ->
\prod_(i in A) (F i * x) = \prod_(i in A) F i * x ^+ #|A|.
Proof.
Lemma prodrMn (I : Type) (s : seq I) (P : pred I) (F : I -> R) (g : I -> nat) :
\prod_(i <- s | P i) (F i *+ g i) =
\prod_(i <- s | P i) (F i) *+ \prod_(i <- s | P i) g i.
Lemma prodrMn_const n (I : finType) (A : pred I) (F : I -> R) :
\prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.
Proof.
Lemma natr_prod I r P (F : I -> nat) :
(\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R.
Lemma exprDn_comm x y n (cxy : comm x y) :
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i).
Proof.
elim: n => [|n IHn]; rewrite big_ord_recl mulr1 ?big_ord0 ?addr0 //=.
rewrite exprS {}IHn /= mulrDl !big_distrr /= big_ord_recl mulr1 subn0.
rewrite !big_ord_recr /= !binn !subnn !mul1r !subn0 bin0 !exprS -addrA.
congr (_ + _); rewrite addrA -big_split /=; congr (_ + _).
apply: eq_bigr => i _; rewrite !mulrnAr !mulrA -exprS -subSn ?(valP i) //.
by rewrite subSS (commrX _ (commr_sym cxy)) -mulrA -exprS -mulrnDr.
Qed.
rewrite exprS {}IHn /= mulrDl !big_distrr /= big_ord_recl mulr1 subn0.
rewrite !big_ord_recr /= !binn !subnn !mul1r !subn0 bin0 !exprS -addrA.
congr (_ + _); rewrite addrA -big_split /=; congr (_ + _).
apply: eq_bigr => i _; rewrite !mulrnAr !mulrA -exprS -subSn ?(valP i) //.
by rewrite subSS (commrX _ (commr_sym cxy)) -mulrA -exprS -mulrnDr.
Qed.
Lemma exprD1n x n : (x + 1) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).
Proof.
Lemma sqrrD1 x : (x + 1) ^+ 2 = x ^+ 2 + x *+ 2 + 1.
Section ClosedPredicates.
Variable S : {pred R}.
Definition mulr_2closed := {in S &, forall u v, u * v \in S}.
Definition mulr_closed := 1 \in S /\ mulr_2closed.
Definition semiring_closed := nmod_closed S /\ mulr_closed.
Lemma semiring_closedD : semiring_closed -> nmod_closed S
Proof.
by case. Qed.
Lemma semiring_closedM : semiring_closed -> mulr_closed
Proof.
by case. Qed.
End ClosedPredicates.
End PzSemiRingTheory.
Section NzSemiRingTheory.
Variable R : nzSemiRingType.
Implicit Types x y : R.
Lemma oner_eq0 : (1 == 0 :> R) = false
Lemma lastr_eq0 (s : seq R) x : x != 0 -> (last x s == 0) = (last 1 s == 0).
Lemma lreg_neq0 x : lreg x -> x != 0.
Definition pFrobenius_aut p & p \in pchar R := fun x => x ^+ p.
Section FrobeniusAutomorphism.
Variable p : nat.
Hypothesis pcharFp : p \in pchar R.
Lemma pcharf0 : p%:R = 0 :> R
Lemma pcharf_prime : prime p
Hint Resolve pcharf_prime : core.
Lemma mulrn_pchar x : x *+ p = 0
Lemma natr_mod_pchar n : (n %% p)%:R = n%:R :> R.
Lemma dvdn_pcharf n : (p %| n)%N = (n%:R == 0 :> R).
Proof.
Lemma pcharf_eq : pchar R =i (p : nat_pred).
Proof.
move=> q; apply/andP/eqP=> [[q_pr q0] | ->]; last by rewrite pcharf0.
by apply/eqP; rewrite eq_sym -dvdn_prime2 // dvdn_pcharf.
Qed.
by apply/eqP; rewrite eq_sym -dvdn_prime2 // dvdn_pcharf.
Qed.
Lemma bin_lt_pcharf_0 k : 0 < k < p -> 'C(p, k)%:R = 0 :> R.
Proof.
Local Notation "x ^f" := (pFrobenius_aut pcharFp x).
Lemma pFrobenius_autE x : x^f = x ^+ p
Proof.
by []. Qed.
Lemma pFrobenius_aut0 : 0^f = 0.
Lemma pFrobenius_aut1 : 1^f = 1.
Lemma pFrobenius_autD_comm x y (cxy : comm x y) : (x + y)^f = x^f + y^f.
Proof.
have defp := prednK (prime_gt0 pcharf_prime).
rewrite !f'E exprDn_comm // big_ord_recr subnn -defp big_ord_recl /= defp.
rewrite subn0 mulr1 mul1r bin0 binn big1 ?addr0 // => i _.
by rewrite -mulr_natl bin_lt_pcharf_0 ?mul0r //= -{2}defp ltnS (valP i).
Qed.
rewrite !f'E exprDn_comm // big_ord_recr subnn -defp big_ord_recl /= defp.
rewrite subn0 mulr1 mul1r bin0 binn big1 ?addr0 // => i _.
by rewrite -mulr_natl bin_lt_pcharf_0 ?mul0r //= -{2}defp ltnS (valP i).
Qed.
Lemma pFrobenius_autMn x n : (x *+ n)^f = x^f *+ n.
Proof.
elim: n => [|n IHn]; first exact: pFrobenius_aut0.
by rewrite !mulrS pFrobenius_autD_comm ?IHn //; apply: commrMn.
Qed.
by rewrite !mulrS pFrobenius_autD_comm ?IHn //; apply: commrMn.
Qed.
Lemma pFrobenius_aut_nat n : (n%:R)^f = n%:R.
Proof.
Lemma pFrobenius_autM_comm x y : comm x y -> (x * y)^f = x^f * y^f.
Proof.
Lemma pFrobenius_autX x n : (x ^+ n)^f = x^f ^+ n.
End FrobeniusAutomorphism.
Section Char2.
Hypothesis pcharR2 : 2 \in pchar R.
Lemma addrr_pchar2 x : x + x = 0
Proof.
End Char2.
End NzSemiRingTheory.
#[short(type="pzRingType")]
HB.structure Definition PzRing := { R of PzSemiRing R & Zmodule R }.
HB.factory Record Zmodule_isPzRing R & Zmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul +%R;
mulrDr : right_distributive mul +%R;
}.
HB.builders Context R & Zmodule_isPzRing R.
Local Notation "1" := one.
Local Notation "x * y" := (mul x y).
Lemma mul0r : @left_zero R R 0 mul.
Lemma mulr0 : @right_zero R R 0 mul.
HB.instance Definition _ := Nmodule_isPzSemiRing.Build R
mulrA mul1r mulr1 mulrDl mulrDr mul0r mulr0.
HB.end.
HB.factory Record isPzRing R & Choice R := {
zero : R;
opp : R -> R;
add : R -> R -> R;
one : R;
mul : R -> R -> R;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add;
addNr : left_inverse zero opp add;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
}.
HB.builders Context R & isPzRing R.
HB.instance Definition _ := @isZmodule.Build R
zero opp add addrA addrC add0r addNr.
HB.instance Definition _ := @Zmodule_isPzRing.Build R
one mul mulrA mul1r mulr1 mulrDl mulrDr.
HB.end.
Module PzRingExports.
Bind Scope ring_scope with PzRing.sort.
End PzRingExports.
HB.export PzRingExports.
#[short(type="nzRingType")]
HB.structure Definition NzRing := { R of NzSemiRing R & Zmodule R }.
HB.factory Record Zmodule_isNzRing R & Zmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul +%R;
mulrDr : right_distributive mul +%R;
oner_neq0 : one != 0
}.
HB.builders Context R & Zmodule_isNzRing R.
HB.instance Definition _ := Zmodule_isPzRing.Build R
mulrA mul1r mulr1 mulrDl mulrDr.
HB.instance Definition _ := PzSemiRing_isNonZero.Build R oner_neq0.
HB.end.
HB.factory Record isNzRing R & Choice R := {
zero : R;
opp : R -> R;
add : R -> R -> R;
one : R;
mul : R -> R -> R;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add;
addNr : left_inverse zero opp add;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
oner_neq0 : one != zero
}.
HB.builders Context R & isNzRing R.
HB.instance Definition _ := @isZmodule.Build R
zero opp add addrA addrC add0r addNr.
HB.instance Definition _ := @Zmodule_isNzRing.Build R
one mul mulrA mul1r mulr1 mulrDl mulrDr oner_neq0.
HB.end.
Module NzRingExports.
Bind Scope ring_scope with NzRing.sort.
End NzRingExports.
HB.export NzRingExports.
Notation sign R b := (exp (- @one R) (nat_of_bool b)) (only parsing).
Local Notation "- 1" := (- (1)) : ring_scope.
Section PzRingTheory.
Variable R : pzRingType.
Implicit Types x y : R.
Lemma mulrN x y : x * (- y) = - (x * y).
Lemma mulNr x y : (- x) * y = - (x * y).
Lemma mulrNN x y : (- x) * (- y) = x * y.
Lemma mulN1r x : -1 * x = - x.
Lemma mulrN1 x : x * -1 = - x.
Lemma mulrBl x y z : (y - z) * x = y * x - z * x.
Lemma mulrBr x y z : x * (y - z) = x * y - x * z.
Lemma natrB m n : n <= m -> (m - n)%:R = m%:R - n%:R :> R.
Proof.
Lemma commrN x y : comm x y -> comm x (- y).
Lemma commrN1 x : comm x (-1)
Lemma commrB x y z : comm x y -> comm x z -> comm x (y - z).
Lemma commr_sign x n : comm x ((-1) ^+ n).
Lemma signr_odd n : (-1) ^+ (odd n) = (-1) ^+ n :> R.
Lemma mulr_sign (b : bool) x : (-1) ^+ b * x = (if b then - x else x).
Lemma signr_addb b1 b2 : (-1) ^+ (b1 (+) b2) = (-1) ^+ b1 * (-1) ^+ b2 :> R.
Lemma signrE (b : bool) : (-1) ^+ b = 1 - b.*2%:R :> R.
Lemma signrN b : (-1) ^+ (~~ b) = - (-1) ^+ b :> R.
Proof.
Lemma mulr_signM (b1 b2 : bool) x1 x2 :
((-1) ^+ b1 * x1) * ((-1) ^+ b2 * x2) = (-1) ^+ (b1 (+) b2) * (x1 * x2).
Proof.
Lemma exprNn x n : (- x) ^+ n = (-1) ^+ n * x ^+ n :> R.
Lemma sqrrN x : (- x) ^+ 2 = x ^+ 2
Proof.
Lemma sqrr_sign n : ((-1) ^+ n) ^+ 2 = 1 :> R.
Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)).
Lemma mulrI0_lreg x : (forall y, x * y = 0 -> y = 0) -> lreg x.
Proof.
Lemma lregN x : lreg x -> lreg (- x).
Lemma lreg_sign n : lreg ((-1) ^+ n : R)
Lemma prodrN (I : finType) (A : pred I) (F : I -> R) :
\prod_(i in A) - F i = (- 1) ^+ #|A| * \prod_(i in A) F i.
Proof.
Lemma exprBn_comm x y n (cxy : comm x y) :
(x - y) ^+ n =
\sum_(i < n.+1) ((-1) ^+ i * x ^+ (n - i) * y ^+ i) *+ 'C(n, i).
Proof.
rewrite exprDn_comm; first exact: commrN.
by apply: eq_bigr => i _; congr (_ *+ _); rewrite -commr_sign -mulrA -exprNn.
Qed.
by apply: eq_bigr => i _; congr (_ *+ _); rewrite -commr_sign -mulrA -exprNn.
Qed.
Lemma subrXX_comm x y n (cxy : comm x y) :
x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i).
Proof.
case: n => [|n]; first by rewrite big_ord0 mulr0 subrr.
rewrite mulrBl !big_distrr big_ord_recl big_ord_recr /= subnn mulr1 mul1r.
rewrite subn0 -!exprS opprD -!addrA; congr (_ + _); rewrite addrA -sumrB.
rewrite big1 ?add0r // => i _; rewrite !mulrA -exprS -subSn ?(valP i) //.
by rewrite subSS (commrX _ (commr_sym cxy)) -mulrA -exprS subrr.
Qed.
rewrite mulrBl !big_distrr big_ord_recl big_ord_recr /= subnn mulr1 mul1r.
rewrite subn0 -!exprS opprD -!addrA; congr (_ + _); rewrite addrA -sumrB.
rewrite big1 ?add0r // => i _; rewrite !mulrA -exprS -subSn ?(valP i) //.
by rewrite subSS (commrX _ (commr_sym cxy)) -mulrA -exprS subrr.
Qed.
Lemma subrX1 x n : x ^+ n - 1 = (x - 1) * (\sum_(i < n) x ^+ i).
Proof.
Lemma sqrrB1 x : (x - 1) ^+ 2 = x ^+ 2 - x *+ 2 + 1.
Lemma subr_sqr_1 x : x ^+ 2 - 1 = (x - 1) * (x + 1).
Proof.
Section ClosedPredicates.
Variable S : {pred R}.
Definition smulr_closed := -1 \in S /\ mulr_2closed S.
Definition subring_closed := [/\ 1 \in S, subr_closed S & mulr_2closed S].
Lemma smulr_closedM : smulr_closed -> mulr_closed S.
Lemma smulr_closedN : smulr_closed -> oppr_closed S.
Proof.
Lemma subring_closedB : subring_closed -> zmod_closed S.
Proof.
Lemma subring_closedM : subring_closed -> smulr_closed.
Proof.
Lemma subring_closed_semi : subring_closed -> semiring_closed S.
Proof.
End ClosedPredicates.
End PzRingTheory.
Section NzRingTheory.
Variable R : nzRingType.
Implicit Types x y : R.
Lemma signr_eq0 n : ((-1) ^+ n == 0 :> R) = false.
Section FrobeniusAutomorphism.
Variable p : nat.
Hypothesis pcharFp : p \in pchar R.
Hint Resolve pcharf_prime : core.
Local Notation "x ^f" := (pFrobenius_aut pcharFp x).
Lemma pFrobenius_autN x : (- x)^f = - x^f.
Proof.
apply/eqP; rewrite -subr_eq0 opprK addrC.
by rewrite -(pFrobenius_autD_comm _ (commrN _)) // subrr pFrobenius_aut0.
Qed.
by rewrite -(pFrobenius_autD_comm _ (commrN _)) // subrr pFrobenius_aut0.
Qed.
Lemma pFrobenius_autB_comm x y : comm x y -> (x - y)^f = x^f - y^f.
Proof.
End FrobeniusAutomorphism.
Lemma exprNn_pchar x n : (pchar R).-nat n -> (- x) ^+ n = - (x ^+ n).
Proof.
pose p := pdiv n; have [|n_gt1 pcharRn] := leqP n 1; first by case: (n) => [|[]].
have pcharRp: p \in pchar R by rewrite (pnatPpi pcharRn) // pi_pdiv.
have /p_natP[e ->]: p.-nat n by rewrite -(eq_pnat _ (pcharf_eq pcharRp)).
elim: e => // e IHe; rewrite expnSr !exprM {}IHe.
by rewrite -pFrobenius_autE pFrobenius_autN.
Qed.
have pcharRp: p \in pchar R by rewrite (pnatPpi pcharRn) // pi_pdiv.
have /p_natP[e ->]: p.-nat n by rewrite -(eq_pnat _ (pcharf_eq pcharRp)).
elim: e => // e IHe; rewrite expnSr !exprM {}IHe.
by rewrite -pFrobenius_autE pFrobenius_autN.
Qed.
Section Char2.
Hypothesis pcharR2 : 2 \in pchar R.
Lemma oppr_pchar2 x : - x = x.
Proof.
Lemma subr_pchar2 x y : x - y = x + y
Proof.
Lemma addrK_pchar2 x : involutive (+%R^~ x).
Proof.
Lemma addKr_pchar2 x : involutive (+%R x).
Proof.
End Char2.
End NzRingTheory.
Section ConverseRing.
#[export]
HB.instance Definition _ (T : eqType) := Equality.on T^c.
#[export]
HB.instance Definition _ (T : choiceType) := Choice.on T^c.
#[export]
HB.instance Definition _ (U : nmodType) := Nmodule.on U^c.
#[export]
HB.instance Definition _ (U : zmodType) := Zmodule.on U^c.
#[export]
HB.instance Definition _ (R : pzSemiRingType) :=
let mul' (x y : R) := y * x in
let mulrA' x y z := esym (mulrA z y x) in
let mulrDl' x y z := mulrDr z x y in
let mulrDr' x y z := mulrDl y z x in
Nmodule_isPzSemiRing.Build R^c
mulrA' mulr1 mul1r mulrDl' mulrDr' mulr0 mul0r.
#[export]
HB.instance Definition _ (R : pzRingType) := PzSemiRing.on R^c.
#[export]
HB.instance Definition _ (R : nzSemiRingType) :=
PzSemiRing_isNonZero.Build R^c oner_neq0.
#[export]
HB.instance Definition _ (R : nzRingType) := NzSemiRing.on R^c.
End ConverseRing.
Lemma rev_prodr (R : pzSemiRingType)
(I : Type) (r : seq I) (P : pred I) (E : I -> R) :
\prod_(i <- r | P i) (E i : R^c) = \prod_(i <- rev r | P i) E i.
Proof.
Section SemiRightRegular.
Variable R : pzSemiRingType.
Implicit Types x y : R.
Lemma mulIr_eq0 x y : rreg x -> (y * x == 0) = (y == 0).
Lemma rreg1 : rreg (1 : R).
Lemma rregM x y : rreg x -> rreg y -> rreg (x * y).
Lemma revrX x n : (x : R^c) ^+ n = (x : R) ^+ n.
Lemma rregX x n : rreg x -> rreg (x ^+ n).
End SemiRightRegular.
Lemma rreg_neq0 (R : nzSemiRingType) (x : R) : rreg x -> x != 0.
Section RightRegular.
Variable R : pzRingType.
Implicit Types x y : R.
Lemma mulIr0_rreg x : (forall y, y * x = 0 -> y = 0) -> rreg x.
Proof.
Lemma rregN x : rreg x -> rreg (- x)
End RightRegular.
HB.mixin Record Nmodule_isLSemiModule (R : pzSemiRingType) V & Nmodule V := {
scale : R -> V -> V;
scalerA : forall a b v, scale a (scale b v) = scale (a * b) v;
scale0r : forall v, scale 0 v = 0;
scale1r : left_id 1 scale;
scalerDr : right_distributive scale +%R;
scalerDl : forall v, {morph scale^~ v: a b / a + b}
}.
#[short(type="lSemiModType")]
HB.structure Definition LSemiModule (R : pzSemiRingType) :=
{M of Nmodule M & Nmodule_isLSemiModule R M}.
Module LSemiModExports.
Bind Scope ring_scope with LSemiModule.sort.
End LSemiModExports.
HB.export LSemiModExports.
Local Notation "*:%R" := (@scale _ _) : function_scope.
Local Notation "a *: v" := (scale a v) : ring_scope.
#[short(type="lmodType")]
HB.structure Definition Lmodule (R : pzRingType) :=
{M of Zmodule M & Nmodule_isLSemiModule R M}.
Arguments scalerA [R s] (a b)%_ring_scope v.
Module LmodExports.
Bind Scope ring_scope with Lmodule.sort.
End LmodExports.
HB.export LmodExports.
HB.factory Record Zmodule_isLmodule (R : pzRingType) V & Zmodule V := {
scale : R -> V -> V;
scalerA : forall a b v, scale a (scale b v) = scale (a * b) v;
scale1r : left_id 1 scale;
scalerDr : right_distributive scale +%R;
scalerDl : forall v, {morph scale^~ v: a b / a + b}
}.
HB.builders Context R V & Zmodule_isLmodule R V.
Lemma scale0r v : scale 0 v = 0.
HB.instance Definition _ :=
Nmodule_isLSemiModule.Build R V scalerA scale0r scale1r scalerDr scalerDl.
HB.end.
HB.factory Record LSemiModule_isLmodule (R : pzRingType) V
& LSemiModule R V := {}.
HB.builders Context R V & LSemiModule_isLmodule R V.
Definition opp : V -> V := scale (- 1).
Lemma addNr : left_inverse 0 opp +%R.
Proof.
HB.instance Definition _ := Nmodule_isZmodule.Build V addNr.
HB.end.
Section LSemiModuleTheory.
Variables (R : pzSemiRingType) (V : lSemiModType R).
Implicit Types (a b c : R) (u v : V).
Lemma scaler0 a : a *: 0 = 0 :> V.
Lemma scaler_nat n v : n%:R *: v = v *+ n.
Proof.
Lemma scalerMnl a v n : a *: v *+ n = (a *+ n) *: v.
Lemma scalerMnr a v n : a *: v *+ n = a *: (v *+ n).
Lemma scaler_suml v I r (P : pred I) F :
(\sum_(i <- r | P i) F i) *: v = \sum_(i <- r | P i) F i *: v.
Lemma scaler_sumr a I r (P : pred I) (F : I -> V) :
a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.
Section ClosedPredicates.
Variable S : {pred V}.
Definition scaler_closed := forall a, {in S, forall v, a *: v \in S}.
Definition subsemimod_closed := nmod_closed S /\ scaler_closed.
Lemma subsemimod_closedD : subsemimod_closed -> nmod_closed S.
Proof.
by case. Qed.
Lemma subsemimod_closedZ : subsemimod_closed -> scaler_closed.
Proof.
by case. Qed.
End ClosedPredicates.
End LSemiModuleTheory.
Section LmoduleTheory.
Variables (R : pzRingType) (V : lmodType R).
Implicit Types (a b c : R) (u v : V).
Lemma scaleNr a v : - a *: v = - (a *: v).
Lemma scaleN1r v : - 1 *: v = - v.
Lemma scalerN a v : a *: - v = - (a *: v).
Lemma scalerBl a b v : (a - b) *: v = a *: v - b *: v.
Lemma scalerBr a u v : a *: (u - v) = a *: u - a *: v.
Lemma scaler_sign (b : bool) v : (-1) ^+ b *: v = (if b then - v else v).
Lemma signrZK n : @involutive V ( *:%R ((-1) ^+ n)).
Section ClosedPredicates.
Variable S : {pred V}.
Definition linear_closed := forall a, {in S &, forall u v, a *: u + v \in S}.
Definition submod_closed := 0 \in S /\ linear_closed.
Lemma linear_closedB : linear_closed -> subr_closed S.
Lemma submod_closedB : submod_closed -> zmod_closed S.
Proof.
Lemma submod_closed_semi : submod_closed -> subsemimod_closed S.
Proof.
move=> /[dup] /submod_closedB /zmod_closed0D SD [S0 Slin]; split => // a v Sv.
by rewrite -[a *: v]addr0 Slin.
Qed.
by rewrite -[a *: v]addr0 Slin.
Qed.
Lemma subsemimod_closed_submod : subsemimod_closed S -> submod_closed.
Proof.
by case=> [[S0 SD] SZ]; split => // a u v Su Sv; apply/SD/Sv/SZ. Qed.
Lemma subsemimod_closedB : subsemimod_closed S -> zmod_closed S.
Proof.
End ClosedPredicates.
End LmoduleTheory.
HB.mixin Record LSemiModule_isLSemiAlgebra R V
& PzSemiRing V & LSemiModule R V := {
scalerAl : forall (a : R) (u v : V), a *: (u * v) = (a *: u) * v
}.
#[short(type="pzLSemiAlgType")]
HB.structure Definition PzLSemiAlgebra R :=
{A of LSemiModule R A & PzSemiRing A & LSemiModule_isLSemiAlgebra R A}.
Module PzLSemiAlgExports.
Bind Scope ring_scope with PzLSemiAlgebra.sort.
End PzLSemiAlgExports.
HB.export PzLSemiAlgExports.
#[short(type="nzLSemiAlgType")]
HB.structure Definition NzLSemiAlgebra (R : nzSemiRingType) :=
{A of LSemiModule R A & NzSemiRing A & LSemiModule_isLSemiAlgebra R A}.
Module NzLSemiAlgExports.
Bind Scope ring_scope with NzLSemiAlgebra.sort.
End NzLSemiAlgExports.
HB.export NzLSemiAlgExports.
Local Notation "k %:A" := (k *: 1) : ring_scope.
#[short(type="pzLalgType")]
HB.structure Definition PzLalgebra R :=
{A of Lmodule R A & PzRing A & LSemiModule_isLSemiAlgebra R A}.
Module PzLalgExports.
Bind Scope ring_scope with PzLalgebra.sort.
End PzLalgExports.
HB.export PzLalgExports.
#[short(type="nzLalgType")]
HB.structure Definition NzLalgebra (R : nzRingType) :=
{A of Lmodule R A & NzRing A & LSemiModule_isLSemiAlgebra R A}.
Module NzLalgExports.
Bind Scope ring_scope with NzLalgebra.sort.
End NzLalgExports.
HB.export NzLalgExports.
Definition regular R : Type := R.
Local Notation "R ^o" := (regular R) : type_scope.
Section RegularAlgebra.
#[export]
HB.instance Definition _ (V : nmodType) := Nmodule.on V^o.
#[export]
HB.instance Definition _ (V : zmodType) := Zmodule.on V^o.
#[export]
HB.instance Definition _ (R : pzSemiRingType) := PzSemiRing.on R^o.
#[export]
HB.instance Definition _ (R : nzSemiRingType) := NzSemiRing.on R^o.
#[export]
HB.instance Definition _ (R : pzSemiRingType) :=
@Nmodule_isLSemiModule.Build R R^o
mul mulrA mul0r mul1r mulrDr (fun v a b => mulrDl a b v).
#[export]
HB.instance Definition _ (R : pzSemiRingType) :=
LSemiModule_isLSemiAlgebra.Build R R^o mulrA.
#[export]
HB.instance Definition _ (R : nzSemiRingType) := NzSemiRing.on R^o.
#[export]
HB.instance Definition _ (R : pzRingType) := PzRing.on R^o.
#[export]
HB.instance Definition _ (R : nzRingType) := NzRing.on R^o.
End RegularAlgebra.
Section LSemiAlgebraTheory.
Variables (R : pzSemiRingType) (A : pzLSemiAlgType R).
Lemma mulr_algl (a : R) (x : A) : (a *: 1) * x = a *: x.
Section ClosedPredicates.
Variable S : {pred A}.
Definition subsemialg_closed :=
[/\ 1 \in S, nmod_closed S, scaler_closed S & mulr_2closed S].
Lemma subsemialg_closedZ : subsemialg_closed -> subsemimod_closed S.
Proof.
by case. Qed.
Lemma subsemialg_closedM : subsemialg_closed -> semiring_closed S.
Proof.
by case. Qed.
End ClosedPredicates.
End LSemiAlgebraTheory.
Section LalgebraTheory.
Variables (R : pzRingType) (A : pzLalgType R).
Section ClosedPredicates.
Variable S : {pred A}.
Definition subalg_closed := [/\ 1 \in S, linear_closed S & mulr_2closed S].
Lemma subalg_closedZ : subalg_closed -> submod_closed S.
Proof.
Lemma subalg_closedBM : subalg_closed -> subring_closed S.
Proof.
Lemma subalg_closed_semi : subalg_closed -> subsemialg_closed S.
Proof.
move=> /[dup] /subalg_closedZ /submod_closedB /zmod_closed0D.
by move=> [S0 SD] [S1 Slin SM]; split => // a u Su; rewrite -[a *: u]addr0 Slin.
Qed.
by move=> [S0 SD] [S1 Slin SM]; split => // a u Su; rewrite -[a *: u]addr0 Slin.
Qed.
Lemma subsemialg_closed_subalg : subsemialg_closed S -> subalg_closed.
Proof.
by case=> S1 [S0 SD] SZ SM; split => // a u v Su Sv; apply/SD/Sv/SZ. Qed.
Lemma subsemialg_closedBM : subsemialg_closed S -> subring_closed S.
Proof.
End ClosedPredicates.
End LalgebraTheory.
Section LiftedSemiRing.
Variables (R : pzSemiRingType) (T : Type).
Implicit Type f : T -> R.
Definition mull_fun a f x := a * f x.
Definition mulr_fun a f x := f x * a.
Definition mul_fun f g x := f x * g x.
End LiftedSemiRing.
Section LiftedScale.
Variables (R : pzSemiRingType) (U : Type).
Variables (V : lSemiModType R) (A : pzLSemiAlgType R).
Definition scale_fun a (f : U -> V) x := a *: f x.
Definition in_alg k : A := k%:A.
End LiftedScale.
Local Notation "\0" := (null_fun _) : function_scope.
Local Notation "f \+ g" := (add_fun f g) : function_scope.
Local Notation "f \- g" := (sub_fun f g) : function_scope.
Local Notation "\- f" := (opp_fun f) : function_scope.
Local Notation "a \*: f" := (scale_fun a f) : function_scope.
Local Notation "x \*o f" := (mull_fun x f) : function_scope.
Local Notation "x \o* f" := (mulr_fun x f) : function_scope.
Local Notation "f \* g" := (mul_fun f g) : function_scope.
Arguments in_alg {_} A _ /.
Arguments mull_fun {_ _} a f _ /.
Arguments mulr_fun {_ _} a f _ /.
Arguments scale_fun {_ _ _} a f _ /.
Arguments mul_fun {_ _} f g _ /.
Section AdditiveTheory.
Section SemiRingProperties.
Variables (R S : pzSemiRingType) (f : {additive R -> S}).
Lemma raddfMnat n x : f (n%:R * x) = n%:R * f x.
Variables (U : lSemiModType R) (V : lSemiModType S) (h : {additive U -> V}).
Lemma raddfZnat n u : h (n%:R *: u) = n%:R *: h u.
Proof.
End SemiRingProperties.
Section MulFun.
Variables (R : pzSemiRingType) (U : nmodType) (a : R) (f : {additive U -> R}).
Fact mull_fun_is_nmod_morphism : nmod_morphism (a \*o f).
#[export]
HB.instance Definition _ := isNmodMorphism.Build U R (a \*o f)
mull_fun_is_nmod_morphism.
Fact mulr_fun_is_nmod_morphism : nmod_morphism (a \o* f).
#[export]
HB.instance Definition _ := isNmodMorphism.Build U R (a \o* f)
mulr_fun_is_nmod_morphism.
End MulFun.
Section Properties.
Variables (U V : zmodType) (f : {additive U -> V}).
Lemma raddfN : {morph f : x / - x}
Proof.
Proof.
Lemma raddf_inj : (forall x, f x = 0 -> x = 0) -> injective f.
Proof.
Lemma raddfMNn n : {morph f : x / x *- n}
Proof.
End Properties.
Section RingProperties.
Variables (R S : pzRingType) (f : {additive R -> S}).
Lemma raddfMsign n x : f ((-1) ^+ n * x) = (-1) ^+ n * f x.
Variables (U : lmodType R) (V : lmodType S) (h : {additive U -> V}).
Lemma raddfZsign n u : h ((-1) ^+ n *: u) = (-1) ^+ n *: h u.
End RingProperties.
Section ScaleFun.
Variables (R : pzSemiRingType) (U : nmodType) (V : lSemiModType R).
Variables (a : R) (f : {additive U -> V}).
#[export]
HB.instance Definition _ :=
isNmodMorphism.Build V V ( *:%R a) (conj (scaler0 _ a) (scalerDr a)).
#[export]
HB.instance Definition _ := Additive.copy (a \*: f) (f \; *:%R a).
End ScaleFun.
End AdditiveTheory.
Definition monoid_morphism (R S : pzSemiRingType) (f : R -> S) : Prop :=
(f 1 = 1) * {morph f : x y / x * y}%R.
HB.mixin Record isMonoidMorphism (R S : pzSemiRingType) (f : R -> S) := {
monoid_morphism_subproof : monoid_morphism f
}.
HB.structure Definition RMorphism (R S : pzSemiRingType) :=
{f of @isNmodMorphism R S f & isMonoidMorphism R S f}.
Module RMorphismExports.
Notation "{ 'rmorphism' U -> V }" := (RMorphism.type U%type V%type)
: type_scope.
End RMorphismExports.
HB.export RMorphismExports.
Section RmorphismTheory.
Section Properties.
Variables (R S : pzSemiRingType) (f : {rmorphism R -> S}).
Lemma rmorph0 : f 0 = 0
Proof.
Proof.
Proof.
f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).
Proof.
Lemma rmorphism_monoidP : monoid_morphism f.
Proof.
Lemma rmorph1 : f 1 = 1
Proof.
Proof.
Lemma rmorph_prod I r (P : pred I) E :
f (\prod_(i <- r | P i) E i) = \prod_(i <- r | P i) f (E i).
Lemma rmorphXn n : {morph f : x / x ^+ n}.
Lemma rmorph_nat n : f n%:R = n%:R
Lemma rmorph_eq_nat x n : injective f -> (f x == n%:R) = (x == n%:R).
Proof.
Lemma rmorph_eq1 x : injective f -> (f x == 1) = (x == 1).
Proof.
Lemma can2_monoid_morphism f' : cancel f f' -> cancel f' f -> monoid_morphism f'.
Proof.
Definition can2_rmorphism f' (cff' : cancel f f') :=
(fun p => (p.2, p.1)) \o (can2_monoid_morphism cff').
End Properties.
Lemma rmorph_pchar (R S : nzSemiRingType) (f : {rmorphism R -> S}) p :
p \in pchar R -> p \in pchar S.
Proof.
Section Projections.
Variables (R S T : pzSemiRingType).
Variables (f : {rmorphism S -> T}) (g : {rmorphism R -> S}).
Fact idfun_is_monoid_morphism : monoid_morphism (@idfun R).
Proof.
by []. Qed.
HB.instance Definition _ := isMonoidMorphism.Build R R idfun
idfun_is_monoid_morphism.
Fact comp_is_monoid_morphism : monoid_morphism (f \o g).
#[export]
HB.instance Definition _ := isMonoidMorphism.Build R T (f \o g)
comp_is_monoid_morphism.
End Projections.
Section Properties.
Variables (R S : pzRingType) (f : {rmorphism R -> S}).
Lemma rmorphN : {morph f : x / - x}
Proof.
Proof.
Proof.
Proof.
Lemma rmorphN1 : f (- 1) = (- 1)
Lemma rmorph_sign n : f ((- 1) ^+ n) = (- 1) ^+ n.
End Properties.
Section InSemiAlgebra.
Variables (R : pzSemiRingType) (A : pzLSemiAlgType R).
Fact in_alg_is_nmod_morphism : nmod_morphism (in_alg A).
#[export]
HB.instance Definition _ :=
isNmodMorphism.Build R A (in_alg A) in_alg_is_nmod_morphism.
Fact in_alg_is_monoid_morphism : monoid_morphism (in_alg A).
#[export]
HB.instance Definition _ := isMonoidMorphism.Build R A (in_alg A)
in_alg_is_monoid_morphism.
Lemma in_algE a : in_alg A a = a%:A
Proof.
by []. Qed.
End InSemiAlgebra.
End RmorphismTheory.
Module Scale.
HB.mixin Record isPreLaw
(R : pzSemiRingType) (V : nmodType) (op : R -> V -> V) := {
op_nmod_morphism : forall a, nmod_morphism (op a);
}.
#[export]
HB.structure Definition PreLaw R V := {op of isPreLaw R V op}.
Definition preLaw := PreLaw.type.
HB.mixin Record isSemiLaw
(R : pzSemiRingType) (V : nmodType) (op : R -> V -> V) := {
op0v : forall v, op 0 v = 0;
op1v : op 1 =1 id;
opA : forall a b v, op a (op b v) = op (a * b) v;
}.
#[export]
HB.structure Definition SemiLaw R V :=
{op of isPreLaw R V op & isSemiLaw R V op}.
Definition semiLaw := SemiLaw.type.
HB.mixin Record isLaw (R : pzRingType) (V : zmodType) (op : R -> V -> V) :=
{ N1op : op (-1) =1 -%R }.
#[export]
HB.structure Definition Law (R : pzRingType) (V : zmodType) :=
{op of isPreLaw R V op & isLaw R V op}.
Definition law := Law.type.
Section CompSemiLaw.
Context (R : pzSemiRingType) (V : nmodType) (s : semiLaw R V).
Context (aR : pzSemiRingType) (nu : {rmorphism aR -> R}).
Fact comp_op0v v : (nu \; s) 0 v = 0.
Fact comp_op1v : (nu \; s) 1 =1 id.
Fact comp_opA a b v : (nu \; s) a ((nu \; s) b v) = (nu \; s) (a * b) v.
End CompSemiLaw.
Fact compN1op
(R : pzRingType) (V : zmodType) (s : law R V)
(aR : pzRingType) (nu : {rmorphism aR -> R}) : (nu \; s) (-1) =1 -%R.
Module Exports. HB.reexport. End Exports.
End Scale.
Export Scale.Exports.
#[export]
HB.instance Definition _ (R : pzSemiRingType) :=
Scale.isPreLaw.Build R R *%R (fun => mull_fun_is_nmod_morphism _ idfun).
#[export]
HB.instance Definition _ (R : pzSemiRingType) :=
Scale.isSemiLaw.Build R R *%R mul0r mul1r mulrA.
#[export]
HB.instance Definition _ (R : pzRingType) :=
Scale.isLaw.Build R R *%R (@mulN1r R).
#[export]
HB.instance Definition _ (R : pzSemiRingType) (V : lSemiModType R) :=
Scale.isPreLaw.Build R V *:%R (fun => (scaler0 _ _, scalerDr _)).
#[export]
HB.instance Definition _ (R : pzSemiRingType) (V : lSemiModType R) :=
Scale.isSemiLaw.Build R V *:%R scale0r scale1r (@scalerA _ _).
#[export]
HB.instance Definition _ (R : pzRingType) (U : lmodType R) :=
Scale.isLaw.Build R U *:%R (@scaleN1r R U).
#[export]
HB.instance Definition _
(R : pzSemiRingType) (V : nmodType) (s : Scale.preLaw R V)
(aR : pzSemiRingType) (nu : {rmorphism aR -> R}) :=
Scale.isPreLaw.Build aR V (nu \; s) (fun => Scale.op_nmod_morphism _).
#[export]
HB.instance Definition _
(R : pzSemiRingType) (V : nmodType) (s : Scale.semiLaw R V)
(aR : pzSemiRingType) (nu : {rmorphism aR -> R}) :=
Scale.isSemiLaw.Build aR V (nu \; s)
(Scale.comp_op0v s nu) (Scale.comp_op1v s nu) (Scale.comp_opA s nu).
#[export]
HB.instance Definition _
(R : pzRingType) (V : zmodType) (s : Scale.law R V)
(aR : pzRingType) (nu : {rmorphism aR -> R}) :=
Scale.isLaw.Build aR V (nu \; s) (Scale.compN1op s nu).
#[export, non_forgetful_inheritance]
HB.instance Definition _
(R : pzSemiRingType) (V : nmodType) (s : Scale.preLaw R V) a :=
isNmodMorphism.Build V V (s a) (Scale.op_nmod_morphism a).
Definition scalable_for (R : pzSemiRingType) (U : lSemiModType R) (V : nmodType)
(s : R -> V -> V) (f : U -> V) :=
forall a, {morph f : u / a *: u >-> s a u}.
HB.mixin Record isScalable (R : pzSemiRingType) (U : lSemiModType R)
(V : nmodType) (s : R -> V -> V) (f : U -> V) := {
semi_linear_subproof : scalable_for s f;
}.
HB.structure Definition Linear (R : pzSemiRingType)
(U : lSemiModType R) (V : nmodType) (s : R -> V -> V) :=
{f of @isNmodMorphism U V f & isScalable R U V s f}.
Definition semilinear_for (R : pzSemiRingType)
(U : lSemiModType R) (V : nmodType) (s : R -> V -> V) (f : U -> V) : Type :=
scalable_for s f * {morph f : x y / x + y}.
Lemma nmod_morphism_semilinear (R : pzSemiRingType)
(U : lSemiModType R) (V : nmodType) (s : Scale.semiLaw R V) (f : U -> V) :
semilinear_for s f -> nmod_morphism f.
Definition additive_semilinear := nmod_morphism_semilinear.
Lemma scalable_semilinear (R : pzSemiRingType)
(U : lSemiModType R) (V : nmodType) (s : Scale.preLaw R V) (f : U -> V) :
semilinear_for s f -> scalable_for s f.
Proof.
by case. Qed.
HB.factory Record isSemilinear (R : pzSemiRingType) (U : lSemiModType R)
(V : nmodType) (s : Scale.semiLaw R V) (f : U -> V) := {
linear_subproof : semilinear_for s f;
}.
HB.builders Context R U V s f & isSemilinear R U V s f.
HB.instance Definition _ := isNmodMorphism.Build U V f
(additive_semilinear linear_subproof).
HB.instance Definition _ :=
isScalable.Build R U V s f (scalable_semilinear linear_subproof).
HB.end.
Definition linear_for (R : pzSemiRingType) (U : lSemiModType R) (V : nmodType)
(s : R -> V -> V) (f : U -> V) :=
forall a, {morph f : u v / a *: u + v >-> s a u + v}.
Lemma zmod_morphism_linear (R : pzRingType) (U : lmodType R) V
(s : Scale.law R V) (f : U -> V) : linear_for s f -> zmod_morphism f.
Lemma scalable_linear (R : pzRingType) (U : lmodType R) V
(s : Scale.law R V) (f : U -> V) : linear_for s f -> scalable_for s f.
Proof.
Lemma semilinear_linear (R : pzRingType) (U : lmodType R) V
(s : Scale.law R V) (f : U -> V) : linear_for s f -> semilinear_for s f.
Proof.
move=> Lsf; split=> [a x|x y]; first exact: (scalable_linear Lsf).
have f0: f 0 = 0 by rewrite -[0 in LHS]subr0 (zmod_morphism_linear Lsf) subrr.
by rewrite -[y in LHS]opprK -[- y]add0r !(zmod_morphism_linear Lsf) f0 sub0r opprK.
Qed.
have f0: f 0 = 0 by rewrite -[0 in LHS]subr0 (zmod_morphism_linear Lsf) subrr.
by rewrite -[y in LHS]opprK -[- y]add0r !(zmod_morphism_linear Lsf) f0 sub0r opprK.
Qed.
HB.factory Record isLinear (R : pzRingType) (U : lmodType R) (V : zmodType)
(s : Scale.law R V) (f : U -> V) := {
linear_subproof : linear_for s f;
}.
HB.builders Context R U V s f & isLinear R U V s f.
HB.instance Definition _ := isZmodMorphism.Build U V f
(zmod_morphism_linear linear_subproof).
HB.instance Definition _ := isScalable.Build R U V s f
(scalable_linear linear_subproof).
HB.end.
Module LinearExports.
Notation scalable f := (scalable_for *:%R f).
Notation semilinear f := (semilinear_for *:%R f).
Notation semiscalar f := (semilinear_for *%R f).
Notation linear f := (linear_for *:%R f).
Notation scalar f := (linear_for *%R f).
Module Linear.
Section Linear.
Variables (R : pzSemiRingType) (U : lSemiModType R) (V : nmodType).
Variables (s : R -> V -> V).
Local Notation mapUV := (@Linear.type R U V s).
Definition map_class := mapUV.
Definition map_at (a : R) := mapUV.
Structure map_for a s_a := MapFor {map_for_map : mapUV; _ : s a = s_a}.
Definition unify_map_at a (g : map_at a) := MapFor g (erefl (s a)).
Structure wrapped := Wrap {unwrap : mapUV}.
Definition wrap (f : map_class) := Wrap f.
End Linear.
End Linear.
Notation "{ 'linear' U -> V | s }" := (@Linear.type _ U V s) : type_scope.
Notation "{ 'linear' U -> V }" := {linear U -> V | *:%R} : type_scope.
Notation "{ 'scalar' U }" := {linear U -> _ | *%R}
(format "{ 'scalar' U }") : type_scope.
Coercion Linear.map_for_map : Linear.map_for >-> Linear.type.
Coercion Linear.unify_map_at : Linear.map_at >-> Linear.map_for.
Canonical Linear.unify_map_at.
Coercion Linear.unwrap : Linear.wrapped >-> Linear.type.
Coercion Linear.wrap : Linear.map_class >-> Linear.wrapped.
Canonical Linear.wrap.
End LinearExports.
HB.export LinearExports.
Section LinearTheory.
Section GenericProperties.
Variables (R : pzSemiRingType) (U : lSemiModType R) (V : nmodType).
Variables (s : R -> V -> V) (f : {linear U -> V | s}).
Lemma linear0 : f 0 = 0
Proof.
Proof.
Proof.
f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).
Proof.
Lemma linearZ_LR : scalable_for s f
Proof.
Proof.
Proof.
End GenericProperties.
Section GenericProperties.
Variables (R : pzRingType) (U : lmodType R) (V : zmodType) (s : R -> V -> V).
Variables (f : {linear U -> V | s}).
Lemma linearN : {morph f : x / - x}
Proof.
Proof.
Proof.
End GenericProperties.
Section BidirectionalLinearZ.
Lemma linearZ (R : pzSemiRingType) (U : lSemiModType R) (V : nmodType)
(s : R -> V -> V) (S : pzSemiRingType) (h : Scale.preLaw S V)
(c : S) (a : R) (h_c := h c) (f : Linear.map_for U s a h_c) (u : U) :
f (a *: u) = h_c (Linear.wrap f u).
Proof.
End BidirectionalLinearZ.
Section LmodProperties.
Variables (R : pzSemiRingType) (U V : lSemiModType R) (f : {linear U -> V}).
Lemma linearZZ : scalable f
Proof.
Proof.
Proof.
Lemma can2_scalable f' : cancel f f' -> cancel f' f -> scalable f'.
Lemma can2_semilinear f' : cancel f f' -> cancel f' f -> semilinear f'.
Proof.
Lemma can2_linear f' : cancel f f' -> cancel f' f -> linear f'.
End LmodProperties.
Section ScalarProperties.
Variable (R : pzSemiRingType) (U : lSemiModType R) (f : {scalar U}).
Lemma scalarZ : scalable_for *%R f
Proof.
Proof.
Proof.
End ScalarProperties.
Section LinearLSemiMod.
Section Idfun.
Variables (R : pzSemiRingType) (U : lSemiModType R).
Lemma idfun_is_scalable : scalable (@idfun U)
Proof.
by []. Qed.
HB.instance Definition _ := isScalable.Build R U U *:%R idfun idfun_is_scalable.
End Idfun.
Section Plain.
Variables (R : pzSemiRingType) (W U : lSemiModType R) (V : nmodType).
Variables (s : R -> V -> V) (f : {linear U -> V | s}) (g : {linear W -> U}).
Lemma comp_is_scalable : scalable_for s (f \o g).
Proof.
#[export]
HB.instance Definition _ := isScalable.Build R W V s (f \o g) comp_is_scalable.
End Plain.
Section SemiScale.
Variables (R : pzSemiRingType) (U : lSemiModType R) (V : nmodType).
Variables (s : Scale.preLaw R V) (f g : {linear U -> V | s}).
Lemma null_fun_is_scalable : scalable_for s (\0 : U -> V).
Proof.
HB.instance Definition _ :=
isScalable.Build R U V s \0 null_fun_is_scalable.
Lemma add_fun_is_scalable : scalable_for s (add_fun f g).
Proof.
HB.instance Definition _ :=
isScalable.Build R U V s (f \+ g) add_fun_is_scalable.
End SemiScale.
End LinearLSemiMod.
Section LinearLmod.
Variables (R : pzRingType) (U : lmodType R).
Lemma opp_is_scalable : scalable (-%R : U -> U).
Proof.
HB.instance Definition _ := isScalable.Build R U U *:%R -%R opp_is_scalable.
End LinearLmod.
Section Scale.
Variables (R : pzRingType) (U : lmodType R) (V : zmodType).
Variables (s : Scale.preLaw R V) (f g : {linear U -> V | s}).
Lemma sub_fun_is_scalable : scalable_for s (f \- g).
Proof.
HB.instance Definition _ :=
isScalable.Build R U V s (f \- g) sub_fun_is_scalable.
Lemma opp_fun_is_scalable : scalable_for s (\- f).
Proof.
HB.instance Definition _ := isScalable.Build R U V s (\- f) opp_fun_is_scalable.
End Scale.
Section LinearLSemiAlg.
Variables (R : pzSemiRingType) (A : pzLSemiAlgType R) (U : lSemiModType R).
Variables (a : A) (f : {linear U -> A}).
Fact mulr_fun_is_scalable : scalable (a \o* f).
#[export]
HB.instance Definition _ :=
isScalable.Build R U A *:%R (a \o* f) mulr_fun_is_scalable.
End LinearLSemiAlg.
End LinearTheory.
HB.structure Definition LRMorphism (R : pzSemiRingType) (A : pzLSemiAlgType R)
(B : pzSemiRingType) (s : R -> B -> B) :=
{f of @RMorphism A B f & isScalable R A B s f}.
Module LRMorphismExports.
Notation "{ 'lrmorphism' A -> B | s }" := (@LRMorphism.type _ A%type B%type s)
: type_scope.
Notation "{ 'lrmorphism' A -> B }" := {lrmorphism A%type -> B%type | *:%R}
: type_scope.
End LRMorphismExports.
HB.export LRMorphismExports.
Section LRMorphismTheory.
Variables (R : pzSemiRingType) (A B : pzLSemiAlgType R) (C : pzSemiRingType).
Variables (s : R -> C -> C).
Variables (f : {lrmorphism A -> B}) (g : {lrmorphism B -> C | s}).
#[export] HB.instance Definition _ := RMorphism.on (@idfun A).
#[export] HB.instance Definition _ := RMorphism.on (g \o f).
Lemma rmorph_alg a : f a%:A = a%:A.
End LRMorphismTheory.
HB.mixin Record SemiRing_hasCommutativeMul R & PzSemiRing R := {
mulrC : commutative (@mul R)
}.
#[short(type="comPzSemiRingType")]
HB.structure Definition ComPzSemiRing :=
{R of PzSemiRing R & SemiRing_hasCommutativeMul R}.
Module ComPzSemiRingExports.
Bind Scope ring_scope with ComPzSemiRing.sort.
End ComPzSemiRingExports.
HB.export ComPzSemiRingExports.
HB.factory Record Nmodule_isComPzSemiRing R & Nmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mulrC : commutative mul;
mul1r : left_id one mul;
mulrDl : left_distributive mul add;
mul0r : left_zero zero mul;
}.
HB.builders Context R & Nmodule_isComPzSemiRing R.
Definition mulr1 := Monoid.mulC_id mulrC mul1r.
Definition mulrDr := Monoid.mulC_dist mulrC mulrDl.
Lemma mulr0 : right_zero zero mul.
HB.instance Definition _ := Nmodule_isPzSemiRing.Build R
mulrA mul1r mulr1 mulrDl mulrDr mul0r mulr0.
HB.instance Definition _ := SemiRing_hasCommutativeMul.Build R mulrC.
HB.end.
#[short(type="comNzSemiRingType")]
HB.structure Definition ComNzSemiRing :=
{R of NzSemiRing R & SemiRing_hasCommutativeMul R}.
Module ComNzSemiRingExports.
Bind Scope ring_scope with ComNzSemiRing.sort.
End ComNzSemiRingExports.
HB.export ComNzSemiRingExports.
HB.factory Record Nmodule_isComNzSemiRing R & Nmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mulrC : commutative mul;
mul1r : left_id one mul;
mulrDl : left_distributive mul add;
mul0r : left_zero zero mul;
oner_neq0 : one != zero
}.
HB.builders Context R & Nmodule_isComNzSemiRing R.
HB.instance Definition _ := Nmodule_isComPzSemiRing.Build R
mulrA mulrC mul1r mulrDl mul0r.
HB.instance Definition _ := PzSemiRing_isNonZero.Build R oner_neq0.
HB.end.
Section ComSemiRingTheory.
Variable R : comPzSemiRingType.
Implicit Types x y : R.
#[export]
HB.instance Definition _ := SemiGroup.isCommutativeLaw.Build R *%R mulrC.
Lemma mulrCA : @left_commutative R R *%R
Proof.
Proof.
Proof.
Lemma exprMn n : {morph (fun x => x ^+ n) : x y / x * y}.
Proof.
Lemma prodrXl n I r (P : pred I) (F : I -> R) :
\prod_(i <- r | P i) F i ^+ n = (\prod_(i <- r | P i) F i) ^+ n.
Lemma prodr_undup_exp_count (I : eqType) r (P : pred I) (F : I -> R) :
\prod_(i <- undup r | P i) F i ^+ count_mem i r = \prod_(i <- r | P i) F i.
Proof.
Lemma prodrMl {I : finType} (A : pred I) (x : R) F :
\prod_(i in A) (x * F i) = x ^+ #|A| * \prod_(i in A) F i.
Proof.
Lemma prodrMr {I : finType} (A : pred I) (x : R) F :
\prod_(i in A) (F i * x) = \prod_(i in A) F i * x ^+ #|A|.
Proof.
Lemma exprDn x y n :
(x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i).
Proof.
Lemma sqrrD x y : (x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2.
Lemma rmorph_comm (S : pzSemiRingType) (f : {rmorphism R -> S}) x y :
comm (f x) (f y).
Section ScaleLinear.
Variables (U V : lSemiModType R) (b : R) (f : {linear U -> V}).
Lemma scale_is_scalable : scalable ( *:%R b : V -> V).
#[export]
HB.instance Definition _ :=
isScalable.Build R V V *:%R ( *:%R b) scale_is_scalable.
Lemma scale_fun_is_scalable : scalable (b \*: f).
Proof.
HB.instance Definition _ :=
isScalable.Build R U V *:%R (b \*: f) scale_fun_is_scalable.
End ScaleLinear.
End ComSemiRingTheory.
Section ComNzSemiRingTheory.
Variable R : comNzSemiRingType.
Implicit Types x y : R.
Section FrobeniusAutomorphism.
Variables (p : nat) (pcharRp : p \in pchar R).
Lemma pFrobenius_aut_is_nmod_morphism : nmod_morphism (pFrobenius_aut pcharRp).
Proof.
Lemma pFrobenius_aut_is_monoid_morphism : monoid_morphism (pFrobenius_aut pcharRp).
Proof.
#[export]
HB.instance Definition _ := isNmodMorphism.Build R R (pFrobenius_aut pcharRp)
pFrobenius_aut_is_nmod_morphism.
#[export]
HB.instance Definition _ := isMonoidMorphism.Build R R (pFrobenius_aut pcharRp)
pFrobenius_aut_is_monoid_morphism.
End FrobeniusAutomorphism.
Lemma exprDn_pchar x y n : (pchar R).-nat n -> (x + y) ^+ n = x ^+ n + y ^+ n.
Proof.
pose p := pdiv n; have [|n_gt1 pcharRn] := leqP n 1; first by case: (n) => [|[]].
have pcharRp: p \in pchar R by rewrite (pnatPpi pcharRn) ?pi_pdiv.
have{pcharRn} /p_natP[e ->]: p.-nat n by rewrite -(eq_pnat _ (pcharf_eq pcharRp)).
by elim: e => // e IHe; rewrite !expnSr !exprM IHe -pFrobenius_autE rmorphD.
Qed.
have pcharRp: p \in pchar R by rewrite (pnatPpi pcharRn) ?pi_pdiv.
have{pcharRn} /p_natP[e ->]: p.-nat n by rewrite -(eq_pnat _ (pcharf_eq pcharRp)).
by elim: e => // e IHe; rewrite !expnSr !exprM IHe -pFrobenius_autE rmorphD.
Qed.
End ComNzSemiRingTheory.
#[short(type="comPzRingType")]
HB.structure Definition ComPzRing := {R of PzRing R & ComPzSemiRing R}.
HB.factory Record Zmodule_isComPzRing R & Zmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mulrC : commutative mul;
mul1r : left_id one mul;
mulrDl : left_distributive mul add;
}.
HB.builders Context R & Zmodule_isComPzRing R.
Definition mulr1 := Monoid.mulC_id mulrC mul1r.
Definition mulrDr := Monoid.mulC_dist mulrC mulrDl.
HB.instance Definition _ := Zmodule_isPzRing.Build R
mulrA mul1r mulr1 mulrDl mulrDr.
HB.instance Definition _ := SemiRing_hasCommutativeMul.Build R mulrC.
HB.end.
Module ComPzRingExports.
Bind Scope ring_scope with ComPzRing.sort.
End ComPzRingExports.
HB.export ComPzRingExports.
#[short(type="comNzRingType")]
HB.structure Definition ComNzRing := {R of NzRing R & ComNzSemiRing R}.
HB.factory Record Zmodule_isComNzRing R & Zmodule R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mulrC : commutative mul;
mul1r : left_id one mul;
mulrDl : left_distributive mul add;
oner_neq0 : one != zero
}.
HB.builders Context R & Zmodule_isComNzRing R.
HB.instance Definition _ := Zmodule_isComPzRing.Build R
mulrA mulrC mul1r mulrDl.
HB.instance Definition _ := PzSemiRing_isNonZero.Build R oner_neq0.
HB.end.
Module ComNzRingExports.
Bind Scope ring_scope with ComNzRing.sort.
End ComNzRingExports.
HB.export ComNzRingExports.
Section ComPzRingTheory.
Variable R : comPzRingType.
Implicit Types x y : R.
Lemma exprBn x y n :
(x - y) ^+ n =
\sum_(i < n.+1) ((-1) ^+ i * x ^+ (n - i) * y ^+ i) *+ 'C(n, i).
Proof.
Lemma subrXX x y n :
x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i).
Proof.
Lemma sqrrB x y : (x - y) ^+ 2 = x ^+ 2 - x * y *+ 2 + y ^+ 2.
Lemma subr_sqr x y : x ^+ 2 - y ^+ 2 = (x - y) * (x + y).
Lemma subr_sqrDB x y : (x + y) ^+ 2 - (x - y) ^+ 2 = x * y *+ 4.
Proof.
End ComPzRingTheory.
HB.mixin Record LSemiAlgebra_isSemiAlgebra R V & PzLSemiAlgebra R V := {
scalerAr : forall k (x y : V), k *: (x * y) = x * (k *: y);
}.
#[short(type="pzSemiAlgType")]
HB.structure Definition PzSemiAlgebra (R : pzSemiRingType) :=
{A of LSemiAlgebra_isSemiAlgebra R A & PzLSemiAlgebra R A}.
Module PzSemiAlgExports.
Bind Scope ring_scope with PzSemiAlgebra.sort.
End PzSemiAlgExports.
#[short(type="nzSemiAlgType")]
HB.structure Definition NzSemiAlgebra (R : nzSemiRingType) :=
{A of LSemiAlgebra_isSemiAlgebra R A & NzLSemiAlgebra R A}.
Module NzSemiAlgExports.
Bind Scope ring_scope with NzSemiAlgebra.sort.
End NzSemiAlgExports.
HB.factory Record LSemiAlgebra_isComSemiAlgebra R V
& ComPzSemiRing V & PzLSemiAlgebra R V := {}.
HB.builders Context R V & LSemiAlgebra_isComSemiAlgebra R V.
Lemma scalarAr k (x y : V) : k *: (x * y) = x * (k *: y).
HB.instance Definition _ := LSemiAlgebra_isSemiAlgebra.Build R V scalarAr.
HB.end.
HB.factory Record LSemiModule_isComSemiAlgebra R V
& ComPzSemiRing V & LSemiModule R V := {
scalerAl : forall (a : R) (u v : V), a *: (u * v) = (a *: u) * v
}.
HB.builders Context R V & LSemiModule_isComSemiAlgebra R V.
HB.instance Definition _ := LSemiModule_isLSemiAlgebra.Build R V scalerAl.
HB.instance Definition _ := LSemiAlgebra_isComSemiAlgebra.Build R V.
HB.end.
#[short(type="pzAlgType")]
HB.structure Definition PzAlgebra (R : pzRingType) :=
{A of LSemiAlgebra_isSemiAlgebra R A & PzLalgebra R A}.
Module PzAlgExports.
Bind Scope ring_scope with PzAlgebra.sort.
End PzAlgExports.
HB.export PzAlgExports.
#[short(type="nzAlgType")]
HB.structure Definition NzAlgebra (R : nzRingType) :=
{A of LSemiAlgebra_isSemiAlgebra R A & NzLalgebra R A}.
Module NzAlgExports.
Bind Scope ring_scope with NzAlgebra.sort.
End NzAlgExports.
HB.export NzAlgExports.
#[short(type="comPzSemiAlgType")]
HB.structure Definition ComPzSemiAlgebra (R : pzSemiRingType) :=
{V of ComPzSemiRing V & PzSemiAlgebra R V}.
Module ComPzSemiAlgExports.
Bind Scope ring_scope with ComPzSemiAlgebra.sort.
End ComPzSemiAlgExports.
HB.export ComPzSemiAlgExports.
#[short(type="comNzSemiAlgType")]
HB.structure Definition ComNzSemiAlgebra (R : nzSemiRingType) :=
{V of ComNzSemiRing V & NzSemiAlgebra R V}.
Module ComNzSemiAlgExports.
Bind Scope ring_scope with ComNzSemiAlgebra.sort.
End ComNzSemiAlgExports.
HB.export ComNzSemiAlgExports.
Section SemiAlgebraTheory.
#[export]
HB.instance Definition _ (R : comPzSemiRingType) :=
SemiRing_hasCommutativeMul.Build R^c (fun _ _ => mulrC _ _).
#[export]
HB.instance Definition _ (R : comPzSemiRingType) := ComPzSemiRing.on R^o.
#[export]
HB.instance Definition _ (R : comPzSemiRingType) :=
LSemiAlgebra_isComSemiAlgebra.Build R R^o.
#[export]
HB.instance Definition _ (R : comNzSemiRingType) := ComNzSemiRing.on R^c.
#[export]
HB.instance Definition _ (R : comNzSemiRingType) := ComNzSemiRing.on R^o.
End SemiAlgebraTheory.
#[short(type="comPzAlgType")]
HB.structure Definition ComPzAlgebra (R : pzRingType) :=
{V of ComPzRing V & PzAlgebra R V}.
Module ComPzAlgExports.
Bind Scope ring_scope with ComPzAlgebra.sort.
End ComPzAlgExports.
HB.export ComPzAlgExports.
#[short(type="comNzAlgType")]
HB.structure Definition ComNzAlgebra (R : nzRingType) :=
{V of ComNzRing V & NzAlgebra R V}.
Module ComNzAlgExports.
Bind Scope ring_scope with ComNzAlgebra.sort.
End ComNzAlgExports.
HB.export ComNzAlgExports.
Section AlgebraTheory.
#[export]
HB.instance Definition _ (R : comPzRingType) := ComPzRing.on R^c.
#[export]
HB.instance Definition _ (R : comPzRingType) := ComPzRing.on R^o.
#[export]
HB.instance Definition _ (R : comNzRingType) := ComNzRing.on R^c.
#[export]
HB.instance Definition _ (R : comNzRingType) := ComNzRing.on R^o.
End AlgebraTheory.
Section SemiAlgebraTheory.
Variables (R : pzSemiRingType) (A : pzSemiAlgType R).
Implicit Types (k : R) (x y : A).
Lemma scalerCA k x y : k *: x * y = x * (k *: y).
Lemma mulr_algr a x : x * a%:A = a *: x.
Lemma comm_alg a x : comm a%:A x.
Lemma exprZn k x n : (k *: x) ^+ n = k ^+ n *: x ^+ n.
Proof.
Lemma scaler_prod I r (P : pred I) (F : I -> R) (G : I -> A) :
\prod_(i <- r | P i) (F i *: G i) =
\prod_(i <- r | P i) F i *: \prod_(i <- r | P i) G i.
Proof.
Lemma scaler_prodl (I : finType) (S : pred I) (F : I -> A) k :
\prod_(i in S) (k *: F i) = k ^+ #|S| *: \prod_(i in S) F i.
Proof.
Lemma scaler_prodr (I : finType) (S : pred I) (F : I -> R) x :
\prod_(i in S) (F i *: x) = \prod_(i in S) F i *: x ^+ #|S|.
Proof.
End SemiAlgebraTheory.
Section AlgebraTheory.
Variables (R : pzSemiRingType) (A : pzSemiAlgType R).
Variables (U : lSemiModType R) (a : A) (f : {linear U -> A}).
Lemma mull_fun_is_scalable : scalable (a \*o f).
#[export]
HB.instance Definition _ := isScalable.Build R U A *:%R (a \*o f)
mull_fun_is_scalable.
End AlgebraTheory.
Module ClosedExports.
Notation nmod_closed := nmod_closed.
Notation oppr_closed := oppr_closed.
Notation zmod_closed := zmod_closed.
Notation mulr_closed := mulr_closed.
Notation semiring_closed := semiring_closed.
Notation smulr_closed := smulr_closed.
Notation subring_closed := subring_closed.
Notation scaler_closed := scaler_closed.
Notation subsemimod_closed := subsemimod_closed.
Notation linear_closed := linear_closed.
Notation submod_closed := submod_closed.
Notation subalg_closed := subalg_closed.
Coercion zmod_closed0D : zmod_closed >-> nmod_closed.
Coercion zmod_closedN : zmod_closed >-> oppr_closed.
Coercion semiring_closedD : semiring_closed >-> nmod_closed.
Coercion semiring_closedM : semiring_closed >-> mulr_closed.
Coercion smulr_closedM : smulr_closed >-> mulr_closed.
Coercion smulr_closedN : smulr_closed >-> oppr_closed.
Coercion subring_closedB : subring_closed >-> zmod_closed.
Coercion subring_closedM : subring_closed >-> smulr_closed.
Coercion subring_closed_semi : subring_closed >-> semiring_closed.
Coercion subsemimod_closedD : subsemimod_closed >-> nmod_closed.
Coercion subsemimod_closedZ : subsemimod_closed >-> scaler_closed.
Coercion linear_closedB : linear_closed >-> subr_closed.
Coercion submod_closedB : submod_closed >-> zmod_closed.
Coercion submod_closed_semi : submod_closed >-> subsemimod_closed.
Coercion subsemialg_closedZ : subsemialg_closed >-> subsemimod_closed.
Coercion subsemialg_closedM : subsemialg_closed >-> semiring_closed.
Coercion subalg_closedZ : subalg_closed >-> submod_closed.
Coercion subalg_closedBM : subalg_closed >-> subring_closed.
Coercion subalg_closed_semi : subalg_closed >-> subsemialg_closed.
End ClosedExports.
HB.mixin Record isMul2Closed (R : pzSemiRingType) (S : {pred R}) := {
rpredM : mulr_2closed S
}.
HB.mixin Record isMul1Closed (R : pzSemiRingType) (S : {pred R}) := {
rpred1 : 1 \in S
}.
HB.mixin Record isScaleClosed (R : pzSemiRingType) (V : lSemiModType R)
(S : {pred V}) := {
rpredZ : scaler_closed S
}.
Local Notation addrClosed := addrClosed.
Local Notation opprClosed := opprClosed.
#[short(type="mulr2Closed")]
HB.structure Definition Mul2Closed (R : pzSemiRingType) :=
{S of isMul2Closed R S}.
#[short(type="mulrClosed")]
HB.structure Definition MulClosed (R : pzSemiRingType) :=
{S of Mul2Closed R S & isMul1Closed R S}.
#[short(type="semiring2Closed")]
HB.structure Definition Semiring2Closed (R : pzSemiRingType) :=
{S of AddClosed R S & Mul2Closed R S}.
#[short(type="semiringClosed")]
HB.structure Definition SemiringClosed (R : pzSemiRingType) :=
{S of AddClosed R S & MulClosed R S}.
#[short(type="smulClosed")]
HB.structure Definition SmulClosed (R : pzRingType) :=
{S of OppClosed R S & MulClosed R S}.
#[short(type="subringClosed")]
HB.structure Definition SubringClosed (R : pzRingType) :=
{S of ZmodClosed R S & MulClosed R S}.
#[short(type="submodClosed")]
HB.structure Definition SubmodClosed (R : pzSemiRingType) (V : lSemiModType R)
:= {S of AddClosed V S & isScaleClosed R V S}.
#[short(type="subalgClosed")]
HB.structure Definition SubalgClosed (R : pzSemiRingType) (A : pzLSemiAlgType R)
:= {S of SemiringClosed A S & isScaleClosed R A S}.
HB.factory Record isMulClosed (R : pzSemiRingType) (S : {pred R}) := {
rpred1M : mulr_closed S
}.
HB.builders Context R S & isMulClosed R S.
HB.instance Definition _ := isMul2Closed.Build R S (proj2 rpred1M).
HB.instance Definition _ := isMul1Closed.Build R S (proj1 rpred1M).
HB.end.
HB.factory Record isSmulClosed (R : pzRingType) (S : R -> bool) := {
smulr_closed_subproof : smulr_closed S
}.
HB.builders Context R S & isSmulClosed R S.
HB.instance Definition _ := isMulClosed.Build R S
(smulr_closedM smulr_closed_subproof).
HB.instance Definition _ := isOppClosed.Build R S
(smulr_closedN smulr_closed_subproof).
HB.end.
HB.factory Record isSemiringClosed (R : pzSemiRingType) (S : R -> bool) := {
semiring_closed_subproof : semiring_closed S
}.
HB.builders Context R S & isSemiringClosed R S.
HB.instance Definition _ := isAddClosed.Build R S
(semiring_closedD semiring_closed_subproof).
HB.instance Definition _ := isMulClosed.Build R S
(semiring_closedM semiring_closed_subproof).
HB.end.
HB.factory Record isSubringClosed (R : pzRingType) (S : R -> bool) := {
subring_closed_subproof : subring_closed S
}.
HB.builders Context R S & isSubringClosed R S.
HB.instance Definition _ := isZmodClosed.Build R S
(subring_closedB subring_closed_subproof).
HB.instance Definition _ := isSmulClosed.Build R S
(subring_closedM subring_closed_subproof).
HB.end.
HB.factory Record isSubSemiModClosed (R : pzSemiRingType) (V : lSemiModType R)
(S : V -> bool) := {
subsemimod_closed_subproof : subsemimod_closed S
}.
HB.builders Context R V S & isSubSemiModClosed R V S.
HB.instance Definition _ := isAddClosed.Build V S
(subsemimod_closedD subsemimod_closed_subproof).
HB.instance Definition _ := isScaleClosed.Build R V S
(subsemimod_closedZ subsemimod_closed_subproof).
HB.end.
HB.factory Record isSubmodClosed (R : pzRingType) (V : lmodType R)
(S : V -> bool) := {
subsemimod_closed_subproof : subsemimod_closed S
}.
HB.builders Context R V S & isSubmodClosed R V S.
HB.instance Definition _ := isZmodClosed.Build V S
(subsemimod_closedB subsemimod_closed_subproof).
HB.instance Definition _ := isScaleClosed.Build R V S
(subsemimod_closedZ subsemimod_closed_subproof).
HB.end.
HB.factory Record isSubSemiAlgClosed (R : pzSemiRingType) (A : pzLSemiAlgType R)
(S : A -> bool) := {
subsemialg_closed_subproof : subsemialg_closed S
}.
HB.builders Context R A S & isSubSemiAlgClosed R A S.
HB.instance Definition _ := isSubSemiModClosed.Build R A S
(subsemialg_closedZ subsemialg_closed_subproof).
HB.instance Definition _ := isSemiringClosed.Build A S
(subsemialg_closedM subsemialg_closed_subproof).
HB.end.
HB.factory Record isSubalgClosed (R : pzRingType) (A : pzLalgType R)
(S : A -> bool) := {
subsemialg_closed_subproof : subsemialg_closed S
}.
HB.builders Context R A S & isSubalgClosed R A S.
HB.instance Definition _ := isSubmodClosed.Build R A S
(subsemialg_closedZ subsemialg_closed_subproof).
HB.instance Definition _ := isSemiringClosed.Build A S
(subsemialg_closedM subsemialg_closed_subproof).
HB.end.
Section SemiRingPred.
Variables (R : pzSemiRingType).
Section Mul.
Variable S : mulrClosed R.
Lemma rpred1M : mulr_closed S.
Lemma rpred_prod I r (P : pred I) F :
(forall i, P i -> F i \in S) -> \prod_(i <- r | P i) F i \in S.
Lemma rpredX n : {in S, forall u, u ^+ n \in S}.
Proof.
End Mul.
Lemma rpred_nat (S : semiringClosed R) n : n%:R \in S.
Lemma semiringClosedP (rngS : semiringClosed R) : semiring_closed rngS.
End SemiRingPred.
Section RingPred.
Variables (R : pzRingType).
Lemma rpredMsign (S : opprClosed R) n x : ((-1) ^+ n * x \in S) = (x \in S).
Lemma rpredN1 (S : smulClosed R) : -1 \in S.
Lemma rpred_sign (S : smulClosed R) n : (-1) ^+ n \in S.
Lemma subringClosedP (rngS : subringClosed R) : subring_closed rngS.
End RingPred.
Section LmodPred.
Variables (R : pzSemiRingType) (V : lSemiModType R).
Lemma rpredZnat (S : addrClosed V) n : {in S, forall u, n%:R *: u \in S}.
Proof.
Lemma subsemimodClosedP (modS : submodClosed V) : subsemimod_closed modS.
End LmodPred.
Section LmodPred.
Variables (R : pzRingType) (V : lmodType R).
Lemma rpredZsign (S : opprClosed V) n u : ((-1) ^+ n *: u \in S) = (u \in S).
Lemma submodClosedP (modS : submodClosed V) : submod_closed modS.
Proof.
End LmodPred.
Section LalgPred.
Variables (R : pzSemiRingType) (A : pzLSemiAlgType R).
Lemma subsemialgClosedP (algS : subalgClosed A) : subsemialg_closed algS.
End LalgPred.
Section LalgPred.
Variables (R : pzRingType) (A : pzLalgType R).
Lemma subalgClosedP (algS : subalgClosed A) : subalg_closed algS.
Proof.
End LalgPred.
HB.mixin Record isSubPzSemiRing (R : pzSemiRingType) (S : pred R) U
& SubNmodule R S U & PzSemiRing U := {
valM_subproof : monoid_morphism (val : U -> R);
}.
#[short(type="subPzSemiRingType")]
HB.structure Definition SubPzSemiRing (R : pzSemiRingType) (S : pred R) :=
{ U of SubNmodule R S U & PzSemiRing U & isSubPzSemiRing R S U }.
#[short(type="subNzSemiRingType")]
HB.structure Definition SubNzSemiRing (R : nzSemiRingType) (S : pred R) :=
{ U of SubNmodule R S U & NzSemiRing U & isSubPzSemiRing R S U }.
Section multiplicative.
Context (R : pzSemiRingType) (S : pred R) (U : SubPzSemiRing.type S).
Notation val := (val : U -> R).
#[export]
HB.instance Definition _ := isMonoidMorphism.Build U R val valM_subproof.
Lemma val1 : val 1 = 1
Proof.
Proof.
Proof.
HB.factory Record SubNmodule_isSubPzSemiRing (R : pzSemiRingType) S U
& SubNmodule R S U := {
mulr_closed_subproof : mulr_closed S
}.
HB.builders Context R S U & SubNmodule_isSubPzSemiRing R S U.
HB.instance Definition _ := isMulClosed.Build R S mulr_closed_subproof.
Let inU v Sv : U := Sub v Sv.
Let oneU : U := inU (@rpred1 _ (MulClosed.clone R S _)).
Let mulU (u1 u2 : U) := inU (rpredM _ _ (valP u1) (valP u2)).
Lemma mulrA : associative mulU.
Lemma mul1r : left_id oneU mulU.
Lemma mulr1 : right_id oneU mulU.
Lemma mulrDl : left_distributive mulU +%R.
Lemma mulrDr : right_distributive mulU +%R.
Lemma mul0r : left_zero 0%R mulU.
Lemma mulr0 : right_zero 0%R mulU.
HB.instance Definition _ := Nmodule_isPzSemiRing.Build U
mulrA mul1r mulr1 mulrDl mulrDr mul0r mulr0.
Lemma valM : monoid_morphism (val : U -> R).
Proof.
HB.end.
HB.factory Record SubPzSemiRing_isNonZero (R : nzSemiRingType) S U
& SubPzSemiRing R S U := {}.
HB.builders Context R S U & SubPzSemiRing_isNonZero R S U.
Lemma oner_neq0 : (1 : U) != 0.
HB.instance Definition _ := PzSemiRing_isNonZero.Build U oner_neq0.
HB.end.
HB.factory Record SubNmodule_isSubNzSemiRing (R : nzSemiRingType) S U
& SubNmodule R S U := {
mulr_closed_subproof : mulr_closed S
}.
HB.builders Context R S U & SubNmodule_isSubNzSemiRing R S U.
HB.instance Definition _ := SubNmodule_isSubPzSemiRing.Build R S U
mulr_closed_subproof.
HB.instance Definition _ := SubPzSemiRing_isNonZero.Build R S U.
HB.end.
#[short(type="subComPzSemiRingType")]
HB.structure Definition SubComPzSemiRing (R : pzSemiRingType) S :=
{U of SubPzSemiRing R S U & ComPzSemiRing U}.
HB.factory Record SubSemiRing_isSubComSemiRing (R : comPzSemiRingType) S U
& SubPzSemiRing R S U := {}.
HB.builders Context R S U & SubSemiRing_isSubComSemiRing R S U.
Lemma mulrC : @commutative U U *%R.
HB.instance Definition _ := SemiRing_hasCommutativeMul.Build U mulrC.
HB.end.
#[short(type="subComNzSemiRingType")]
HB.structure Definition SubComNzSemiRing (R : nzSemiRingType) S :=
{U of SubNzSemiRing R S U & ComNzSemiRing U}.
#[short(type="subPzRingType")]
HB.structure Definition SubPzRing (R : pzRingType) (S : pred R) :=
{ U of SubPzSemiRing R S U & PzRing U & isSubZmodule R S U }.
#[short(type="subNzRingType")]
HB.structure Definition SubNzRing (R : nzRingType) (S : pred R) :=
{ U of SubNzSemiRing R S U & NzRing U & isSubBaseAddUMagma R S U }.
#[short(type="subComPzRingType")]
HB.structure Definition SubComPzRing (R : pzRingType) S :=
{U of SubPzRing R S U & ComPzRing U}.
#[short(