Commit 2025-03-31 07:56 5fc21982

feat(RingTheory/PolynomialLaw/Basic): definition and elementary properties of polynomial laws (#22912) Let M and N be a modules over a commutative ring R. A polynomial law f : PolynomialLaw R M N, with notation f : M →ₚ[R] N, is a “law” that assigns, to every R-algebra S,

• a map PolynomialLaw.toFun' f S : S ⊗[R] M → S ⊗[R] N,
• compatibly with morphisms of R-algebras, as expressed by PolynomialLaw.isCompat' f These expressions behave as “polynomials from M to N“. This PR is the first of a series that formalizes their properties. They will be used for the study of the universal divided power algebra. Coauthored with @mariainesdff