The class of reduced closed subspaces and the type of embedded-desingularization functors

The embedded desingularization of a reduced closed analytic subspace Y of a manifold M [Wlo09, Theorem 2.0.2] (also [Wlo05, Theorem 4.7.1]) is, in this library, the value of a family functor on the triple (M, I_Y, ∅). This file defines the class and the type in which that functor is stated, beside the family records of Hironaka.Resolution.Analytic.Functor.Family:

• DomBEDan 𝕜: the class of analytic triples at the standard model with E = ∅ (IsEmpty T.F.ι) and 𝓘 reduced (IdealSheaf.IsReduced: every stalk radical), Włodarczyk's hypothesis of a reduced closed subspace Y, with no dimension clause. The ideal sheaves of the vocabulary are locally finitely generated by definition, so the class is exactly the reduced ideals of closed analytic subspaces; the triple's own isNonzeroEverywhere is the one extra condition.
• BEDanFam 𝕜 n: the type of family functors on the class, a compatible family of finite blow-up sequences for every triple of the class; reducible, so that the predicates of family functors and the field fam apply to its terms directly.
• BEDanFamStar 𝕜: the all-dimensions record, fam : ∀ n, BEDanFam 𝕜 n with the ambient closed-embedding clause of [Wlo09, Theorem 2.0.2, (4)] in its per-open form (CommutesWithClosedEmbeddingsOfEmptyDivisorFam), and BEDanFamStar.IsEmbeddedDesing, the clauses of [Wlo09, Theorem 2.0.2] that the main theorem asserts of some bed : BEDanFamStar 𝕜; theorems about an arbitrary bed are stated under this predicate.

Clause (6) of IsEmbeddedDesing binds its exponents per point, ∀ x, ∃ (s : Finset ι) (α : ι → ℕ), …: one exponent per irreducible component of the exceptional divisor through the point, as in [Wlo09, Theorem 2.0.2] (Ẽ a locally finite combination of the irreducible components of E_r); binding ∃ α before ∀ x would give one exponent per member of totalTransformSeq, a member being the whole exceptional divisor π⁻¹(Z_i) of one blow-up, a stronger statement than the source when a centre is disconnected. The functor itself is built from the modified marked resolution of [Wlo09, §7] in the order-reduction modules.

def Hironaka.Manifold.DomBEDan (𝕜 : Type) [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M → Prop

The class of reduced closed subspaces — the analytic triples (M, 𝓘, E) at the standard model with E = ∅ (no boundary components) and 𝓘 the reduced ideal of a closed analytic subspace Y (IdealSheaf.IsReduced: every stalk radical). No dimension clause on Y.

Equations

• Hironaka.Manifold.DomBEDan 𝕜 T = (IsEmpty T.F.ι ∧ T.I.IsReduced)

@[reducible, inline]

abbrev Hironaka.Manifold.BEDanFam (𝕜 : Type) [RCLike 𝕜] (n : ℕ) : Type (u + 1)

The type of family functors BED^{an} in dimension n — AnalyticFamilyFunctor on the class of reduced closed subspaces at the standard model 𝕜ⁿ; a term assigns to every triple of the class a CompatibleFamily, the finite blow-up sequence over each relatively compact open of the ambient, compatible under restriction up to empty blow-ups ([Wlo09, Definition 3.2.6]). Reducible, so that the predicates of family functors apply to its terms directly.

Equations

• Hironaka.Manifold.BEDanFam 𝕜 n = Hironaka.Manifold.AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Hironaka.Manifold.DomBEDan 𝕜

structure Hironaka.Manifold.BEDanFamStar (𝕜 : Type) [RCLike 𝕜] : Type (u + 1)

The embedded-desingularization functor in every dimension, with the ambient closed-embedding clause of [Wlo09, Theorem 2.0.2, (4)] (also [Wlo09, Theorem 3.5.1, (3)]): for a closed submanifold S ⊆ M of codimension s and the reduced ideal of Y ⊆ S, the value on U of the functor in dimension n is the restricted push-forward of the value on U ∩ S of the functor in dimension n − s (per-open predicate).

• fam (n : ℕ) : BEDanFam 𝕜 n

  The embedded desingularization functor in every dimension.

• closedEmbedding (n s : ℕ) : AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (self.fam n) (self.fam (n - s))

  [Wlo09, Theorem 2.0.2] (4), bullet 3: commutation with closed embeddings of ambient manifolds, per relatively compact open, through the functor of dimension n − s.

def Hironaka.Manifold.BEDanFamStar.IsEmbeddedDesing (𝕜 : Type) [RCLike 𝕜] (bed : BEDanFamStar 𝕜) : Prop

The clauses (1)–(6) of [Wlo09, Theorem 2.0.2]: bed is an embedded-desingularization functor — for every dimension n, every triple of the class and every relatively compact open U, the value ((bed.fam n).fam T hT).seqOn U hU satisfies, against the restricted ideal 𝓘 := (T|U).I: (1) the exceptional divisors totalTransformSeq i are snc and every centre has snc with them; (2′) no point of any centre maps under the composite into the image of the regularLocus of the closed subspace IdealSheaf.toAnalyticSpace 𝓘; (3) the ideal-theoretic final strict transform Ỹ := strictTransformSubspaceSeq 𝓘 (Fin.last _) is smooth (the IsNonsingular of its closed subspace) and at every point of its cosupport has a chart adapted to the cosupport (its codimension chosen at the point) which is an snc chart of the final exceptional divisors; (6) σ^* 𝓘 = 𝓘_Ỹ · 𝓘_Ẽ: at every point of the last stage the stalk of the pulled-back ideal is Ỹ's stalk times a monomial in the vanishing ideals of the exceptional components through the point, the exponents α chosen at the point (one exponent per irreducible component through x; see the module docstring); and, for every n, bed.fam n commutes with local analytic isomorphisms ([Wlo09, Theorem 2.0.2] (4) bullets 1–2). Clause (4)'s third bullet is the field closedEmbedding, clause (5) the value's compat. The hypothesis under which the theorems about local resolutions from an arbitrary bed are stated; the functor built in Hironaka.Resolution.Analytic.Wlo09.Assembly satisfies it (concreteBEDanFamStar_isEmbeddedDesing), which is the input of the main theorem exists_functorial_resolution.

Equations

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