The strict transform as the saturation of the total transform

Włodarczyk's strict transform Ỹ ⊂ M̃ [Wlo09, Theorem 2.0.2] is defined here on the glued space M̃ as the saturation of the total transform σ^*(I_Y) by the exceptional divisor E (IdealSheaf.saturation: the ideal sheaf whose stalk at q is ⋃_k (σ^*(I_Y)_q : E_q^k), coherent by the finite type of saturations, [BM97, Proposition 3.13], AnalyticSpace.saturation_hasLocalGenerators). The library's strict transform along a succession is built stage by stage; this module shows that at the last stage of a succession desingularizing Y (IdealSheaf.IsDesingularizedBy) it is the saturation of the total transform along the composite by the last exceptional divisor (IsDesingularizedBy.stalkIdeal_strictTransformSubspaceSeq_last_eq_iSup_colon), from the clauses (3) and (6) alone: with J the stalk of Ỹ, e a generator of the stalk of E_r and σ^*(I_Y) = J · m with m a monomial in the members of E_r through the point (clause (6)), m divides a power of e, so J ⊆ (J m : e^∞); and J is prime (the quotient is a regular local ring by (3), hence a domain) with e ∉ J: e is a product of coordinates of a chart adapted to Ỹ off the block of Ỹ (the transversality of (3)), and such a coordinate does not vanish on Ỹ near the point (coord_notMem_vanishingStalk_of_notMem_range), while every element of J does. Not in the sources beyond the statements cited; the saturation description of the strict transform is [BM97, Proposition 3.13].

theorem Manifold.coord_notMem_vanishingStalk_of_notMem_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {φ : OpenPartialHomeomorph M E} {c : ℕ} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) {a : M} (ha : a ∈ φ.source) (haY : a ∈ Y) {k : Fin n} (hk : k ∉ Set.range ⇑σ) : coord E ψ φ ⋯ ha k ∉ vanishingStalk Y a

A coordinate of a chart adapted to Y off the block of Y does not vanish on Y near a point a of Y: along the curve t ↦ φ⁻¹(φ(a) + t e_k), which lies in Y and tends to a, the coordinate is z_k(a) + t.

theorem Ideal.le_iSup_colon_pow_of_pow_mem {R : Type u_1} [CommRing R] {J T B m : Ideal R} {e : R} (hT : T = J * m) (hB : B = span {e}) {N : ℕ} (hpow : e ^ N ∈ m) : J ≤ ⨆ (k : ℕ), Submodule.colon T ↑(B ^ k)

The two inclusions of the saturation identity, in a commutative ring: if T = J m and B = (e) with e^N ∈ m, then J ⊆ ⋃_k (T : B^k).

theorem Ideal.iSup_colon_pow_le_of_isPrime {R : Type u_1} [CommRing R] {J T B m : Ideal R} {e : R} (hT : T = J * m) (hB : B = span {e}) (hne : e ∉ J) (hJ : J.IsPrime) : ⨆ (k : ℕ), Submodule.colon T ↑(B ^ k) ≤ J

If moreover J is prime and e ∉ J, then ⋃_k (T : B^k) ⊆ J.

theorem AnalyticManifold.IdealSheaf.hasLocalGenerators_saturation {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (J B : M.IdealSheaf) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↧M.carrier) => ⨆ (k : ℕ), Submodule.colon (Manifold.IdealSheaf.stalkIdeal J x) ↑(Manifold.IdealSheaf.stalkIdeal B x ^ k)

The saturation stalks ⋃_k (J_x : B_x^k) of an ideal sheaf J by an ideal sheaf B have local generators: Bierstone–Milman's finite type of saturations [BM97, Proposition 3.13] (AnalyticSpace.saturation_hasLocalGenerators, read on the analytic space of M).

noncomputable def AnalyticManifold.IdealSheaf.saturation {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (J B : M.IdealSheaf) : M.IdealSheaf

The saturation of J by B: the ideal sheaf whose stalk at x is ⋃_k (J_x : B_x^k), the germs g with b g ∈ J_x for some b ∈ B_x^k. For J = σ^*(I_Y) and B the exceptional divisor it is the strict transform of Y [BM97, Proposition 3.13].

Equations

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

@[simp]

theorem AnalyticManifold.IdealSheaf.stalkIdeal_saturation {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (J B : M.IdealSheaf) (x : M.carrier) : Manifold.IdealSheaf.stalkIdeal (J.saturation B) x = ⨆ (k : ℕ), Submodule.colon (Manifold.IdealSheaf.stalkIdeal J x) ↑(Manifold.IdealSheaf.stalkIdeal B x ^ k)

theorem AnalyticManifold.IdealSheaf.saturation_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (J B : M.IdealSheaf) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : Manifold.IdealSheaf.pullback ⇑g ⋯ (J.saturation B) = saturation (Manifold.IdealSheaf.pullback ⇑g ⋯ J) (Manifold.IdealSheaf.pullback ⇑g ⋯ B)

The saturation pulls back along a local analytic isomorphism to the saturation of the pull-backs: the colon ideals and their union transport along the bijective germ maps (Ideal.map_colon_pow_of_bijective, Ideal.map_iSup).

theorem AnalyticManifold.IdealSheaf.IsDesingularizedBy.stalkIdeal_strictTransformSubspaceSeq_last_eq_iSup_colon {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {S : M.FiniteSuccession} (h : I.IsDesingularizedBy S) (a : S.last.carrier) : Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq I (Fin.last S.length)) a = ⨆ (k : ℕ), Submodule.colon ((Manifold.IdealSheaf.pullback ⇑S.composite ⋯ I).stalkIdeal a) ↑(Manifold.IdealSheaf.stalkIdeal (S.boundarySeq ⊤ (Fin.last S.length)) a ^ k)

The last strict transform is the saturation of the total transform by the last exceptional divisor, at every point, for a succession desingularizing Y: from clauses (3) and (6) of [Wlo09, Theorem 2.0.2] (isNonsingular_strictTransform, isSncBoundaryTransversalTo_strictTransform, isMulBoundaryMonomial_pullback).

theorem AnalyticManifold.IdealSheaf.IsDesingularizedBy.strictTransformSubspaceSeq_last_eq_saturation {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {S : M.FiniteSuccession} (h : I.IsDesingularizedBy S) : S.strictTransformSubspaceSeq I (Fin.last S.length) = saturation (Manifold.IdealSheaf.pullback ⇑S.composite ⋯ I) (S.boundarySeq ⊤ (Fin.last S.length))

The last strict transform of a succession desingularizing Y is the saturation of the total transform of I_Y along the composite by the last exceptional divisor.