Documentation

Hironaka.Resolution.Analytic.Wlo09.Concrete

The concrete embedded desingularization functor #

The embedded desingularization functor of this library, assembled from concrete inputs. The modified marked resolution concreteBMOmodFam in every dimension is built by the construction BMOmodFamOfInput_of_hid of Włodarczyk's modified algorithm (the proof of [Wlo09, Theorem 7.4.1]) from the concrete order-reduction families concreteBOanFam and concreteBMOanFam of the standard tower (OrderReduction/Stage/Concrete.lean) and the transform identity nonmonomialTransformIdentity_refl; it commutes with closed embeddings of empty divisor at every codimension (concreteBMOmodFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam: the codimension-one case of [Wlo09, §7.1], chained along a flag of hypersurfaces as in [Kol07, 108]); and the all-dimensions embedded desingularization functor concreteBEDanFamStar is BEDanFamStarOfInput at these data (Hironaka/Resolution/Analytic/Wlo09/Functoriality.lean), with the clauses of [Wlo09, Theorem 2.0.2] (concreteBEDanFamStar_isEmbeddedDesing, the assembly of Hironaka/Resolution/Analytic/Wlo09/Assembly.lean).

This is the functor from which the resolution of analytic spaces exists_functorial_resolution is assembled (Hironaka/Resolution/Analytic/Kol07Thm45/ResolutionAssembly.lean).

source
noncomputable def Hironaka.concreteBMOmodFam (K : Type) [RCLike K] (n : ℕ) :
Manifold.BMOmodFam K n

The modified marked resolution in every dimension (the construction BMOmodFamOfInput_of_hid of the proof of [Wlo09, Theorem 7.4.1]) at the concrete order-reduction families concreteBOanFam and concreteBMOanFam of the standard tower and the transform identity nonmonomialTransformIdentity_refl.

Equations
Instances For
    source
    theorem Hironaka.concreteBMOmodFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam (K : Type) [RCLike K] (n s : ℕ) :
    (concreteBMOmodFam K n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (concreteBMOmodFam K (n - s)).functor

    concreteBMOmodFam commutes with closed embeddings of empty divisor at every codimension s: the codimension-one commutation of BMOmodFamOfInput_of_hid (resolving (M, I, ∅, 1) commutes with embeddings of the ambient manifold, [Wlo09, §7.1]) chained along a flag of hypersurfaces (BMOmodFam_commutesWithClosedEmbeddingsOfEmptyDivisorFam_all of Functor/ChainClosedEmbeddingZero.lean, the reduction to the hypersurface case as in [Kol07, 108]).

    source
    noncomputable def Hironaka.concreteBEDanFamStar (K : Type) [RCLike K] :
    Manifold.BEDanFamStar K

    The concrete embedded desingularization functor in all dimensions: BEDanFamStarOfInput at concreteBMOmodFam.

    Equations
    Instances For
      source
      theorem Hironaka.concreteBEDanFamStar_isEmbeddedDesing (K : Type) [RCLike K] :
      Manifold.BEDanFamStar.IsEmbeddedDesing K (concreteBEDanFamStar K)

      concreteBEDanFamStar is an embedded desingularization: the clauses of [Wlo09, Theorem 2.0.2], by the assembly BEDanFamStarOfInput_isEmbeddedDesing.