Polynomial relations on germs of functions of several variables

Polynomials in the coordinates act on germs of functions f : (σ → R) → R along a filter l as polynomial functions: p : MvPolynomial σ R acts as the germ of y ↦ MvPolynomial.eval y p. This algebra structure (Filter.Germ.mvPolynomialAlgebra) is not an instance; activate it locally with attribute [local instance] Filter.Germ.mvPolynomialAlgebra.

With this structure, a polynomial P : (MvPolynomial σ R)[X] evaluated at the germ of f is the germ of y ↦ P (y, f y) (Filter.Germ.aeval_coe). Consequently the germ of f is algebraic over the coordinate polynomials exactly when f satisfies a nonzero polynomial relation P (y, f y) = 0 eventually along l (Filter.Germ.isAlgebraic_coe_iff). This turns closure properties of functions satisfying polynomial relations, such as Nash germs, into Mathlib's closure properties of algebraic elements.

Main declarations

• Filter.Germ.mvPolynomialAlgebra: coordinate polynomials acting on germs as polynomial functions.
• Filter.Germ.aeval_coe: evaluating a polynomial relation at the germ of a function.
• Filter.Germ.isAlgebraic_coe_iff: algebraic germs are germs of functions satisfying a nonzero polynomial relation.

@[instance_reducible]

noncomputable def Filter.Germ.mvPolynomialAlgebra {σ : Type u_1} {R : Type u_2} [CommSemiring R] (l : Filter (σ → R)) : Algebra (MvPolynomial σ R) (l.Germ R)

Polynomials in the coordinates act on germs along l of functions (σ → R) → R as polynomial functions: p acts as the germ of y ↦ MvPolynomial.eval y p.

theorem Filter.Germ.mvPolynomialAlgebra_algebraMap_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (l : Filter (σ → R)) (p : MvPolynomial σ R) : (algebraMap (MvPolynomial σ R) (l.Germ R)) p = ↑fun (y : σ → R) => (MvPolynomial.eval y) p

A coordinate polynomial acts on germs as the germ of its polynomial function.

theorem Filter.Germ.aeval_coe {σ : Type u_1} {R : Type u_2} [CommSemiring R] {l : Filter (σ → R)} (P : Polynomial (MvPolynomial σ R)) (f : (σ → R) → R) : (Polynomial.aeval ↑f) P = ↑fun (y : σ → R) => Polynomial.eval (f y) (Polynomial.map (MvPolynomial.eval y) P)

Evaluating P : (MvPolynomial σ R)[X] at the germ of f gives the germ of y ↦ P (y, f y), where P (y, t) is (P.map (MvPolynomial.eval y)).eval t.

theorem Filter.Germ.isAlgebraic_coe_iff {σ : Type u_1} {R : Type u_2} [CommRing R] {l : Filter (σ → R)} {f : (σ → R) → R} : IsAlgebraic (MvPolynomial σ R) ↑f ↔ ∃ (P : Polynomial (MvPolynomial σ R)), P ≠ 0 ∧ ∀ᶠ (y : σ → R) in l, Polynomial.eval (f y) (Polynomial.map (MvPolynomial.eval y) P) = 0

The germ of f is algebraic over the coordinate polynomials exactly when f satisfies a nonzero polynomial relation P (y, f y) = 0 eventually along l.