Construction of the prepared-prime certificate

This file constructs the finite pointwise certificate from generic-fibre data and closes the prepared-prime induction step.

noncomputable def LocalComplexGeometry.preparedPrimeFiberCertificateOfGenericMinpoly {n d : ℕ} (hd : 0 < d) (a : Fin d → ClassicalComplexWPT.Base 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) (hmem : WPTBridge.preparedPolynomialGerm a ha ∈ P) (g : ↥(HolomorphicGerm (n + 1))) : PreparedPrimeFiberCertificate a P g

Construct the prepared-prime fiber certificate from the generic minimal polynomial.

Equations

• One or more equations did not get rendered due to their size.

theorem LocalComplexGeometry.preparedPrimeZeroSetStep_of_primeZeroSetProperty {n : ℕ} (hprime : PrimeZeroSetProperty n) : PreparedPrimeZeroSetStep n

The lower-dimensional prime theorem supplies the geometric cancellation step needed to close the prepared successor case.

theorem LocalComplexGeometry.primeZeroSetProperty_all (n : ℕ) : PrimeZeroSetProperty n

The prepared-prime construction closes the prime zero-set theorem in every dimension by induction.