The prepared-prime geometric step

This file joins the generic-fibre algebra to the local geometry of finite prepared fibres. The small certificate below deliberately records only the finite pointwise information used by the geometric argument. Its fields are later furnished by denominator-cleared minimal-polynomial identities.

theorem LocalComplexGeometry.eventually_representative_finsetProd {n : ℕ} {ι : Type u_1} (S : Finset ι) (f : ι → ↥(HolomorphicGerm n)) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, HolomorphicGerm.representative (∏ i ∈ S, f i) z = ∏ i ∈ S, HolomorphicGerm.representative (f i) z

Chosen representatives respect a finite product after one common shrinking.

theorem LocalComplexGeometry.eventually_representative_mul {n : ℕ} (f g : ↥(HolomorphicGerm n)) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, HolomorphicGerm.representative (f * g) z = HolomorphicGerm.representative f z * HolomorphicGerm.representative g z

Binary form of representative multiplication.

structure LocalComplexGeometry.PreparedPrimeFiberCertificate {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (P : Ideal ↥(HolomorphicGerm (n + 1))) (g : ↥(HolomorphicGerm (n + 1))) : Type

Finite pointwise data extracted from the denominator-cleared generic minimal polynomial for one target germ. The final field is the purely algebraic return path: once all coefficients of the small remainder lie in the contraction, generic divisibility puts the target back in the ambient prime.

• e : ℕ

  The positive degree of the generic minimal polynomial.

• positiveDegree : 0 < self.e
• q : Fin (self.e + 1) → ↥(HolomorphicGerm n)

  Coefficients of the specialized minimal polynomial.

• b : Fin self.e → ↥(HolomorphicGerm n)

  Coefficients of the specialized strict remainder.

• bad : ↥(HolomorphicGerm n)

  A base germ whose nonvanishing controls specialization.

• bad_not_mem : self.bad ∉ lowerDimensionalContraction P
• eventually_specializes : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, (∀ (f : ↥(idealGeneratorFinset (lowerDimensionalContraction P))), HolomorphicGerm.representative (↑f) z = 0) → HolomorphicGerm.representative self.bad z ≠ 0 → let Qz := fixedDegreePolynomialAt (HolomorphicGerm.coefficientRepresentatives self.q) z; Qz.natDegree = self.e ∧ Qz.Separable ∧ ∀ (w : ℂ), Polynomial.eval w Qz = 0 → preparedValue a z w = 0 ∧ (∀ (f : ↥(idealGeneratorFinset P)), HolomorphicGerm.representative (↑f) ((appendLastCLE n) (z, w)) = 0) ∧ (HolomorphicGerm.representative g ((appendLastCLE n) (z, w)) = 0 → Polynomial.eval w (remainderPolynomialAt (HolomorphicGerm.coefficientRepresentatives self.b) z) = 0)
• mem_of_coeff_mem : (∀ (i : Fin self.e), self.b i ∈ lowerDimensionalContraction P) → g ∈ P

theorem LocalComplexGeometry.mem_prime_of_preparedPrimeFiberCertificate {n d : ℕ} (hprime : PrimeZeroSetProperty n) (hd : 0 < d) (a : Fin d → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (P : Ideal ↥(HolomorphicGerm (n + 1))) (hP : P.IsPrime) (g : ↥(HolomorphicGerm (n + 1))) (hg : g ∈ vanishingIdeal (idealZeroSetGerm P)) (C : PreparedPrimeFiberCertificate a P g) : g ∈ P

The geometric heart of the prepared-prime argument. A finite-fibre certificate turns vanishing on the ambient prime zero set into membership in the prime, using the lower-dimensional prime theorem and cancellation of one common bad factor.