Smooth affine complete intersections

Let p : ι → MvPolynomial σ 𝕜 be a finite family of polynomials over a complete nontrivially normed field, and let TauCeti.affineZeroLocus p ⊆ 𝕜^σ be its common zero set. Suppose the Jacobian matrix (∂pᵢ/∂xⱼ) of the family is surjective at every common zero, so that the zero set is a smooth complete intersection. Then the zero set is a closed analytic submanifold of 𝕜^σ of dimension |σ| - |ι|:

• TauCeti.affineZeroLocusChartedSpace and TauCeti.isManifold_affineZeroLocus: the zero set, with its subspace topology, is a C^r manifold modelled on Fin (|σ| - |ι|) → 𝕜 for every r : ℕ∞ω, with the implicit-function charts of the evaluation map;
• TauCeti.contMDiff_coe_affineZeroLocus, TauCeti.injective_mfderiv_coe_affineZeroLocus and TauCeti.range_mfderiv_coe_affineZeroLocus: its inclusion into 𝕜^σ is analytic and an immersion, with tangent space at x the kernel of the Jacobian matrix at x.

The zero set is closed (TauCeti.isClosed_affineZeroLocus). The surjectivity hypothesis forces the zero set to have codimension |ι|, so a smooth affine variety is covered only through a defining family with as many equations as its codimension; a family with more equations than the codimension never satisfies it.

Over ℂ this is the input to Milnor's theorem that a smooth affine algebraic variety of complex dimension n has the homotopy type of a CW complex of dimension at most n, for smooth complete intersections. The Euclidean squared distance x ↦ ‖x - a‖² from any point a restricts to a proper function on the zero set (TauCeti.isProperMap_norm_sq_sub_toLp_affineZeroLocus), and every critical point of this restriction has real Morse index at most the complex dimension |σ| - |ι| (TauCeti.manifoldMorseIndex_norm_sq_sub_toLp_affineZeroLocus_le). The latter is the Levi-form bound TauCeti.manifoldMorseIndex_norm_sq_sub_comp_le for a holomorphic immersion, applied to the inclusion of the zero set into Euclidean space ℂ^σ, which is holomorphic and an immersion (TauCeti.contMDiff_toLp_coe_affineZeroLocus and TauCeti.injective_mvfderiv_toLp_coe_affineZeroLocus).

References

• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Section 7, Theorem 7.2.
• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Corollary 5.14, for regular level sets.

theorem TauCeti.isProperMap_norm_sq_sub_toLp_affineZeroLocus {𝕜 : Type u_1} {σ : Type u_2} {ι : Type u_3} [RCLike 𝕜] [Fintype σ] (p : ι → MvPolynomial σ 𝕜) (a : EuclideanSpace 𝕜 σ) : IsProperMap fun (x : ↑(affineZeroLocus p)) => ‖WithLp.toLp 2 ↑x - a‖ ^ 2

Squared distance is proper on an affine algebraic set. For every point a of Euclidean space 𝕜^σ, the Euclidean squared distance from a, restricted to the common zero set of a family of polynomials, is a proper map.

@[instance_reducible]

noncomputable def TauCeti.affineZeroLocusChartedSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {σ : Type u_2} {ι : Type u_3} [Fintype σ] {p : ι → MvPolynomial σ 𝕜} [Fintype ι] [CompleteSpace 𝕜] (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) : ChartedSpace (Fin (Fintype.card σ - Fintype.card ι) → 𝕜) ↑(affineZeroLocus p)

The charts of a smooth affine complete intersection. If the Jacobian matrix of a polynomial family is surjective at every common zero, the zero set is a charted space modelled on Fin (|σ| - |ι|) → 𝕜, the charts being the implicit-function charts TauCeti.levelSetChartAt of the evaluation map.

theorem TauCeti.isManifold_affineZeroLocus {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {σ : Type u_2} {ι : Type u_3} [Fintype σ] {p : ι → MvPolynomial σ 𝕜} [Fintype ι] [CompleteSpace 𝕜] (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) (r : WithTop ℕ∞) : IsManifold (modelWithCornersSelf 𝕜 (Fin (Fintype.card σ - Fintype.card ι) → 𝕜)) r ↑(affineZeroLocus p)

A smooth affine complete intersection is an analytic manifold. If the Jacobian matrix of a polynomial family is surjective at every common zero, the zero set is a C^r manifold of dimension |σ| - |ι| for every r, including r = ω.

theorem TauCeti.contMDiff_coe_affineZeroLocus {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {σ : Type u_2} {ι : Type u_3} [Fintype σ] {p : ι → MvPolynomial σ 𝕜} [Fintype ι] [CompleteSpace 𝕜] (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) (r : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf 𝕜 (Fin (Fintype.card σ - Fintype.card ι) → 𝕜)) (modelWithCornersSelf 𝕜 (σ → 𝕜)) r Subtype.val

The inclusion of a smooth affine complete intersection into 𝕜^σ is C^r for every r, including r = ω.

theorem TauCeti.injective_mfderiv_coe_affineZeroLocus {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {σ : Type u_2} {ι : Type u_3} [Fintype σ] {p : ι → MvPolynomial σ 𝕜} [Fintype ι] [CompleteSpace 𝕜] (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) (x : ↑(affineZeroLocus p)) : Function.Injective ⇑(mfderiv% Subtype.val x)

The inclusion of a smooth affine complete intersection into 𝕜^σ is an immersion.

theorem TauCeti.range_mfderiv_coe_affineZeroLocus {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {σ : Type u_2} {ι : Type u_3} [Fintype σ] {p : ι → MvPolynomial σ 𝕜} [Fintype ι] [CompleteSpace 𝕜] (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) (x : ↑(affineZeroLocus p)) : (↑(mfderiv% Subtype.val x)).range = (jacobiMatrixAt p ↑x).mulVecLin.ker

The tangent space of a smooth affine complete intersection. At a point x of the zero set, the range of the differential of the inclusion is the kernel of the Jacobian matrix at x.

theorem TauCeti.contMDiff_toLp_coe_affineZeroLocus {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Fintype ι] {p : ι → MvPolynomial σ ℂ} (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) (r : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ (Fin (Fintype.card σ - Fintype.card ι) → ℂ)) (modelWithCornersSelf ℂ (EuclideanSpace ℂ σ)) r fun (y : ↑(affineZeroLocus p)) => WithLp.toLp 2 ↑y

The inclusion of a smooth affine complete intersection into Euclidean space ℂ^σ is holomorphic of every order.

theorem TauCeti.injective_mvfderiv_toLp_coe_affineZeroLocus {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Fintype ι] {p : ι → MvPolynomial σ ℂ} (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) (x : ↑(affineZeroLocus p)) : Function.Injective ⇑((d% fun (y : ↑(affineZeroLocus p)) => WithLp.toLp 2 ↑y) x)

The inclusion of a smooth affine complete intersection into Euclidean space ℂ^σ is an immersion.

theorem TauCeti.manifoldMorseIndex_norm_sq_sub_toLp_affineZeroLocus_le {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Fintype ι] {p : ι → MvPolynomial σ ℂ} (hp : ∀ x ∈ affineZeroLocus p, Function.Surjective (jacobiMatrixAt p x).mulVec) (a : EuclideanSpace ℂ σ) (x : ↑(affineZeroLocus p)) (hcrit : (d% fun (y : ↑(affineZeroLocus p)) => ‖WithLp.toLp 2 ↑y - a‖ ^ 2) x = 0) : manifoldMorseIndex (modelWithCornersSelf ℝ (Fin (Fintype.card σ - Fintype.card ι) → ℂ)) (fun (y : ↑(affineZeroLocus p)) => ‖WithLp.toLp 2 ↑y - a‖ ^ 2) x ≤ Fintype.card σ - Fintype.card ι

Milnor's index bound on a smooth affine complete intersection. On the common zero set in ℂ^σ of a polynomial family with surjective Jacobian at every common zero, every critical point of the Euclidean squared distance from a point a has real Morse index at most the complex dimension |σ| - |ι| of the zero set.