Definition of product of polynomials.
Meta Kunt
R (commutative ring with 1)
F: ( ZZ i^i Fin) --> NN0 (Maps from subset of integers to nonnegative integers.
I'd like to define the following two polynomials in R[X].
Given the canonical embedding from ZZ to R, which is denoted by s and a F with above domain and codomain,
\begin{equation*}
g=\prod_{i\in \mathrm{dom} F}(x- s(i))^{F(i))
\end{equation*}
This should be a polynomial in R[X].
I'd also like to define for r in R and a positive integers e the following two polynomials.
g(x^e) and g(x)^e, both as polynomials of R[X]
g is the product of finitely many monomials (x-s(a))
h1 =g(x^e)
h2= g(x)^e
I can't see how I can define the polynomials at the easiest.
The closest I can find is this https://us.metamath.org/mpeuni/lply1binomsc.html
But I need the product of polynomials and not the sum.
Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.
Thierry Arnoux
Hi!
The `R gsum F` operation is a repeated group operation, but from a ring `R`, one can get the multiplicative group `M = (mulGrp ` R )`.
Then `M gsum F` becomes a repeated multiplicative operation,
which is what you need here (the product of a list of factors).
There is also a `( .g ` R )` group multiple function, which is a repeated group operation (every term is the same). When used on the multiplicative group, it is the exponentiation you need.
As a side note, in the case of a the decomposition of a polynomial, maybe you could use a single function, without powers:
\begin{equation*}
g=\prod_{i\in \mathrm{dom} s}(x- s(i))
\end{equation*}
Then all roots are simple when `s` is injective.
This might make things easier.
BR,
_
Thierry
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/3c80deb45e287639d48927a3bde99078%40mail.eclipso.de.
Meta Kunt
I've tried, painstakingly, to match the definitions. A typo now would be horrific.
Reference: https://www3.nd.edu/~andyp/notes/AKS.pdf
1:: |- ( ph -> K e. Field )
2:: |- R = ( Poly1 ` K )
3:: |- B = ( Base ` K )
4:: |- X = ( var1 ` K )
5:: |- W = ( mulGrp ` R )
6:: |- M = ( mulGrp ` K )
7:: |- D = ( .g ` M )
8:: |- C = ( algSc ` W )
9:: |- E = ( .g ` W )
10:: |- P = ( chr ` K )
11:: |- ( ph -> ( Q C_ ZZ /\ Q e. Fin ) )
12:: |- F = { g | ( g : ZZ --> NN0 /\ ( g supp 0 ) = Q ) }
13:: |- ( ph -> P e. Prime )
14:: |- I = { x e. ( NN X. B ) | A. r e. S th }
15:: |- O = ( eval1 ` K )
16:: |- .- = ( -g ` R )
17:: |- T = ( f e. F |-> ( W gsum ( z e. ZZ |-> ( ( f ` z ) E ( X .- ( C ` ( ( ZRHom ` K ) ` z ) ) ) ) ) ) )
18:: |- ( th <-> ( ( 1st ` x ) D ( ( O ` ( 2nd ` x ) ) ` r ) ) = ( ( O ` ( 2nd ` x ) ) ` ( ( 1st ` x ) D r ) ) )
The explanation for the following lines.
1: K is a field, in our case it will be an algebraic closure of Fp, I think we'll need the Euclidean ring.
2: R=K[X], the polynomial ring in one variable
3: B are the elements of K[X]
4: The monomial X of K[X]
5: W is the multiplicative monoid of K[X] with the multiplication as operation (+g)
6: M, but with the Field K.
7: Group exponentiation of K. in CC ( 3 D 2 ) = ( 2 ^ 3 ) = 9
8: The scalars of K[X], which is "left scalar multiplication with K"
9: Same, but with the polynomial ring K[X], for example in Z[X] ( 2 E ( X + 1 ) ) = ( X^2+2X+1) (informally)
10,13: K with prime characteristic.
11: A finite subset of ZZ, in corresponds to the following integers 0 ≤ ai ≤ ⌊pϕ(r) log n⌋ (11 INFO)
12: This is a bit more complicated, this is data necessary to define P. Here is an example: assume f that is in F with f(2)=3. Then the polynomial under T would be ( x-2)^3, where the 2 is in K. This "transfers" information of the monic linear factors to the product of polynomials in K[X]
14: Definition of the introspective property. In the literature we have (e,f), we want to say that (e,f) is introspective when for all r-th primitive roots S, which by abuse of notation we also call r (in the literature this is \mu) the property 18 holds.
15: Polynomial evaluation of K[X]
16: Polynomial subtraction of K[X]
17: Define the elements of the literature script P as a product of finitely many linear factors, where the offsets are bounded by [11 INFO]
18: (μ)e ≡ f (μe) in Fp in the literature.
Did I make any mistakes? Hint: I want to show that for every e \in Literature script E and every f \in Literature script P that e and f are introspective.
Claim 1(i) shows it for the monomials f=(x-a) and e=n/p, and e=p
Claim 1(ii) shows it for the product of f. In our case this corresponds to the pointwise sum of elements of F.
Claim 1(iii) shows it for the products of e. Here we need the properties of primitive roots and the fact that all elements of e are coprime to r. That's why \mu^e is also a primitive root, see the definition of 14 and recall that in this definition S stands for primitive roots.
If everything is fine I would like to formalise the statements and collect some more feedback before I start to formalising Claim 1. In our Case, transcribed it would be ( ph -> A. e e. ( (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) `` ( NN0 X. NN0 )) A. f e. ( T `` F ) -> e I f )
Feedback would be immensely helpful, as I need to put several definitions in place, in particular I will need PerfectRings, PrimitiveRoots, maybe even roots of unity. I don't know yet what API I will need to formalise before I can tackle this statement.
Thierry Arnoux
Hi Metakunt!
This looks quite good - my remarks:
- you'll probably need to add additional properties of the field
`K` for the claims (i), (ii) or (iii)
- I think B should be ( Base ` R ) instead (that's the set of
polynomials considered)
- for the exponentiation operation D, you could use the class
variable `.^` , it might make things a bit clearer,
- do you really need negative exponents? Would Q C_ NN0 instead of
Q C_ ZZ suffice ?
- I would probably have formalized this in a more direct way: for
example take a concrete `G : ZZ --> NN0`, and directly assume
its properties:
|- ph -> G : ZZ --> NN0
|- ph -> ( G supp 0 ) e. Fin ( you don't need ( G supp 0 )
C_ ZZ , you can deduce it from its domain )
- same for I and x: I would have taken a F instead of ( 2nd ` x )
and an E instead of ( 1st ` x ) (assuming we free the letters!):
|- ph -> F e. B <or some other smaller set depending
on (i), (ii), (iii) >
|- ph -> E e. NN <or some other smaller set depending on
(i), (ii), (iii) >
- same for r, let's take a concrete \mu (say, Y) :
|- ph -> Y e. ( Base ` K )
|- ph -> ( S D Y ) = ( 1r ` K ) (taking S for r)
- you also need conditions on S, like 2 <_ S, ( S gcd N ) = 1,
etc., which I don't see in your statement. Maybe you could swap my
S and R to keep the same letters as in the paper!
Then your final statement becomes:
qed:: |- ph -> ( E .^ ( ( O ` F ) ` Y ) ) = ( ( ( O ` F ) ` ( E D Y ) ) )
qed:: |- ph -> E .~ F
(I've dropped a few parentheses around the ( ph -> ... ) !)
3:: |- B = ( Base ` S )
4:: |- X = ( var1 ` S )
5:: |- W = ( mulGrp ` S )
6:: |- V = ( mulGrp ` K )
7:: |- .^ = ( .g ` V )
8:: |- C = ( algSc ` W )
10:: |- P = ( chr ` K )
12:: |- .- = ( -g ` S )
12:: |- ( ph -> K e. Field )
13:: |- ( ph -> P e. Prime )
19:: |- ( ph -> E e. NN )
qed:: |- ( ph -> E .~ F )
Maybe for (ii) something like:
20:: |- ( ph -> M e. NN )
21:: |- ( ph -> G : ( 0 ..^ M ) --> NN0 )
22:: |- ( ph -> F = ( V gsum ( x e. ( 0 ..^ M ) |-> ( X .- (
C ` ( ( ZRHom ` K ) ` ( G ` x ) ) ) )
23:: |- ( ph -> I e. NN0 )
24:: |- ( ph -> J e. NN0 )
25:: |- ( ph -> E = ( ( N / P ) ^ I ) .x. ( P ^ J ) )
qed:: |- ( ph -> E .~ F )
I hope this is clear!
_
Thierry
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/529b6b8d724cff6c3a66478989cc8f0a%40mail.eclipso.de.