Geometric finite projection of a prepared hypersurface

This module packages the genuine local finite-map conclusion of Weierstrass preparation. The source is the actual zero locus in an open vertical tube, and properness is asserted over the open base neighborhood itself.

Coordinate and zero-locus definitions

noncomputable def LocalComplexGeometry.dropLastCLM (n : ℕ) : ComplexEuclidean (n + 1) →L[ℂ] ComplexEuclidean n

Projection to the first n standard complex coordinates.

Equations

• LocalComplexGeometry.dropLastCLM n = LocalComplexGeometry.baseProjectionCLM n

noncomputable def LocalComplexGeometry.appendLastCLE (n : ℕ) : (ComplexEuclidean n × ℂ) ≃L[ℂ] ComplexEuclidean (n + 1)

Append a distinguished last coordinate.

Equations

• LocalComplexGeometry.appendLastCLE n = (LocalComplexGeometry.wptAmbientEquiv n).symm

@[simp]

theorem LocalComplexGeometry.dropLastCLM_appendLastCLE (n : ℕ) (z : ComplexEuclidean n) (w : ℂ) : (dropLastCLM n) ((appendLastCLE n) (z, w)) = z

theorem LocalComplexGeometry.lastCoordinateCLM_appendLastCLE (n : ℕ) (z : ComplexEuclidean n) (w : ℂ) : (lastCoordinateCLM n) ((appendLastCLE n) (z, w)) = w

theorem LocalComplexGeometry.appendLastCLE_dropLast_lastCoordinate (n : ℕ) (x : ComplexEuclidean (n + 1)) : (appendLastCLE n) ((dropLastCLM n) x, (lastCoordinateCLM n) x) = x

theorem LocalComplexGeometry.wptAmbientEquiv_eq_dropLast_lastCoordinate (n : ℕ) (x : ComplexEuclidean (n + 1)) : (wptAmbientEquiv n) x = ((dropLastCLM n) x, (lastCoordinateCLM n) x)

def LocalComplexGeometry.preparedValue {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) (w : ℂ) : ℂ

Evaluation of a monic prepared polynomial in its base and last variables.

Equations

• LocalComplexGeometry.preparedValue a z w = w ^ d + ∑ i : Fin d, a i z * w ^ ↑i

@[simp]

theorem LocalComplexGeometry.preparedValue_eq_preparedPolynomial {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) (w : ℂ) : preparedValue a z w = ClassicalComplexWPT.preparedPolynomial d a (z, w)

@[reducible, inline]

abbrev LocalComplexGeometry.LocalHypersurface {n : ℕ} (F : ComplexEuclidean (n + 1) → ℂ) (U : Set (ComplexEuclidean n)) (R : ℝ) : Type

The zero locus of F in the open vertical tube U × {‖w‖ < R}.

Equations

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

noncomputable def LocalComplexGeometry.localProjection {n : ℕ} (F : ComplexEuclidean (n + 1) → ℂ) (U : Set (ComplexEuclidean n)) (R : ℝ) : LocalHypersurface F U R → ↑U

Projection of the local hypersurface to its open base.

Equations

• LocalComplexGeometry.localProjection F U R x = ⟨(LocalComplexGeometry.dropLastCLM n) ↑x, ⋯⟩

theorem LocalComplexGeometry.continuous_localProjection {n : ℕ} (F : ComplexEuclidean (n + 1) → ℂ) (U : Set (ComplexEuclidean n)) (R : ℝ) : Continuous (localProjection F U R)

Audited geometric finite-projection predicate

def LocalComplexGeometry.HasGeometricFiniteProjection {n : ℕ} (F : ComplexEuclidean (n + 1) → ℂ) (d : ℕ) : Prop

An explicit local finite projection, including analytic preparation on a tube, vertical boundary control, finite fibers, surjectivity, and genuine properness over the open base U.

Equations

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

The polynomial associated to one vertical fiber

noncomputable def LocalComplexGeometry.preparedPolynomialAt {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : Polynomial ℂ

The prepared value at z, regarded as a polynomial in the last variable.

Equations

• LocalComplexGeometry.preparedPolynomialAt a z = Polynomial.X ^ d + ∑ i : Fin d, Polynomial.C (a i z) * Polynomial.X ^ ↑i

@[simp]

theorem LocalComplexGeometry.preparedPolynomialAt_eval {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) (w : ℂ) : Polynomial.eval w (preparedPolynomialAt a z) = preparedValue a z w

theorem LocalComplexGeometry.preparedPolynomialAt_monic {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : (preparedPolynomialAt a z).Monic

@[simp]

theorem LocalComplexGeometry.preparedPolynomialAt_natDegree {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : (preparedPolynomialAt a z).natDegree = d

theorem LocalComplexGeometry.preparedValue_zero_set_finite {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : {w : ℂ | preparedValue a z w = 0}.Finite

theorem LocalComplexGeometry.preparedValue_zero_set_ncard_le {n d : ℕ} (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : {w : ℂ | preparedValue a z w = 0}.ncard ≤ d

theorem LocalComplexGeometry.preparedValue_exists_zero {n d : ℕ} (hd : 0 < d) (a : Fin d → ComplexEuclidean n → ℂ) (z : ComplexEuclidean n) : ∃ (w : ℂ), preparedValue a z w = 0

theorem LocalComplexGeometry.norm_lt_of_monic_sum_eq_zero_of_coeff_bound {d : ℕ} (hd : 0 < d) {r : ℝ} (hr : 0 < r) (b : Fin d → ℂ) (w : ℂ) (hb : ∀ (i : Fin d), ‖b i‖ < r ^ (d - ↑i) / (2 * ↑d)) (hzero : w ^ d + ∑ i : Fin d, b i * w ^ ↑i = 0) : ‖w‖ < r

A quantitative root bound for a monic polynomial with sufficiently small lower coefficients.

A compact-preimage criterion for the local projection

theorem LocalComplexGeometry.isProperMap_localProjection_of_inner_bound {n : ℕ} {F : ComplexEuclidean (n + 1) → ℂ} {U : Set (ComplexEuclidean n)} {r R : ℝ} (_hr : 0 ≤ r) (hrR : r < R) (hF : ContinuousOn F {x : ComplexEuclidean (n + 1) | (dropLastCLM n) x ∈ U ∧ ‖(lastCoordinateCLM n) x‖ < R}) (hbound : ∀ (x : ComplexEuclidean (n + 1)), (dropLastCLM n) x ∈ U → ‖(lastCoordinateCLM n) x‖ < R → F x = 0 → ‖(lastCoordinateCLM n) x‖ ≤ r) : IsProperMap (localProjection F U R)

If all zeros in the radius-R tube actually lie in a fixed smaller closed disc, then projection of the zero locus to the open base is proper.

From an open preparation witness to finite projection

theorem LocalComplexGeometry.hasGeometricFiniteProjection_of_open_preparation {n d : ℕ} (hd : 0 < d) {f : ClassicalComplexWPT.Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (u : ClassicalComplexWPT.Ambient n → ℂ) (s : Set (ClassicalComplexWPT.Ambient n)) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hu : AnalyticAt ℂ u 0) (hs : IsOpen s) (hs0 : 0 ∈ s) (hunit : ∀ x ∈ s, u x ≠ 0) (hfactor : ∀ x ∈ s, f x = u x * ClassicalComplexWPT.preparedPolynomial d a x) : HasGeometricFiniteProjection (fun (x : ComplexEuclidean (n + 1)) => f ((wptAmbientEquiv n) x)) d

A positive-degree preparation on an open neighborhood yields the full audited geometric finite-projection predicate after shrinking to a product tube.

theorem LocalComplexGeometry.hasGeometricFiniteProjection_of_exactOrder {n d : ℕ} (hd : 0 < d) {f : ClassicalComplexWPT.Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) (horder : ClassicalComplexWPT.ExactOrderInLastVariable f d) : HasGeometricFiniteProjection (fun (x : ComplexEuclidean (n + 1)) => f ((wptAmbientEquiv n) x)) d

Positive exact order, through the pinned WPT theorem, gives a genuine geometric finite projection in the standard coordinate model.