Implement algebra evaluation and substitution: `aeval` and `bind₁`

[dhsorens]

Implement algebra evaluation and substitution: aeval and bind₁

Summary

Implement algebra evaluation (aeval) and polynomial substitution (bind₁) for multivariate polynomials. These are fundamental operations for evaluating polynomials in algebras and composing polynomials.

Context

Part of Phase 1: Foundation Completion (API completeness) as outlined in ROADMAP.md line 55. These functions are essential for working with polynomial algebras and are commonly used in Mathlib.

What to Implement

1. aeval {n : ℕ} {R σ : Type} [CommSemiring R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p : CMvPolynomial n R) : σ

   • Algebra evaluation: evaluates polynomial in an algebra
   • Given an algebra σ over R and a function f : Fin n → σ, evaluates the polynomial
   • Location: CompPoly/Multivariate/CMvPolynomial.lean line 207

2. bind₁ {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : CMvPolynomial m R

   • Substitution: substitutes polynomials for variables
   • Given f : Fin n → CMvPolynomial m R, substitutes f i for variable X i
   • Location: CompPoly/Multivariate/CMvPolynomial.lean line 215

Dependencies

• eval₂ (already exists) - can be used as a building block for aeval
• Algebra typeclass from Mathlib
• CMvPolynomial multiplication and addition (for bind₁)
• monomial constructor (for building substituted terms)

Implementation Notes

aeval

• Can likely implement via eval₂ using algebraMap R σ as the ring homomorphism
• For each monomial m with coefficient c, compute algebraMap R σ c * ∏ᵢ (f i)^(m[i])
• Sum over all monomials

bind₁

• For each monomial m with coefficient c, compute c * ∏ᵢ (f i)^(m[i])
• Sum over all monomials
• Can use aeval with CMvPolynomial m R as the algebra, or implement directly

Properties to Prove

• aeval f (C c) = algebraMap R σ c
• aeval f (X i) = f i
• aeval f (p + q) = aeval f p + aeval f q
• aeval f (p * q) = aeval f p * aeval f q
• bind₁ f (C c) = C c
• bind₁ f (X i) = f i
• bind₁ f (p + q) = bind₁ f p + bind₁ f q
• bind₁ f (p * q) = bind₁ f p * bind₁ f q
• bind₁ (fun i => X i) p = p (identity substitution)

Mathlib References

• MvPolynomial.aeval - Similar concept in Mathlib
• MvPolynomial.bind₁ - Similar concept in Mathlib
• MvPolynomial.eval₂Hom - Related evaluation homomorphism

Success Criteria

• aeval correctly evaluates polynomials in an algebra
• bind₁ correctly substitutes polynomials for variables
• All basic properties are proven (see above)
• Relationship with eval₂ is established

Tags

• phase-1
• api-completeness
• multivariate-polynomials
• algebra

[DimitriosMitsios]

@dhsorens Is anybody working on it? If not, can I take it?

[dhsorens]

No one that I know of!

[DimitriosMitsios]

Ok, I will start looking into it!