V(x² + y²) ⊆ ℝ² is reduced

The real-analytic space X = V(x² + y²) ⊆ ℝ² is reduced although its simple locus is empty: the example behind Hironaka's remark that the simple locus of a reduced real-analytic space need not be dense [Hir64, Introduction]. Reducedness: the only point of X is the origin, where the local ring is ℝ{x, y}/(x² + y²); x² + y² is irreducible in the unique factorisation domain ℝ{x, y} (Hironaka/Analytic/Rueckert/UFD.lean), hence prime, so the quotient is a domain.

• sumSquares = X₀² + X₁² ∈ Conv ℝ 2 and irreducible_sumSquares: if X₀² + X₁² = a b with a(0) = b(0) = 0, the coefficients of x², y² and xy give a₁ b₁ = 1, a₂ b₂ = 1, a₁ b₂ + a₂ b₁ = 0 for the linear coefficients, whence a₁² + a₂² = 0 — impossible over ℝ; so one factor has a nonzero constant term and is a unit (isUnit_iff_constantCoeff_ne_zero). Hence prime_sumSquares (irreducible_iff_prime in a unique factorisation monoid) and the prime ideal (x² + y²).
• The stalk of X at its point is 𝒜_{⊤,0}/𝓘_0 (stalkEquiv), 𝓘_0 the image of the ambient ideal (germ (x² + y²)) of 𝒜_{ℝ²,0} (stalkIdeal_modelIdeal_eq_map), which the Taylor isomorphism 𝒜_{ℝ²,0} ≅ ℝ{x, y} (taylorEquivConv) carries to (X₀² + X₁²) (the coordinate germs at 0 go to X_i); prime ideals correspond, the quotient is a domain, and reducedness passes back along the isomorphisms.

x² + y² is irreducible in ℝ{x, y}

noncomputable def Hironaka.Space.sumSquares : ↥(Analytic.Conv ℝ 2)

X₀² + X₁² ∈ ℝ{x, y}.

Equations

• Hironaka.Space.sumSquares = Analytic.convX ℝ 0 ^ 2 + Analytic.convX ℝ 1 ^ 2

theorem Hironaka.Space.coe_sumSquares : ↑sumSquares = MvPowerSeries.X 0 ^ 2 + MvPowerSeries.X 1 ^ 2

theorem Hironaka.Space.single_zero_two_ne_single_one_two : Finsupp.single 0 2 ≠ Finsupp.single 1 2

theorem Hironaka.Space.single_add_single_ne_single_zero : Finsupp.single 0 1 + Finsupp.single 1 1 ≠ Finsupp.single 0 2

theorem Hironaka.Space.single_add_single_ne_single_one : Finsupp.single 0 1 + Finsupp.single 1 1 ≠ Finsupp.single 1 2

theorem Hironaka.Space.coeff_single_two_sumSquares (s : Fin 2) : (MvPowerSeries.coeff (Finsupp.single s 2)) ↑sumSquares = 1

theorem Hironaka.Space.coeff_single_add_single_sumSquares : (MvPowerSeries.coeff (Finsupp.single 0 1 + Finsupp.single 1 1)) ↑sumSquares = 0

theorem Hironaka.Space.sumSquares_ne_zero : sumSquares ≠ 0

theorem Hironaka.Space.constantCoeff_sumSquares : MvPowerSeries.constantCoeff ↑sumSquares = 0

theorem Hironaka.Space.nat_antidiagonal_two : Finset.antidiagonal 2 = {(0, 2), (1, 1), (2, 0)}

The antidiagonal of 2 in ℕ.

theorem Hironaka.Space.coeff_single_two_mul {a b : MvPowerSeries (Fin 2) ℝ} (ha : MvPowerSeries.constantCoeff a = 0) (hb : MvPowerSeries.constantCoeff b = 0) (s : Fin 2) : (MvPowerSeries.coeff (Finsupp.single s 2)) (a * b) = (MvPowerSeries.coeff (Finsupp.single s 1)) a * (MvPowerSeries.coeff (Finsupp.single s 1)) b

The x_s²-coefficient of a product of two series without constant term.

theorem Hironaka.Space.antidiagonal_single_add_single : Finset.antidiagonal (Finsupp.single 0 1 + Finsupp.single 1 1) = {(0, Finsupp.single 0 1 + Finsupp.single 1 1), (Finsupp.single 0 1, Finsupp.single 1 1), (Finsupp.single 1 1, Finsupp.single 0 1), (Finsupp.single 0 1 + Finsupp.single 1 1, 0)}

The antidiagonal of e₀ + e₁ in Fin 2 →₀ ℕ.

theorem Hironaka.Space.coeff_single_add_single_mul {a b : MvPowerSeries (Fin 2) ℝ} (ha : MvPowerSeries.constantCoeff a = 0) (hb : MvPowerSeries.constantCoeff b = 0) : (MvPowerSeries.coeff (Finsupp.single 0 1 + Finsupp.single 1 1)) (a * b) = (MvPowerSeries.coeff (Finsupp.single 0 1)) a * (MvPowerSeries.coeff (Finsupp.single 1 1)) b + (MvPowerSeries.coeff (Finsupp.single 1 1)) a * (MvPowerSeries.coeff (Finsupp.single 0 1)) b

The xy-coefficient of a product of two series without constant term.

theorem Hironaka.Space.irreducible_sumSquares : Irreducible sumSquares

x² + y² is irreducible in ℝ{x, y}: a factorisation x² + y² = a b with a(0) = b(0) = 0 would give a₁ b₁ = a₂ b₂ = 1 and a₁ b₂ + a₂ b₁ = 0 for the linear coefficients, i.e. a₁² + a₂² = 0, impossible over ℝ.

theorem Hironaka.Space.prime_sumSquares : Prime sumSquares

theorem Hironaka.Space.isPrime_span_sumSquares : (Ideal.span {sumSquares}).IsPrime

The stalk of V(x² + y²) at the origin

noncomputable def Hironaka.Space.taylorOrigin : ↑((AnalyticSpace.affine ℝ 2).presheaf.stalk { down := 0 }) ≃+* ↥(Analytic.Conv ℝ 2)

The Taylor isomorphism 𝒜_{ℝ²,0} ≃ ℝ{x, y} in the identity chart.

Equations

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

theorem Hironaka.Space.taylorOrigin_germTop_circleEq : taylorOrigin (germTop (circleEq 0) { down := 0 }) = sumSquares

The Taylor series of x² + y² at the origin is X₀² + X₁².

theorem Hironaka.Space.isPrime_ambientIdeal_circleEq : (AnalyticSpace.ambientIdeal ℝ 2 ⊤ circleEq { down := 0 }).IsPrime

The ambient ideal (x² + y²) of 𝒜_{ℝ²,0} is prime.

theorem Hironaka.Space.isPrime_ambientIdeal_circleEq_of_eq (q : AnalyticSpace.Kn ℝ 2) (hq : q = { down := 0 }) : (AnalyticSpace.ambientIdeal ℝ 2 ⊤ circleEq q).IsPrime

theorem Hironaka.Space.isPrime_stalkIdeal_circleEq (z : ↑↑circleSpace.toPresheafedSpace) : (AnalyticSpace.QuotientSpace.stalkIdeal (AnalyticSpace.analyticSpaceOfOpen ℝ 2 ⊤).toLocallyRingedSpace (AnalyticSpace.modelIdeal ℝ 2 ⊤ circleEq) ↑z).IsPrime

The stalk ideal of V(x² + y²) at its point is prime.

theorem Hironaka.Space.circleSpace_isReduced : circleSpace.IsReduced

V(x² + y²) ⊆ ℝ² is reduced: the standard example of a reduced real-analytic space whose simple locus is empty (the phenomenon Hironaka remarks on in [Hir64, Introduction]).