The Jacobian criterion on four hypersurfaces

The Jacobian criterion for the simple points of a local model, isRegularLocalRing_stalk_iff_jacobian (Hironaka.AnalyticSpace.Jacobian), read on four hypersurfaces: the node y² = x² + x³ and the cusp y² = x³ in K² (simple exactly off the origin), the Whitney umbrella x² = z y² in ℝ³ (the multiple points are exactly the z-axis, the handle z < 0 included: there the real points form a line, but the stalk is not regular), and V(x² + y²) ⊆ ℝ², which has no simple point: the standard example of the phenomenon Hironaka remarks on [Hir64, Introduction], a reduced real-analytic space whose simple locus is not dense. (Its support is the origin, since x² + y² = 0 forces x = y = 0 over ℝ, and it is reduced; neither is recorded as a statement in this file — RealPlaneCircle proves the support statement for the ideal sheaf circleIdeal.) "Simple point" is regularLocus's clause, IsRegularLocalRing 𝒪_{X,z}, stated on the local model V(g) ⊆ (Kⁿ, 𝒜_{Kⁿ}).

For a hypersurface X = V(g) the criterion reads: z ∈ X is simple iff dg_z ≠ 0. If dg_z ≠ 0 then g_z is a regular parameter and 𝒜/(g_z) is regular (isRegularLocalRing_stalk_of_dlin_ne_zero). If dg_z = 0, i.e. g_z ∈ 𝔪_z², the only subfamily of the one generator with independent differentials is the empty one, which would force dim 𝒜/(g_z) = n = dim 𝒜, i.e. g_z = 0 in the domain 𝒜_{Kⁿ,z} (eq_bot_of_ringKrullDim_quotient_eq) — excluded because g does not vanish identically near z (germTop_ne_zero_of_curve: the germ of a section is zero iff the section vanishes near the point, the identity lemma). The differential of a polynomial in the coordinates is computed by expanding around the point: g_z = ∑ aᵢ (zᵢ − qᵢ) + r with r ∈ 𝔪_z² gives dg_z = a (dlin_eq_of_sub_sum_mem_sq; dlin is K-linear, kills 𝔪² and sends zᵢ − qᵢ to eᵢ).

The equation circleEq of the last example is used again in HironakaExamples.Space.CircleSpace (the analytic space V(x² + y²)).

noncomputable def Hironaka.Space.germTop {K : Type} [RCLike K] {n : ℕ} (g : AnalyticSpace.AnalyticFun K n ⊤) (q : AnalyticSpace.Kn K n) : ↑((Manifold.structureSheaf K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n)).presheaf.stalk q)

The germ at q of a global analytic function on Kⁿ (a def, so that the expansion lemmas below rewrite it as a single term).

Equations

• Hironaka.Space.germTop g q = (CategoryTheory.ConcreteCategory.hom ((AnalyticSpace.affine K n).presheaf.germ ⊤ q ⋯)) g

theorem Hironaka.Space.germTop_coordSection {K : Type} [RCLike K] {n : ℕ} (q : AnalyticSpace.Kn K n) (i : Fin n) : germTop (AnalyticSpace.coordSection K n i) q = AnalyticSpace.coordAt K n q i

theorem Hironaka.Space.germTop_mul {K : Type} [RCLike K] {n : ℕ} (a b : AnalyticSpace.AnalyticFun K n ⊤) (q : AnalyticSpace.Kn K n) : germTop (a * b) q = germTop a q * germTop b q

theorem Hironaka.Space.germTop_sub {K : Type} [RCLike K] {n : ℕ} (a b : AnalyticSpace.AnalyticFun K n ⊤) (q : AnalyticSpace.Kn K n) : germTop (a - b) q = germTop a q - germTop b q

theorem Hironaka.Space.germTop_add {K : Type} [RCLike K] {n : ℕ} (a b : AnalyticSpace.AnalyticFun K n ⊤) (q : AnalyticSpace.Kn K n) : germTop (a + b) q = germTop a q + germTop b q

theorem Hironaka.Space.germTop_ne_zero_of_curve {K : Type} [RCLike K] {n : ℕ} (g : AnalyticSpace.AnalyticFun K n ⊤) (q : AnalyticSpace.Kn K n) (γ : K → AnalyticSpace.Kn K n) (hγ : Continuous γ) (hγ0 : γ 0 = q) (h : ∀ᶠ (t : K) in nhdsWithin 0 {0}ᶜ, g.eval ⟨γ t, ⋯⟩ ≠ 0) : germTop g q ≠ 0

A global section whose values along a continuous curve through q are nonzero off q has nonzero germ at q (the identity lemma germ_eq_zero_iff).

theorem Hironaka.Space.coordAt_sub_const_mem_maximalIdeal {K : Type} [RCLike K] {n : ℕ} (q : AnalyticSpace.Kn K n) (i : Fin n) : AnalyticSpace.coordAt K n q i - (Manifold.const K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n) q) (q.down i) ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n)).presheaf.stalk q)

The coordinate germ zᵢ − qᵢ lies in 𝔪_q.

theorem Hironaka.Space.dlin_eq_of_sub_sum_mem_sq {K : Type} [RCLike K] {n : ℕ} (q : AnalyticSpace.Kn K n) (s : ↑((Manifold.structureSheaf K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n)).presheaf.stalk q)) (a : Fin n → K) (hr : s - ∑ i : Fin n, (Manifold.const K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n) q) (a i) * (AnalyticSpace.coordAt K n q i - (Manifold.const K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n) q) (q.down i)) ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n)).presheaf.stalk q) ^ 2) : (AnalyticSpace.dlin K n q) s = a

dlin of an explicit expansion: if s − ∑ i, aᵢ (zᵢ − qᵢ) ∈ 𝔪_q², then d_q s = a.

theorem Hironaka.Space.not_isRegularLocalRing_stalk_of_germ_mem_sq_of_ne_zero {K : Type} [RCLike K] {n : ℕ} (f : Fin 1 → AnalyticSpace.AnalyticFun K n ⊤) (z : ↑↑(AnalyticSpace.localModel K n ⊤ f).toPresheafedSpace) (hsq : germTop (f 0) ↑↑z ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf K (AnalyticSpace.Kn K n) (AnalyticSpace.Kn K n)).presheaf.stalk ↑↑z) ^ 2) (hne : germTop (f 0) ↑↑z ≠ 0) : ¬IsRegularLocalRing ↑((AnalyticSpace.localModel K n ⊤ f).presheaf.stalk z)

The criterion for one equation, negative half: at a point z of V(g) where g_z ∈ 𝔪_z² and g_z ≠ 0 the stalk 𝒜_{Kⁿ,z}/(g_z) is not regular.

theorem Hironaka.Space.isRegularLocalRing_stalk_of_dlin_ne_zero {K : Type} [RCLike K] {n : ℕ} (f : Fin 1 → AnalyticSpace.AnalyticFun K n ⊤) (z : ↑↑(AnalyticSpace.localModel K n ⊤ f).toPresheafedSpace) (hd : (AnalyticSpace.dlin K n ↑↑z) (germTop (f 0) ↑↑z) ≠ 0) : IsRegularLocalRing ↑((AnalyticSpace.localModel K n ⊤ f).presheaf.stalk z)

The criterion for one equation, positive half: at a point z of V(g) where dg_z ≠ 0 the stalk is regular (g_z is a regular parameter).

noncomputable def Hironaka.Space.nodeEq (K : Type) [RCLike K] : Fin 1 → AnalyticSpace.AnalyticFun K 2 ⊤

The node y² = x² + x³ in K²: the one equation y·y − x·x − x·x·x.

Equations

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

theorem Hironaka.Space.nodeEq_germ {K : Type} [RCLike K] (q : AnalyticSpace.Kn K 2) : germTop (nodeEq K 0) q = AnalyticSpace.coordAt K 2 q 1 * AnalyticSpace.coordAt K 2 q 1 - AnalyticSpace.coordAt K 2 q 0 * AnalyticSpace.coordAt K 2 q 0 - AnalyticSpace.coordAt K 2 q 0 * AnalyticSpace.coordAt K 2 q 0 * AnalyticSpace.coordAt K 2 q 0

theorem Hironaka.Space.node_isRegularLocalRing_stalk_iff {K : Type} [RCLike K] (z : ↑↑(AnalyticSpace.localModel K 2 ⊤ (nodeEq K)).toPresheafedSpace) : IsRegularLocalRing ↑((AnalyticSpace.localModel K 2 ⊤ (nodeEq K)).presheaf.stalk z) ↔ ↑↑z ≠ { down := 0 }

The node y² = x² + x³ is simple exactly off the origin — at the origin the differential (−2x − 3x², 2y) vanishes and the equation lies in 𝔪²; at every other point of the curve it does not vanish (y ≠ 0, or y = 0 and then x = −1).

noncomputable def Hironaka.Space.cuspEq (K : Type) [RCLike K] : Fin 1 → AnalyticSpace.AnalyticFun K 2 ⊤

The cusp y² = x³ in K²: the one equation y·y − x·x·x.

Equations

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

theorem Hironaka.Space.cuspEq_germ {K : Type} [RCLike K] (q : AnalyticSpace.Kn K 2) : germTop (cuspEq K 0) q = AnalyticSpace.coordAt K 2 q 1 * AnalyticSpace.coordAt K 2 q 1 - AnalyticSpace.coordAt K 2 q 0 * AnalyticSpace.coordAt K 2 q 0 * AnalyticSpace.coordAt K 2 q 0

theorem Hironaka.Space.cusp_isRegularLocalRing_stalk_iff {K : Type} [RCLike K] (z : ↑↑(AnalyticSpace.localModel K 2 ⊤ (cuspEq K)).toPresheafedSpace) : IsRegularLocalRing ↑((AnalyticSpace.localModel K 2 ⊤ (cuspEq K)).presheaf.stalk z) ↔ ↑↑z ≠ { down := 0 }

The cusp y² = x³ is simple exactly off the origin — the differential (−3x², 2y) vanishes on the curve only at the origin, where the equation lies in 𝔪².

noncomputable def Hironaka.Space.umbrellaEq : Fin 1 → AnalyticSpace.AnalyticFun ℝ 3 ⊤

The Whitney umbrella x² = z y² in ℝ³: the one equation x·x − z·(y·y).

Equations

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

theorem Hironaka.Space.umbrellaEq_germ (q : AnalyticSpace.Kn ℝ 3) : germTop (umbrellaEq 0) q = AnalyticSpace.coordAt ℝ 3 q 0 * AnalyticSpace.coordAt ℝ 3 q 0 - AnalyticSpace.coordAt ℝ 3 q 2 * (AnalyticSpace.coordAt ℝ 3 q 1 * AnalyticSpace.coordAt ℝ 3 q 1)

theorem Hironaka.Space.umbrella_not_isRegularLocalRing_of_axis (z : ↑↑(AnalyticSpace.localModel ℝ 3 ⊤ umbrellaEq).toPresheafedSpace) (hx0 : (↑↑z).down 0 = 0) (hy0 : (↑↑z).down 1 = 0) : ¬IsRegularLocalRing ↑((AnalyticSpace.localModel ℝ 3 ⊤ umbrellaEq).presheaf.stalk z)

On the z-axis the umbrella's stalk is not regular: the equation lies in 𝔪² there and does not vanish identically (x² ≠ 0 along the x-direction).

theorem Hironaka.Space.umbrella_isRegularLocalRing_stalk_iff (z : ↑↑(AnalyticSpace.localModel ℝ 3 ⊤ umbrellaEq).toPresheafedSpace) : IsRegularLocalRing ↑((AnalyticSpace.localModel ℝ 3 ⊤ umbrellaEq).presheaf.stalk z) ↔ ¬((↑↑z).down 0 = 0 ∧ (↑↑z).down 1 = 0)

The multiple points of the Whitney umbrella x² = z y² are exactly the z-axis: off the axis (y ≠ 0 on the surface) the differential (2x, −2zy, −y²) does not vanish.

theorem Hironaka.Space.umbrella_not_isRegularLocalRing_stalk_of_neg (z : ↑↑(AnalyticSpace.localModel ℝ 3 ⊤ umbrellaEq).toPresheafedSpace) (hneg : (↑↑z).down 2 < 0) : ¬IsRegularLocalRing ↑((AnalyticSpace.localModel ℝ 3 ⊤ umbrellaEq).presheaf.stalk z)

The handle of the umbrella: every point with z < 0 is a multiple point — the real points there form the z-axis (x² = z y² ≤ 0 forces x = y = 0), so the handle is disjoint from the closure of the simple points, although its real point set is a line.

noncomputable def Hironaka.Space.circleEq : Fin 1 → AnalyticSpace.AnalyticFun ℝ 2 ⊤

V(x² + y²) ⊆ ℝ²: the one equation x·x + y·y, the standard example of the phenomenon Hironaka remarks on [Hir64, Introduction].

Equations

• Hironaka.Space.circleEq = ![AnalyticSpace.coordSection ℝ 2 0 * AnalyticSpace.coordSection ℝ 2 0 + AnalyticSpace.coordSection ℝ 2 1 * AnalyticSpace.coordSection ℝ 2 1]

theorem Hironaka.Space.circleEq_germ (q : AnalyticSpace.Kn ℝ 2) : germTop (circleEq 0) q = AnalyticSpace.coordAt ℝ 2 q 0 * AnalyticSpace.coordAt ℝ 2 q 0 + AnalyticSpace.coordAt ℝ 2 q 1 * AnalyticSpace.coordAt ℝ 2 q 1

theorem Hironaka.Space.circle_setOf_isRegularLocalRing_stalk_eq_empty : {z : ↑↑(AnalyticSpace.localModel ℝ 2 ⊤ circleEq).toPresheafedSpace | IsRegularLocalRing ↑((AnalyticSpace.localModel ℝ 2 ⊤ circleEq).presheaf.stalk z)} = ∅

V(x² + y²) ⊆ ℝ² has no simple point. A point z of the model has x = y = 0 (a real sum of two squares vanishes only if both do), and there the equation lies in 𝔪² and does not vanish identically (x² ≠ 0 along the x-axis): X.regularLocus = ∅ although X ≠ ∅. This is the phenomenon Hironaka remarks on [Hir64, Introduction]. That the support is exactly the origin is not recorded as a separate statement here.