Density of the simple points of a reduced complex space #
The simple points of a reduced complex analytic space are dense [Fre17, II 5.13]: Hironaka's
remark that "if X is a reduced complex-analytic space, then the open subspace V is dense in
X" [Hir64, Introduction]. This file proves it (dense_reg_of_isReduced_of_hyps) from two
statements of the local parametrization theory of a prime germ, taken as explicit hypotheses
h17a, h17c and proved in Hironaka/Analytic/Rueckert/ParametrizationPrimitive.lean
(exists_primitive_normalization) and ParametrizationGraph.lean (exists_graph_of_isPrime); the
unconditional statement is Manifold.dense_reg_of_isReduced_complex of
Hironaka/Manifold/FiniteSuccession/Restrict/LiftRegDense.lean.
The argument (Freitag's, with one change). Let x be a point of a reduced complex space X,
not simple; X|U ≅ (localModel V(f))|W near x, z the image of x, and I = (f)_z ⊆ 𝒪_n the
ideal of the model at z read through the Taylor isomorphism. Because every stalk of X is
reduced, (f)_{z'} is radical at every point z' of W — Freitag spreads radicality from z by
Cartan's coherence theorem, which is therefore not needed. I ≠ ⊤, ⊥ (z is a point, and
𝒪_n/⊥ = 𝒪_n is regular). Take a minimal prime P of I (finitely many) and a separating
series h₀ in every other minimal prime but not in P (prime avoidance). The local
parametrization theorem gives a Noether normalization with a primitive fibre coordinate (h17a:
Q, A, B_i, in the coordinates of σ = substEquiv L, i.e. for P' = comap σ P) and the
graph structure of V(P') near every point x' off A · Res(Q, Q') (h17c). Rückert's
Nullstellensatz gives points x' of V(P') arbitrarily near 0 off
g := (A · Res)(X ∘ e) · σ⁻¹ h₀ (frequently_mem_zeroSet_and_ne_zero). At such x': (i)
V(I') = V(P') near x' (I' = comap σ I): every F ∈ P' has F · σ⁻¹h₀ ∈ I'
(mul_mem_of_mem_minimalPrimes_of_forall_mem), and σ⁻¹h₀ does not vanish near x'; (ii)
V(I') is the translated point set of the model
(eventually_forall_evalSeries_modelGens_eq_zero_iff, eventually_mem_zeroSet_image_symm_iff),
so z' with z'.1.1 = z.1.1 + L⁻¹ x' is a point of the model, in W and in any prescribed
neighbourhood of z (eventually_exists_localModel_pt, exists_mem_nhds_of_mem_opens_localModel,
exists_mem_nhds_of_mem_nhds_localModel_restrict); (iii) the ideal comap σ (f)_{z'} has, near
0, the zero set of the graph ideal J = (X_j − T_j(X ∘ e))_j of the translated graph
(eventually_graph_eq_zero_iff), J is prime because 𝒪_n/J is regular
(isRegularLocalRing_quotient_graphIdeal; a regular local ring is a domain), both are radical, so
Rückert identifies them (eq_of_isRadical_of_zeroSet_eventuallyEq) and 𝒪_n/(f)_{z'} is regular
(isRegularLocalRing_quotient_comap_iff); (iv) the point of X under z' is simple
(mem_reg_iff_isRegularLocalRing_quotient) and lies in the prescribed neighbourhood of x
(exists_regular_pt_of_hyps, dense_reg_of_isReduced_of_hyps). The parametrization is that of
[GR84, Ch. 3–4]. Used by Hironaka/Manifold/FiniteSuccession/Restrict/LiftRegDense.lean.
The finite generating system of (f)_z in Conv ℂ n.
Equations
Instances For
modelGensFinset generates (f)_z.
The zero set of modelGensFinset.
The core of [Fre17, II 5.13] on a local model over ℂ, in the form the component clauses use:
at a point z of a model whose ideals are radical on an open W ∋ z, every nonzero minimal prime
P of (f)_z comes with a normalizing linear change of coordinates L, a generating system S
of P' = comap σ P and a series g ∉ P' such that every point x' of V(P') near 0 off g
is, in the original coordinates, a simple model point of W — given the local parametrization
theorem (the two statements h17a, h17c as hypotheses).
The core of [Fre17, II 5.13] on a local model over ℂ: near a non-simple point z of a model
whose ideals are radical on an open W ∋ z, there are points of W with regular 𝒪_n/(f)_{z'} in
every neighbourhood of z in (localModel)|W — given the local parametrization theorem (h17a,
h17c as hypotheses).
The simple points of a reduced complex analytic space are dense [Fre17, II 5.13],
[Hir64, Introduction] — given the local parametrization theorem (h17a, h17c as hypotheses);
unconditionally, Manifold.dense_reg_of_isReduced_complex of
Hironaka/Manifold/FiniteSuccession/Restrict/LiftRegDense.lean.