Specializing polynomial identities of function germs

A polynomial identity between germs has only finitely many nonzero coefficients. Consequently representatives of its coefficients satisfy the corresponding pointwise complex-polynomial identity on one common neighborhood. This is the finite-uniformity step needed when cleared generic fiber identities are specialized over the analytic base.

noncomputable def LocalComplexGeometry.functionToGermRingHom (n : ℕ) : (ComplexEuclidean n → ℂ) →+* FunctionGerm n

The ring homomorphism sending a function to its germ at the origin.

Equations

• LocalComplexGeometry.functionToGermRingHom n = Filter.Germ.coeRingHom (nhds 0)

theorem LocalComplexGeometry.eventually_polynomial_map_eval_eq_of_map_germ_eq {n : ℕ} (p q : Polynomial (ComplexEuclidean n → ℂ)) (hmap : Polynomial.map (functionToGermRingHom n) p = Polynomial.map (functionToGermRingHom n) q) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, Polynomial.map (Pi.evalRingHom (fun (x : ComplexEuclidean n) => ℂ) z) p = Polynomial.map (Pi.evalRingHom (fun (x : ComplexEuclidean n) => ℂ) z) q

A polynomial identity after passing from coefficient functions to their germs holds pointwise after specializing the coefficient functions on a single neighborhood of the origin.

theorem LocalComplexGeometry.eventually_polynomial_eval_eq_of_map_germ_eq {n : ℕ} (p q : Polynomial (ComplexEuclidean n → ℂ)) (hmap : Polynomial.map (functionToGermRingHom n) p = Polynomial.map (functionToGermRingHom n) q) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, ∀ (w : ℂ), Polynomial.eval w (Polynomial.map (Pi.evalRingHom (fun (x : ComplexEuclidean n) => ℂ) z) p) = Polynomial.eval w (Polynomial.map (Pi.evalRingHom (fun (x : ComplexEuclidean n) => ℂ) z) q)

Eventual equality of coefficient functions gives eventual equality of their fixed polynomial evaluations at every last-coordinate value.