Multilinear maps along polynomial paths

Let A be an algebra over a field R of characteristic zero, possibly noncommutative, and let φ be an R-multilinear map on A. A family p of polynomials with coefficients in A gives a polynomial path t ↦ (p l)(t) in each argument, where t ∈ R is evaluated through the central embedding algebraMap R A. Along such paths t ↦ φ((p l)(t)) is a polynomial function of t, and its derivative is given by the Leibniz rule ∑ₖ φ((p 0)(t), …, (p k)′(t), …), that is, by MultilinearMap.linearDeriv at (p l)(t) in the direction (p l)′(t).

This file proves the resulting zero-derivative principle: if this derivative vanishes for every t, then φ((p l)(t)) does not depend on t. It is the algebraic form of homotopy invariance used for multilinear invariants evaluated along polynomial families, such as the pairing of cyclic cocycles with polynomial paths of idempotents.

Main results

• MultilinearMap.apply_eval_algebraMap_eq_of_linearDeriv_eq_zero: a multilinear map is constant along polynomial paths whose Leibniz derivative vanishes identically.

theorem MultilinearMap.apply_eval_algebraMap_eq_of_linearDeriv_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq ι] [Field R] [CharZero R] [Semiring A] [Algebra R A] [AddCommGroup M] [Module R M] (φ : (ι → A) →ₘₗ[R] M) (p : ι → Polynomial A) (h : ∀ (t : R), ((φ.linearDeriv fun (l : ι) => Polynomial.eval ((algebraMap R A) t) (p l)) fun (l : ι) => Polynomial.eval ((algebraMap R A) t) (Polynomial.derivative (p l))) = 0) (s t : R) : (φ fun (l : ι) => Polynomial.eval ((algebraMap R A) s) (p l)) = φ fun (l : ι) => Polynomial.eval ((algebraMap R A) t) (p l)

Zero-derivative principle for multilinear maps along polynomial paths. If the Leibniz derivative φ.linearDeriv ((p l)(t)) ((p l)′(t)) = ∑ₖ φ((p 0)(t), …, (p k)′(t), …) of t ↦ φ((p l)(t)) vanishes at every scalar t, then φ((p l)(t)) takes the same value at all scalars.