The embedded desingularization functor in every dimension

The all-dimensions embedded desingularization functor BEDanFamStarOfInput bmod hbmod: the functors bedanFamOfInput bmod n of Hironaka/Resolution/Analytic/Wlo09/Basic.lean in every dimension n, together with the commutation with closed embeddings of the ambient manifold that clause (4) of [Wlo09, Theorem 2.0.2] requires, which is proved from the corresponding commutation hbmod of the modified marked resolution bmod.

• AnalyticFamilyFunctor.CommutesWithLocalIsos.restrictDomain and AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam.restrictDomain: the two functoriality predicates descend from a family functor B on a class Dom to any family functor B₀ on a sub-class Dom₀ ⊆ Dom that agrees with B there; the triples and their class proofs are hypotheses of both predicates, so the descent is the transport of the agreements.
• bedanFamOfInput_commutesWithClosedEmbeddings bmod hbmod n s: the embedded desingularization in dimension n commutes with closed embeddings of empty divisor through the one in dimension n − s, the restriction of hbmod n s to the class DomBEDan ⊆ BMOClass 1 (DomBEDan.bmoClass_one).
• BEDanFamStarOfInput bmod hbmod : BEDanFamStar 𝕜: the functors of every dimension with the closed-embedding field; BEDanFamStarOfInput_fam: the dimension-wise functors unfolded (rfl).

Why the field holds. Resolving (M', I', ∅, 1) for a closed embedding M ↪ M' of ambient manifolds is equivalent to resolving (M, I, ∅, 1) [Wlo09, §7.1]: the coordinates u₁, …, u_k of M in M' define tangent directions of I', the algorithm passes to the hypersurface V(u₁) and repeats k times (this is clause (3) of [Wlo09, Theorem 3.5.1] for the canonical resolution of marked ideals). That commutation is a property of the modified marked resolution bmod, taken here as the hypothesis hbmod (proved for the concrete resolution in Hironaka/Resolution/Analytic/Wlo09/Concrete.lean). The embedded desingularization is the restriction of that resolution to the class DomBEDan, so the commutation descends: the predicate's triples and their class proofs are its own hypotheses, and bedanFamOfInput bmod n agrees with (bmod n).functor on the class by definition.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.CommutesWithLocalIsos.restrictDomain {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom Dom₀ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} {B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} {B₀ : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₀} (h : ∀ {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M}, Dom₀ T → Dom T) (hB₀ : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₀ T), B₀.fam T hT = B.fam T ⋯) (hB : B.CommutesWithLocalIsos) : B₀.CommutesWithLocalIsos

The predicate CommutesWithLocalIsos descends to a sub-class: if B commutes with local analytic isomorphisms on Dom and B₀ on Dom₀ ⊆ Dom agrees with B there, then B₀ commutes with local analytic isomorphisms. Not in the sources; bookkeeping.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam.restrictDomain {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom Dom₀ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} {B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} {B₀ : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₀} {s : ℕ} {Dom' Dom₀' : {M' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} → Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M' → Prop} {B' : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} => Dom'} {B₀' : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} => Dom₀'} (h : ∀ {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M}, Dom₀ T → Dom T) (h' : ∀ {M' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M'}, Dom₀' T' → Dom' T') (hB₀ : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₀ T), B₀.fam T hT = B.fam T ⋯) (hB₀' : ∀ {M' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M') (hT' : Dom₀' T'), B₀'.fam T' hT' = B'.fam T' ⋯) (hB : B.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B') : B₀.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B₀'

The predicate CommutesWithClosedEmbeddingsOfEmptyDivisorFam descends to sub-classes: if B commutes with closed embeddings of empty divisor through B' and B₀, B₀' agree with B, B' on the sub-classes Dom₀ ⊆ Dom, Dom₀' ⊆ Dom', then B₀ commutes with closed embeddings of empty divisor through B₀'. Not in the sources; bookkeeping.

theorem Hironaka.Manifold.bedanFamOfInput_commutesWithClosedEmbeddings (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (hbmod : ∀ (n s : ℕ), (bmod n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmod (n - s)).functor) (n s : ℕ) : AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bedanFamOfInput 𝕜 bmod n) (bedanFamOfInput 𝕜 bmod (n - s))

The embedded desingularization in dimension n commutes with closed embeddings of empty divisor through the one in dimension n − s (the embeddings of ambient manifolds in clause (4) of [Wlo09, Theorem 2.0.2]; [Wlo09, §7.1]): the restriction to the class DomBEDan ⊆ BMOClass 1 (DomBEDan.bmoClass_one) of the commutation hbmod n s of the modified marked resolution. The larger functors (bmod n).functor, (bmod (n - s)).functor are passed by name, since the predicate's hypothesis alone does not determine them for the unifier.

def Hironaka.Manifold.BEDanFamStarOfInput (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (hbmod : ∀ (n s : ℕ), (bmod n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmod (n - s)).functor) : BEDanFamStar 𝕜

The embedded desingularization functor in every dimension ([Wlo09, Theorem 2.0.2], with the commutation with embeddings of ambient manifolds of its clause (4), [Wlo09, §7.1] and [Wlo09, Theorem 3.5.1 (3)]), from a modified marked resolution bmod : ∀ n, BMOmodFam 𝕜 n in every dimension and its commutation hbmod with closed embeddings of empty divisor. The dimension-wise functors are bedanFamOfInput bmod n by definition, and the closed-embedding field is bedanFamOfInput_commutesWithClosedEmbeddings, the restriction of hbmod n s to the class DomBEDan ⊆ BMOClass 1.

Equations

• Hironaka.Manifold.BEDanFamStarOfInput 𝕜 bmod hbmod = { fam := fun (n : ℕ) => Hironaka.Manifold.bedanFamOfInput 𝕜 bmod n, closedEmbedding := ⋯ }

theorem Hironaka.Manifold.BEDanFamStarOfInput_fam (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (hbmod : ∀ (n s : ℕ), (bmod n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmod (n - s)).functor) (n : ℕ) : (BEDanFamStarOfInput 𝕜 bmod hbmod).fam n = bedanFamOfInput 𝕜 bmod n

The dimension-wise functors of BEDanFamStarOfInput, unfolded (rfl).