The real-analytic space V(x² + y²) ⊆ ℝ²

Hironaka's remark that the simple locus of a reduced real-analytic space need not be dense [Hir64, Introduction], on the example V(x² + y²) ⊆ ℝ²: circleSpace is the local analytic ℝ-space of the single equation z₀² + z₁² on ℝ² (circleEq of HironakaExamples/JacobianCriterion.lean). Its support is the origin (circleSpace_eq_zero, subsingleton_circleSpace, nonempty_circleSpace: x² + y² = 0 ⇒ x = y = 0 over ℝ) and its simple locus is empty (reg_circleSpace_eq_empty, from circle_setOf_isRegularLocalRing_stalk_eq_empty); it is reduced (HironakaExamples/Space/CircleReduced.lean).

Hironaka's example V(x² + y²) ⊆ ℝ²

noncomputable def Hironaka.Space.circleSpace : AnalyticSpace ℝ

The real-analytic space V(x² + y²) ⊆ ℝ²: the local analytic ℝ-space of the single equation z₀² + z₁² on ℝ² (circleEq of HironakaExamples/JacobianCriterion.lean). Its underlying set is the origin, it is reduced (x² + y² is irreducible in ℝ{x, y}), and its only point is singular (𝒪_{X,0} = ℝ{x, y}/(x² + y²) is not regular): the simple locus is empty although X ≠ ∅: the standard example of the phenomenon Hironaka remarks on, that for a reduced real-analytic space the simple locus need not be dense [Hir64, Introduction].

Equations

• Hironaka.Space.circleSpace = AnalyticSpace.localModelSpace ℝ 2 ⊤ Hironaka.Space.circleEq

theorem Hironaka.Space.circleSpace_toKLocallyRingedSpace : circleSpace.toKLocallyRingedSpace = AnalyticSpace.localModel ℝ 2 ⊤ circleEq

The circle V(x² + y²) ⊆ ℝ²: its points and its simple locus

theorem Hironaka.Space.circleSpace_eq_zero (z : ↑↑circleSpace.toPresheafedSpace) : ↑↑z = { down := 0 }

A point of V(x² + y²) is a point of ℝ² with x² + y² = 0.

theorem Hironaka.Space.subsingleton_circleSpace : Subsingleton ↑↑circleSpace.toPresheafedSpace

The underlying set of V(x² + y²) is a single point.

theorem Hironaka.Space.nonempty_circleSpace : Nonempty ↑↑circleSpace.toPresheafedSpace

The origin lies on V(x² + y²).

theorem Hironaka.Space.reg_circleSpace_eq_empty : circleSpace.regularLocus = ∅

V(x² + y²) ⊆ ℝ² has no simple point (circle_setOf_isRegularLocalRing_stalk_eq_empty).