V(x² + y²) ⊆ ℝ² has support the origin and no simple point

The standard example x² + y² of the phenomenon Hironaka remarks on [Hir64, Introduction], a reduced real-analytic space whose simple locus is not dense: the closed subspace X = V(x² + y²) of the real plane (reduced, since x² + y² is irreducible in ℝ{x, y} and the quotient 𝒪_{ℝ²,0} / (x² + y²) is therefore a domain: circleSpace_isReduced of HironakaExamples/Space/CircleReduced.lean, for the analytic space of the same equation) has the single real point 0, and 0 is not a simple point — the stalk 𝒪_{ℝ²,0} / (x² + y²) is not regular, since x² + y² is a nonzero element of 𝔪_0² of the regular local ring 𝒪_{ℝ²,0} (Hironaka.Local.not_isRegularLocalRing_quotient_span_singleton, [TSPA, Tag 00NR]). So X.regularLocus = ∅ with X ≠ ∅, and the lift of the simple locus is empty; this is why the resolution of real-analytic spaces (AnalyticSpace.exists_functorial_resolution) asserts only that the image of the resolution is the closure of the simple locus.

• the coordinate germs of the identity chart at a point of the plane, their values and the germ of x² + y² (germ_circleSection, extendSection_circleSection);
• circleIdeal_cosupport_eq_singleton: |X| = {0} (x² + y² = 0 iff x = y = 0 over ℝ);
• circleIdeal_regSet_eq_empty: no simple point — the stalk of X at its only point is 𝒪_{ℝ²,0} / (x² + y²) (mem_reg_toAnalyticSpace_iff), x² + y² ∈ 𝔪_0², and x² + y² does not vanish identically near 0 (its value at (t, t) is 2 t²; the identity lemma germ_eq_zero_iff).

The plane's coordinate germs at a point

theorem Hironaka.Manifold.mem_chartAt_source_plane (x : realPlane.carrier) : x ∈ (chartAt (Fin 2 → ℝ) 0).source

Every point of the plane lies in the source of the identity chart (the form rw needs).

theorem Hironaka.Manifold.germ_planeCoordSection (x : realPlane.carrier) (i : Fin 2) : (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.germ planeChart x ⋯)) (planeCoordSection i) = Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ i

The germ at x of the i-th coordinate section is the coordinate germ of the identity chart (coord).

theorem Hironaka.Manifold.eval_coord_plane (x : realPlane.carrier) (i : Fin 2) : (Manifold.eval ℝ (Fin 2 → ℝ) realPlane.carrier x) (Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ i) = x i

The value at x of the i-th coordinate germ is x i.

theorem Hironaka.Manifold.germ_circleSection (x : realPlane.carrier) : (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.germ planeChart x ⋯)) circleSection = Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ 0 ^ 2 + Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ 1 ^ 2

The germ of x² + y² at x in the coordinate germs.

theorem Hironaka.Manifold.extendSection_circleSection (p : realPlane.carrier) : Manifold.extendSection ℝ (Fin 2 → ℝ) circleSection p = p 0 ^ 2 + p 1 ^ 2

The value of x² + y² at a point p of the plane is p 0 ^ 2 + p 1 ^ 2.

V(x² + y²): the support and the simple points

theorem Hironaka.Manifold.circleIdeal_cosupport_eq_singleton : Manifold.IdealSheaf.support circleIdeal = {0}

The support of V(x² + y²) ⊆ ℝ² is the origin ([Hir64, Introduction]).

theorem Hironaka.Manifold.coord_plane_mem_maximalIdeal (i : Fin 2) : Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ i ∈ IsLocalRing.maximalIdeal ↑((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.stalk 0)

The coordinate germs at the origin lie in the maximal ideal.

theorem Hironaka.Manifold.germ_circleSection_ne_zero : (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.germ planeChart 0 ⋯)) circleSection ≠ 0

x² + y² does not vanish identically near the origin: its value at (t, t) is 2 t² (the identity lemma germ_eq_zero_iff).

theorem Hironaka.Manifold.not_isRegularLocalRing_stalk_circleIdeal {x : realPlane.carrier} (hx : x ∈ Manifold.IdealSheaf.support circleIdeal) : ¬IsRegularLocalRing (↑((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.stalk x) ⧸ Manifold.IdealSheaf.stalkIdeal circleIdeal x)

At a point of the support of x² + y² (the origin), 𝒪_{ℝ²,0}/(x² + y²) is not a regular local ring: x² + y² is a nonzero element of the square of the maximal ideal.

theorem Hironaka.Manifold.circleIdeal_regSet_eq_empty : circleIdeal.regSet = ∅

V(x² + y²) ⊆ ℝ² has no simple point ([Hir64, Introduction]). At the only point 0 the stalk of X is 𝒪_{ℝ²,0} / (x² + y²) (mem_reg_toAnalyticSpace_iff) with x² + y² a nonzero element of 𝔪_0², and a regular local ring modulo a nonzero element of 𝔪² is not regular.