where I and J are types which function as index-types for the variables in the generalized polynomial-rings R[I] and R[I][J]. This can be used to show that
R[Fin n][Fin m] = R[Fin (n+m)]
which are the standard multivariate polynomials in n,m and n+m variables. This also works for sets merely equivalent to some Fin k, so a version with actions of permutations can also be defined.
The PR also adds base change for commutative algebras (from R-Algebras to S-Algebras along a hom f:S->R).
This PR is about proving the relation
where
IandJare types which function as index-types for the variables in the generalized polynomial-ringsR[I]andR[I][J]. This can be used to show thatwhich are the standard multivariate polynomials in n,m and n+m variables. This also works for sets merely equivalent to some
Fin k, so a version with actions of permutations can also be defined. The PR also adds base change for commutative algebras (from R-Algebras to S-Algebras along a hom f:S->R).