The subspace predicates on analytic manifolds: elementary facts

The elementary facts about the predicates of Hironaka's Definitions 1 and 2 on the ideal sheaves of an analytic manifold — IsInvertible, IsReduced, IsNonsingular, IsIrreducible, HasOnlyNormalCrossingsWith, HasOnlyNormalCrossings, IsNormalCrossingsDivisor — and the reduced transform IdealSheaf.reducedTransform: the two branches of the reduced transform and its set of points (f⁻¹(E) ∪ f⁻¹(D) on either branch, [Hir64, Main Theorem II'(N) (iii), p. 156]); the ideal sheaf of a closed submanifold defines a non-singular subspace — its quotient stalks are the stalks of the submanifold (Hironaka/Manifold/Submanifold/Ideal.lean), regular local rings (Hironaka/Manifold/Germ/StalkNoetherian.lean) — hence the centre of every monoidal transformation is non-singular (Bierstone–Milman's blowing-up has a closed submanifold as centre, [BM88, Definition 4.1]); a non-singular subspace is reduced (a regular local ring is a domain, so the stalks are prime); an irreducible subspace is nonempty; and the reduced transform is natural along a square of analytic isomorphisms, the compatibility of the boundary with local isomorphisms that the functoriality of the resolution needs.

The reduced transform: the two branches and the set of points

theorem Manifold.reducedTransform_eq_of_hasLocalGenerators {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (D B : N.IdealSheaf) (h : IdealSheaf.HasLocalGenerators fun (x : N'.carrier) => vanishingStalk (⇑f ⁻¹' IdealSheaf.support B ∪ ⇑f ⁻¹' IdealSheaf.support D) x) : AnalyticManifold.IdealSheaf.reducedTransform f B D = IdealSheaf.ofStalks (structureSheaf 𝕜 E N'.carrier) (fun (x : N'.carrier) => vanishingStalk (⇑f ⁻¹' IdealSheaf.support B ∪ ⇑f ⁻¹' IdealSheaf.support D) x) h

The reduced transform on the branch where the vanishing ideals of f⁻¹(E) ∪ f⁻¹(D) have local generators is the ideal sheaf with those stalks.

theorem Manifold.reducedTransform_eq_mul_of_not {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (D B : N.IdealSheaf) (h : ¬IdealSheaf.HasLocalGenerators fun (x : N'.carrier) => vanishingStalk (⇑f ⁻¹' IdealSheaf.support B ∪ ⇑f ⁻¹' IdealSheaf.support D) x) : AnalyticManifold.IdealSheaf.reducedTransform f B D = IdealSheaf.pullback ⇑f ⋯ B * IdealSheaf.pullback ⇑f ⋯ D

The reduced transform on the other branch is the product f^*E · f^*D.

theorem Manifold.reducedTransform_stalkIdeal_of_hasLocalGenerators {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (D B : N.IdealSheaf) (h : IdealSheaf.HasLocalGenerators fun (x : N'.carrier) => vanishingStalk (⇑f ⁻¹' IdealSheaf.support B ∪ ⇑f ⁻¹' IdealSheaf.support D) x) (x : N'.carrier) : IdealSheaf.stalkIdeal (AnalyticManifold.IdealSheaf.reducedTransform f B D) x = vanishingStalk (⇑f ⁻¹' IdealSheaf.support B ∪ ⇑f ⁻¹' IdealSheaf.support D) x

On the first branch the stalks of the reduced transform are the vanishing ideals of f⁻¹(E) ∪ f⁻¹(D).

theorem Manifold.reducedTransform_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (D B : N.IdealSheaf) : IdealSheaf.support (AnalyticManifold.IdealSheaf.reducedTransform f B D) = ⇑f ⁻¹' IdealSheaf.support B ∪ ⇑f ⁻¹' IdealSheaf.support D

The set of points of red(f⁻¹(E) ∪ f⁻¹(D)) is f⁻¹(E) ∪ f⁻¹(D), on either branch of the definition [Hir64, Main Theorem II'(N) (iii), p. 156].

Non-singular, reduced, irreducible

theorem AnalyticManifold.IdealSheaf.IsIrreducible.nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {J : N.IdealSheaf} (hJ : J.IsIrreducible) : (Manifold.IdealSheaf.support J).Nonempty

An irreducible subspace is nonempty (Hironaka's "irreducible" includes nonempty, [Hir64, Definition 2, p. 141]).

theorem Manifold.IsNonsingular.isReduced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {J : N.IdealSheaf} (hJ : J.IsNonsingular) : J.IsReduced

A non-singular subspace is reduced: its stalks are prime off the unit ideal (a regular local ring is a domain).

theorem Manifold.isNonsingular_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {Y : Set N.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : AnalyticManifold.IdealSheaf.IsNonsingular hY.idealSheaf

The ideal sheaf of a closed submanifold defines a non-singular subspace ([Hir64, p. 121]): its quotient stalks 𝒪_{M,a}/𝓘_{Y,a} ≅ 𝒪_{Y,a} are the stalks of the manifold Y, regular local rings.

theorem Manifold.IsMonoidalTransformation.isNonsingular {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (D : N.IdealSheaf) (hf : f.IsMonoidalTransformation D) : D.IsNonsingular

The centre of a monoidal transformation is non-singular (Bierstone–Milman's blowing-up has a closed analytic submanifold as centre, [BM88, Definition 4.1]).

Naturality of the reduced transform along a square of diffeomorphisms

theorem Manifold.reducedTransform_pullback_of_comp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ M₂ : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁.carrier M₂.carrier ⊤) {N₁ N₂ : AnalyticManifold 𝕜 E} (f₁ : AnalyticMap N₁ M₁) (f₂ : AnalyticMap N₂ M₂) (g' : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N₁.carrier N₂.carrier ⊤) (hsq : ⇑f₂ ∘ ⇑g' = ⇑g ∘ ⇑f₁) (D B : M₂.IdealSheaf) : IdealSheaf.pullback ⇑g' ⋯ (AnalyticManifold.IdealSheaf.reducedTransform f₂ B D) = AnalyticManifold.IdealSheaf.reducedTransform f₁ (IdealSheaf.pullback ⇑g ⋯ B) (IdealSheaf.pullback ⇑g ⋯ D)

The reduced transform is natural along a square of diffeomorphisms f₂ ∘ g' = g ∘ f₁: g'^* red(f₂⁻¹E ∪ f₂⁻¹D) = red(f₁⁻¹ g^*E ∪ f₁⁻¹ g^*D), on either branch of the definition — the closed sets correspond under g', their vanishing ideals under the germ maps of g', the local-generator condition is invariant, and on the product branch the pullbacks compose (the compatibility of the boundary with the pull-back of a blow-up sequence along a local isomorphism, [Kol07, 30.1]).