The real plane, its origin, and two hypersurface ideal sheaves

The data of two examples over ℝ: one showing that the ideal-theoretic strict transform of a closed subspace can be strictly larger than the closure of its part off the centre ([BM97, Example 3.16]), one showing that the simple locus of a nonempty real-analytic space can be empty, the phenomenon Hironaka remarks on for reduced spaces ([Hir64, Introduction]). The theorems about them are in RealPlaneCircle and RealPlaneStrictTransform; this file builds the data:

• realPlane: ℝ² (Fin 2 → ℝ) as a bundled analytic manifold with its identity chart;
• isClosedSubmanifold_origin: the origin is a closed submanifold of codimension 2 (the blow-up of the plane at the origin is then blowUp _ isClosedSubmanifold_origin);
• IdealSheaf.ofSectionOn: the ideal sheaf generated by one section over an open set that is the whole space (ofStalks with the constant generator), and its stalks;
• bm316Ideal: the ideal sheaf of x⁴(x−1)² + y² ([BM97, Example 3.16]), built from the coordinate sections chartSection of the identity chart;
• circleIdeal: the ideal sheaf of x² + y², the standard example of the phenomenon Hironaka remarks on [Hir64, Introduction], a reduced real-analytic space whose simple locus is not dense (reduced because x² + y² is irreducible in the ring ℝ{x, y} of convergent power series, so the quotient is a domain: circleSpace_isReduced of HironakaExamples/Space/CircleReduced.lean, for the analytic space of the same equation).

A principal ideal sheaf from one section on the whole space

noncomputable def Manifold.IdealSheaf.ofSectionOn {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X) (U : TopologicalSpace.Opens ↑X) (hU : ∀ (x : ↑X), x ∈ U) (s : ↑(𝒪.presheaf.obj (Opposite.op U))) : IdealSheaf 𝒪

The ideal sheaf generated by one section s over an open set U containing every point (ofStalks with the constant family of generators; the shape of IdealSheaf.ofGlobal, with U in place of ⊤).

Equations

• Manifold.IdealSheaf.ofSectionOn 𝒪 U hU s = Manifold.IdealSheaf.ofStalks 𝒪 (fun (x : ↑X) => Ideal.span {(CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U x ⋯)) s}) ⋯

theorem Manifold.IdealSheaf.stalkIdeal_ofSectionOn {X : TopCat} (𝒪 : TopCat.Sheaf CommRingCat X) (U : TopologicalSpace.Opens ↑X) (hU : ∀ (x : ↑X), x ∈ U) (s : ↑(𝒪.presheaf.obj (Opposite.op U))) (x : ↑X) : (ofSectionOn 𝒪 U hU s).stalkIdeal x = Ideal.span {(CategoryTheory.ConcreteCategory.hom (𝒪.presheaf.germ U x ⋯)) s}

The stalk at x of ofSectionOn U hU s is generated by the germ of s at x.

The real plane and its origin

@[reducible, inline]

abbrev Hironaka.Manifold.realPlane : AnalyticManifold ℝ (Fin 2 → ℝ)

ℝ² as a bundled analytic manifold (the model space with its identity chart; an abbrev so that the carrier is seen as Fin 2 → ℝ).

Equations

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

theorem Hironaka.Manifold.isClosedSubmanifold_origin : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) {0} 2

The origin of the plane is a closed submanifold of codimension 2 — the identity chart is adapted to it with all coordinates vanishing.

def Hironaka.Manifold.planeChart : TopologicalSpace.Opens realPlane.carrier

The source of the identity chart of the plane, as an open set (it is the whole plane).

Equations

• Hironaka.Manifold.planeChart = { carrier := (chartAt (Fin 2 → ℝ) 0).source, is_open' := Hironaka.Manifold.planeChart._proof_1 }

theorem Hironaka.Manifold.mem_planeChart (x : realPlane.carrier) : x ∈ planeChart

noncomputable def Hironaka.Manifold.planeCoordSection (i : Fin 2) : ↑((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.obj (Opposite.op planeChart))

The i-th coordinate function of the plane as a section of the structure sheaf over the identity chart (chartSection).

Equations

• Hironaka.Manifold.planeCoordSection i = Manifold.chartSection (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) Hironaka.Manifold.planeCoordSection._proof_1 i

The two example hypersurfaces

noncomputable def Hironaka.Manifold.bm316Section : ↑((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.obj (Opposite.op planeChart))

[BM97, Example 3.16]: the section x⁴(x−1)² + y².

Equations

• Hironaka.Manifold.bm316Section = Hironaka.Manifold.planeCoordSection 0 ^ 4 * (Hironaka.Manifold.planeCoordSection 0 - 1) ^ 2 + Hironaka.Manifold.planeCoordSection 1 ^ 2

noncomputable def Hironaka.Manifold.bm316Ideal : realPlane.IdealSheaf

[BM97, Example 3.16]: the ideal sheaf of X = V(x⁴(x−1)² + y²) ⊆ ℝ².

Equations

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

theorem Hironaka.Manifold.stalkIdeal_bm316Ideal (x : realPlane.carrier) : Manifold.IdealSheaf.stalkIdeal bm316Ideal x = Ideal.span {(CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.germ planeChart x ⋯)) bm316Section}

noncomputable def Hironaka.Manifold.circleSection : ↑((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.obj (Opposite.op planeChart))

The section x² + y², the standard example of the phenomenon Hironaka remarks on [Hir64, Introduction].

Equations

• Hironaka.Manifold.circleSection = Hironaka.Manifold.planeCoordSection 0 ^ 2 + Hironaka.Manifold.planeCoordSection 1 ^ 2

noncomputable def Hironaka.Manifold.circleIdeal : realPlane.IdealSheaf

The ideal sheaf of X = V(x² + y²) ⊆ ℝ², with support the origin (circleIdeal_cosupport_eq_singleton) and no simple point (circleIdeal_regSet_eq_empty), both in RealPlaneCircle; that X is reduced is circleSpace_isReduced of HironakaExamples/Space/CircleReduced.lean, for the analytic space of the same equation.

Equations

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

theorem Hironaka.Manifold.stalkIdeal_circleIdeal (x : realPlane.carrier) : Manifold.IdealSheaf.stalkIdeal circleIdeal x = Ideal.span {(CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.germ planeChart x ⋯)) circleSection}