Specializing polynomial identities modulo an analytic ideal

An equality of polynomials after reducing their germ coefficients modulo an ideal says that every coefficient difference belongs to that ideal. A finite fixed-degree family of chosen representatives therefore specializes to equal complex polynomials on the ideal's local zero set, on one common neighborhood.

noncomputable def LocalComplexGeometry.germPolynomialCoefficientRepresentatives {n m : ℕ} (p : Polynomial ↥(HolomorphicGerm n)) : Fin (m + 1) → ComplexEuclidean n → ℂ

Chosen representatives of all coefficients through a fixed degree bound.

Equations

• LocalComplexGeometry.germPolynomialCoefficientRepresentatives p i = LocalComplexGeometry.HolomorphicGerm.representative (p.coeff ↑i)

theorem LocalComplexGeometry.analyticAt_germPolynomialCoefficientRepresentatives {n m : ℕ} (p : Polynomial ↥(HolomorphicGerm n)) (i : Fin (m + 1)) : AnalyticAt ℂ (germPolynomialCoefficientRepresentatives p i) 0

noncomputable def LocalComplexGeometry.germPolynomialRepresentativeAt {n : ℕ} (m : ℕ) (p : Polynomial ↥(HolomorphicGerm n)) (z : ComplexEuclidean n) : Polynomial ℂ

The fixed-degree complex polynomial obtained by specializing the chosen coefficient representatives at a base point.

Equations

• LocalComplexGeometry.germPolynomialRepresentativeAt m p z = LocalComplexGeometry.fixedDegreePolynomialAt (LocalComplexGeometry.germPolynomialCoefficientRepresentatives p) z

noncomputable def LocalComplexGeometry.germPolynomialRepresentativeFunctions {n : ℕ} (m : ℕ) (p : Polynomial ↥(HolomorphicGerm n)) : Polynomial (ComplexEuclidean n → ℂ)

The same fixed-degree representative family, before specializing its coefficient functions at a base point.

Equations

• LocalComplexGeometry.germPolynomialRepresentativeFunctions m p = LocalComplexGeometry.fixedDegreePolynomial (LocalComplexGeometry.germPolynomialCoefficientRepresentatives p)

@[simp]

theorem LocalComplexGeometry.germPolynomialRepresentativeFunctions_map_eval {n : ℕ} (m : ℕ) (p : Polynomial ↥(HolomorphicGerm n)) (z : ComplexEuclidean n) : Polynomial.map (Pi.evalRingHom (fun (x : ComplexEuclidean n) => ℂ) z) (germPolynomialRepresentativeFunctions m p) = germPolynomialRepresentativeAt m p z

theorem LocalComplexGeometry.germPolynomialRepresentativeFunctions_map_germ {n m : ℕ} (p : Polynomial ↥(HolomorphicGerm n)) (hp : p.natDegree ≤ m) : Polynomial.map (functionToGermRingHom n) (germPolynomialRepresentativeFunctions m p) = Polynomial.map (holomorphicGermSubring n).subtype p

Through a valid degree bound, the polynomial of chosen representative functions maps back to the original polynomial of raw function germs.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_eq_of_degreeBounds {n k m : ℕ} (p : Polynomial ↥(HolomorphicGerm n)) (hk : p.natDegree ≤ k) (hm : p.natDegree ≤ m) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, germPolynomialRepresentativeAt k p z = germPolynomialRepresentativeAt m p z

Two valid fixed-degree displays of the same germ polynomial agree after shrinking once.

@[simp]

theorem LocalComplexGeometry.germPolynomialRepresentativeAt_zero_C {n : ℕ} (f : ↥(HolomorphicGerm n)) (z : ComplexEuclidean n) : germPolynomialRepresentativeAt 0 (Polynomial.C f) z = Polynomial.C (HolomorphicGerm.representative f z)

At bound zero, a constant germ polynomial specializes to the chosen representative of its constant coefficient.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_add {n m : ℕ} (p q : Polynomial ↥(HolomorphicGerm n)) (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ m) (hpq : (p + q).natDegree ≤ m) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, germPolynomialRepresentativeAt m (p + q) z = germPolynomialRepresentativeAt m p z + germPolynomialRepresentativeAt m q z

Chosen fixed-degree representatives respect polynomial addition after shrinking once, provided the displayed degree bound covers all three polynomials.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_mul {n m : ℕ} (p q : Polynomial ↥(HolomorphicGerm n)) (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ m) (hpq : (p * q).natDegree ≤ m) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, germPolynomialRepresentativeAt m (p * q) z = germPolynomialRepresentativeAt m p z * germPolynomialRepresentativeAt m q z

Chosen fixed-degree representatives respect polynomial multiplication after shrinking once, provided the displayed degree bound covers both factors and their product.

theorem LocalComplexGeometry.eventually_germPolynomialCoefficientRepresentatives_eq_of_map_quotient_eq {n m : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (p q : Polynomial ↥(HolomorphicGerm n)) (hmap : Polynomial.map (Ideal.Quotient.mk I) p = Polynomial.map (Ideal.Quotient.mk I) q) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, idealGeneratorZeroPredicate I z → ∀ (i : Fin (m + 1)), germPolynomialCoefficientRepresentatives p i z = germPolynomialCoefficientRepresentatives q i z

Quotient equality gives simultaneous equality of every represented coefficient through any prescribed finite degree bound.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_eq_of_map_quotient_eq {n m : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (p q : Polynomial ↥(HolomorphicGerm n)) (hmap : Polynomial.map (Ideal.Quotient.mk I) p = Polynomial.map (Ideal.Quotient.mk I) q) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, idealGeneratorZeroPredicate I z → germPolynomialRepresentativeAt m p z = germPolynomialRepresentativeAt m q z

A polynomial identity modulo I specializes to a complex-polynomial identity on V(I), uniformly on one neighborhood.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_eval_eq_of_map_quotient_eq {n m : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (p q : Polynomial ↥(HolomorphicGerm n)) (hmap : Polynomial.map (Ideal.Quotient.mk I) p = Polynomial.map (Ideal.Quotient.mk I) q) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, idealGeneratorZeroPredicate I z → ∀ (w : ℂ), Polynomial.eval w (germPolynomialRepresentativeAt m p z) = Polynomial.eval w (germPolynomialRepresentativeAt m q z)

Evaluation form of quotient-polynomial specialization.