Explanations

This page is a reference for various topics and concepts.

For now, such information has not been moved to set.mm/iset.mm but they may be moved in the future.

Polynomial definitions

~ df-frlm

This is described as some background.

( R freeLMod I ) is a structure whose base is { x e. ( R ^m I ) | ( x finSupp ( 0g ` ( Base ` R ) ) }, i.e. functions I --> R with finite support.

• I is the set of indices, they represent "variables" in polynomials.
• R is the structure of values, usually at least a Ring

For simplicity, the indices will be 0, 1, 2, etc.

As such, the base of ( R freeLMod I ) are vectors <" a_R b_R c_R ... ">

Addition and multiplication is component-wise, and scalars (in R) work as expected.

~ df-psr

The structure of power series is basically ( R freeLMod I ) but the vectors can be of infinite length (finite support not necessary), the indices are bags of variables, and the values are coefficients.

A bag of variables is a function mapping each variable to its exponent. Thus power series are functions:

( ( variables --> exponents ) --> coefficients )

Addition works just like df-frlm's vector addition, but multiplication is modified to work for polynomials.

~ df-mpl

The structure of polynomials add back the restriction that the vectors be of finite length.

(Technically finite support means that the function has a finite amount of non-zero values)

~ df-mvr , ~ df-ascl

algSc takes a scalar and multiplies it by the unit vector.

For polynomials, scalars become constant polynomials. For example, 2_s becomes 2_p (specifically, if( bag maps all vars to 0, coef 2, coef 0 ))

mVar makes a variable a polynomial. For example, x_i becomes x_p (specifically, if( bag maps only x to 1, coef 1, coef 0 ))

~ df-evls

( ( I evlsSub S ) ` R ) is basically ( I eval S ) but with extra information that the coefficients of the polynomial are in a subring R C_ ( Base ` S )

Its value is determined by ~ evlsval2 , informally:

• eval(A+B) = eval(A) + eval(B)
• eval(A*B) = eval(A) * eval(B)
• eval(c) = ( assignment --> c ) (constant polynomials are evaluated to the constants, no matter the assignment)
• eval(x) = ( assignment --> (assignment`x) ) (variables are evaluated to what the assignment assigned)

. While technically ~ evlslem1 is the actual formula, it doesn't seem to be needed. But here's the formula anyway for completeness:

E = ( p e. B |-> ( U gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
B = ( Base ` P )
P = ( I mPoly ( S |`s R ) )
F = ( x e. R |-> ( ( B ^m I ) x. { x } ) )
G = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) )
U = ( S ^s ( B ^m I ) )
T = ( mulGrp ` U )
.^ = ( .g ` T )
.x. = ( .r ` U )
D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
( ph -> I e. W )
( ph -> R e. CRing )
---
( ph -> E = ( ( I evalSub S ) ` R ) )

E sums over each bag, taking the coefficient of the polynomial p at the bag, and multiplying that by the product of each variable raised to the corresponding power of the bag. 

~ df-evl

( I eval S ) : polynomial (...) --> ( assignments ( vars I --> values S ) --> evalvalue S )

• ( I eval S ) evaluates the polynomial with the given assignments, returning the result.

~ df-selv

TODO, here's my discord comment

The comment says what selectVars does is:
( ( I selectVars R ) ` J ) : ( I mPoly R ) -1-1-onto-> ( J mPoly ( ( I / J ) mPoly R ) )

This might be useful if we only want to evaluate some variables (` J `) but not others (` I / J `).
After I R and J, there is only one more parameter/argument: F:

$d c d f i j r t u x $.
76917 df-selv $a |- selectVars = ( i e. _V , r e. _V |-> ( j e. ~P i |->
      ( f e. ( Base ` ( i mPoly r ) ) |->
             [_ ( ( i \ j ) mPoly r ) / u ]_
             [_ ( j mPoly u ) / t ]_
             [_ ( algSc ` t ) / c ]_
             [_ ( c o. ( algSc ` u ) ) / d ]_
               ( ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) `
                 ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) )
               ) ) ) ) $.

Let's first look at ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) )

[_ A / x ]_ is an inline variable assignment, it assigns the class ` A ` to ` x `
So t is ( J mPoly u ) where u is ( ( I / J ) mPoly R )

t is ( J mPoly ( ( I / J ) mPoly R ) )
Passing t into evalSub, we are evaluating a polynomial whose values are... polynomials in T.
The result will be a value... a polynomial in T, exactly what we want.

A polynomial whose values are polynomials in T will be in the form:
  ( I --> NN0 ) --> coefficients ( polynomials in T )

But f is in the form
  ( I --> NN0 ) --> values R C_ Base`S

So d is there, it applies ` algSc ` twice, turning the value of R first into u, and then t

----
We now look at the assignments. We evaluate ( d o. f ) as follows:
  ( x e. i |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) ) )

  if x e. j , assign x to x as a polynomial in t
  else, assign x to x as a polynomial in u... but then use c so it's a polynomial in t

In other words this is like assigning each variable ` x ` to "a value"... a polynomial ` x ` in T
`evalSub` finally takes all these "values" in T and adds them up to make... ` f ` but in T