The prepared divisor is associate to the regularized germ

noncomputable def LocalComplexGeometry.WPTBridge.standardPreparationUnitGerm {n : ℕ} (u : ClassicalComplexWPT.Ambient n → ℂ) (hu : AnalyticAt ℂ u 0) : ↥(HolomorphicGerm (n + 1))

Transport an analytic WPT unit from product coordinates to standard coordinates.

Equations

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

theorem LocalComplexGeometry.WPTBridge.standardPreparationUnitGerm_isUnit {n : ℕ} (u : ClassicalComplexWPT.Ambient n → ℂ) (hu : AnalyticAt ℂ u 0) (hu0 : u 0 ≠ 0) : IsUnit (standardPreparationUnitGerm u hu)

theorem LocalComplexGeometry.WPTBridge.coordinatePullback_eq_unit_mul_preparedPolynomialGerm {n d : ℕ} {f : ↥(HolomorphicGerm (n + 1))} (L : ComplexEuclidean (n + 1) ≃L[ℂ] ComplexEuclidean (n + 1)) (H : ClassicalComplexWPT.Ambient n → ℂ) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (u : ClassicalComplexWPT.Ambient n → ℂ) (hcoord : (↑fun (x : ComplexEuclidean (n + 1)) => H ((wptAmbientEquiv n) x)) = ↑((coordinatePullback L) f)) (hprep : ClassicalComplexWPT.IsWeierstrassPreparation H d a u) : (coordinatePullback L) f = standardPreparationUnitGerm u ⋯ * preparedPolynomialGerm a ⋯

The raw representative identity supplied by regularized preparation descends to an equality saying that the coordinate pullback is a unit times the prepared polynomial germ.

theorem LocalComplexGeometry.WPTBridge.coordinatePullback_associated_preparedPolynomialGerm {n d : ℕ} {f : ↥(HolomorphicGerm (n + 1))} (L : ComplexEuclidean (n + 1) ≃L[ℂ] ComplexEuclidean (n + 1)) (H : ClassicalComplexWPT.Ambient n → ℂ) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (u : ClassicalComplexWPT.Ambient n → ℂ) (hcoord : (↑fun (x : ComplexEuclidean (n + 1)) => H ((wptAmbientEquiv n) x)) = ↑((coordinatePullback L) f)) (hprep : ClassicalComplexWPT.IsWeierstrassPreparation H d a u) : Associated ((coordinatePullback L) f) (preparedPolynomialGerm a ⋯)

The prepared divisor is an associate of the coordinate pullback.