The singular locus of a reduced subspace contains no smooth hypersurface

For a reduced closed analytic subspace Y with ideal sheaf I, the singular locus Sing(Y) = Y ∖ Reg(Y) contains no nonempty closed smooth hypersurface H (IdealSheaf.not_subset_sing_of_isClosedSubmanifold_one), and no nonempty open set (IdealSheaf.not_subset_sing_of_isOpen). The hypersurface statement: at every point q of H the stalk I_q lies in the ideal (h) of H, h an adapted coordinate (every germ of I vanishes on Y ⊇ H), and h ∉ I_q, since otherwise I_q = (h) and 𝒪_q/I_q would be regular, against q ∈ Sing(Y). So the saturation (I : I_H^∞) (IdealSheaf.saturation) is a proper ideal at every point of H, hence its stalk at a ∈ H also lies in (h). For f ∈ I_a this gives f ∈ (h²), and then f ∈ (h^m) for every m by induction, since I_a is radical: from f = h^m g, (hg)^m = f g^{m−1} ∈ I_a, so hg ∈ I_a ⊆ (h²) and g ∈ (h), the stalk being a domain. Krull's intersection theorem (Ideal.iInf_pow_eq_bot_of_isLocalRing) then gives f = 0, so I_a = 0 and 𝒪_a/I_a = 𝒪_a is regular, against a ∈ Sing(Y). The open-set statement: a germ of I_a vanishing on a neighbourhood of a is zero, so I_a = 0.

These are the facts behind Włodarczyk's remark that the centres of the embedded desingularization have codimension at least two [Wlo09, Remark (2) after Theorem 2.0.3]: a centre of codimension at most one lies over Sing(Y), so it meets the exceptional divisor everywhere (Hironaka/Resolution/Analytic/Wlo09/CenterCodim.lean). The arguments are not in the sources.

theorem AnalyticManifold.IdealSheaf.not_subset_sing_of_isClosedSubmanifold_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (hI : I.IsReduced) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) (hsub : H ⊆ Manifold.IdealSheaf.support I \ I.regularLocus) (hne : H.Nonempty) : False

The singular locus of a reduced subspace contains no nonempty closed smooth hypersurface.

theorem AnalyticManifold.IdealSheaf.not_subset_sing_of_isOpen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {O : Set M.carrier} (hO : IsOpen O) (hsub : O ⊆ Manifold.IdealSheaf.support I \ I.regularLocus) (hne : O.Nonempty) : False

The singular locus of a subspace contains no nonempty open set: a germ vanishing on a neighbourhood is zero, so the stalk of I at a point of the open set is zero and the quotient is regular.