Documentation

Hironaka.Resolution.Analytic.ModelTransport.Principalization

Włodarczyk's principalization and its functoriality along the re-modelling #

The clauses of Włodarczyk's locally finite principalization [Wlo09, Theorem 2.0.3] and of its commutation with local analytic isomorphisms carry over from a compatible family over the re-modelled manifold M.transport ψ (the standard model 𝕜ⁿ, where the resolution family resolveFam lives) to the family read back on M (ExtensionCompatibleFamily.transportBack, Hironaka/Resolution/Analytic/ModelTransport/Family.lean):

Analytic maps between the re-modelled manifolds #

source
def AnalyticManifold.AnalyticMap.transport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M N : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (g : AnalyticMap N M) :
AnalyticMap (N.transport ψ) (M.transport ψ)

An analytic map g : N → M read between the re-modelled manifolds N.transport ψ and M.transport ψ: the same map on points, analytic as M.transportDiffeomorph ψ ∘ g ∘ (N.transportDiffeomorph ψ)⁻¹.

Equations
Instances For
    source
    theorem AnalyticManifold.AnalyticMap.transport_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M N : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (g : AnalyticMap N M) (x : N.carrier) :
    (transport ψ g) (N.toTransport ψ x) = M.toTransport ψ (g x)

    The re-modelled map is the map on points.

    source
    theorem AnalyticManifold.AnalyticMap.isLocalDiffeomorph_transport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M N : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') {g : AnalyticMap N M} (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) :
    IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E') ⊤ ⇑(transport ψ g)

    The re-modelled map of a local analytic isomorphism is a local analytic isomorphism: a composite of g with the two identities, which are analytic isomorphisms across the models.

    source
    theorem AnalyticManifold.IdealSheaf.transport_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M N : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (g : AnalyticMap N M) (J : M.IdealSheaf) :
    transport ψ (Manifold.IdealSheaf.pullback ⇑g ⋯ J) = Manifold.IdealSheaf.pullback ⇑(AnalyticMap.transport ψ g) ⋯ (transport ψ J)

    The re-modelled pull-back is the pull-back of the re-modelled ideal sheaf along the re-modelled map (both are the pull-back of J along the same map on points).

    The pull-back predicate along the re-modelling #

    source
    theorem AnalyticManifold.FiniteSuccession.IsPullbackUpToEmptyAlong.transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M N : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') {U : TopologicalSpace.Opens M.carrier} {U' : TopologicalSpace.Opens N.carrier} {S : ((M.transport ψ).restrict (M.transportOpens ψ U)).FiniteSuccession} {R : ((N.transport ψ).restrict (N.transportOpens ψ U')).FiniteSuccession} (g : AnalyticMap N M) (gT : AnalyticMap (N.transport ψ) (M.transport ψ)) (hg : ∀ (x : N.carrier), gT (N.toTransport ψ x) = M.toTransport ψ (g x)) (h : R.IsPullbackUpToEmptyAlong S gT) :
    (FiniteSuccession.transportAlong (N.restrictTransportDiffeomorph ψ U') ψ.symm R).IsPullbackUpToEmptyAlong (FiniteSuccession.transportAlong (M.restrictTransportDiffeomorph ψ U) ψ.symm S) g

    Włodarczyk's pull-back up to empty blow-ups [Wlo09, Theorem 3.5.1 (2)] carries back from the re-modelled manifolds: if the succession R over an open U' of N.transport ψ is the pull-back of the succession S over an open U of M.transport ψ along the re-modelled map gT of g, then the successions carried back to N and M (transportAlong at the identities of the opens) are related in the same way along g. The block index is kept and every lift is conjugated by the stage identifications of the two transports.

    The principalization clauses along the re-modelling #

    source
    theorem AnalyticManifold.ExtensionCompatibleFamily.isLocallyFinitelyPrincipalizedBy_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (I : M.IdealSheaf) (h : (IdealSheaf.transport ψ I).IsLocallyFinitelyPrincipalizedBy F) :
    I.IsLocallyFinitelyPrincipalizedBy (transportBack ψ F)

    The clauses of Włodarczyk's principalization (IdealSheaf.IsLocallyFinitelyPrincipalizedBy, [Wlo09, Theorem 2.0.3 (1)–(3)]) carry over from the family F over the re-modelled M and the re-modelled ideal sheaf to the family read back on M and the ideal sheaf: the properness, the divisor clause on M̃ and the isomorphism off the support by the global transport lemmas of Family.lean; the centres and the boundaries by their transport lemmas per compact; and the monomial clause (3) by IsMulBoundaryMonomial.pullbackDiffeomorph along the stage identification of the last stage, which carries the pull-back of the ideal sheaf (pullbackDiffeomorph_comap), the unit ideal and the last exceptional divisor (boundarySeq_seq_transportBack) to those of F.