metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

move polynomial section #3995

Closed icecream17 closed 2 months ago

icecream17 commented 3 months ago

reason

~ df-mhp is wrong

The sum is over I not NN0, since g : I --> NN0.

This change also means df-gsum needs to be used instead of df-sum, since I can technically be infinite in size, and is not necessarily a range over the integers. (The defining property of I is being finely supported, which gsum handles nicely).

And since we are summing numbers, we need a structure whose base set includes NN0...

Unfortunately the complex numbers as an algebraic structure (and various substructures) come in the section right after the polynomials

So I propose to move the polynomial section.

where

While simply moving it right after the number structures is the obvious move, I would actually like to move it somewhere after "vectors and free modules" because both seem potentially useful.

For instance, compare ~ frlmelbas and ~ mplelbas, or note how https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz#Formulation represents the "Assignments" below as a vector

evaluated polynomial = ((IndexVars eval Structure)`Polynomial)`(AssignmentsFromIVarsToStructValues)

though it could also go right before "Polynomial matrices" two sections after

tirix commented 3 months ago

Just to be explicit : I support the move. If you look in the direction of the Nullstellensatz you'll also need a lot about Ideals, too.

avekens commented 3 months ago

Until now, only @tirix agreed with this restructuring. I have not a clear opionion about it yet. @benjub @digama0 what's your opinion?

icecream17 commented 3 months ago

for clarity, given the new df-mhp, the section can go anywhere after "Complex numbers as an algebraic structure" and before "Polynomial matrices" (2 sections after "Matrices")

The pr moves the section right before "Matrices"

image

Edit: Now that I look closer, I'm starting to think it should go right before "Polynomial matrices"...

benjub commented 3 months ago

I agree. I'd move both "10.8 Associative Algebras" and "10.9 Multivariate Polynomials" (no need for "Abstract" in the title IMO) after "Vector spaces and free modules". Actually, there is also some linear algebra lost in Part 10 which should be moved at the beginning of Part 11 (can be done later, and not sure how much of it, if any, is needed by the section on complex numbers).

Actually, algebras and polynomials should go in a new Part 12, "Multilinear Algebra" (can be done later).

tirix commented 3 months ago

Can we move forward with this and #4014 ? I don't see any disagreement for the move.

icecream17 commented 3 months ago

I guess 10.8 Associative Algebras can be moved in a follow up pr