Transports along a diffeomorphism of two models; the last-stage lift of a diffeomorphism

The independence of the resolution of a piece from its embedding [Kol07, Theorem 36, proof] compares the local resolutions for two embeddings by passing through the coordinate slice of a padded embedding (Kollár's enlargement 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ of the ambient space and the weak commutation with closed embeddings [Kol07, 34.4]; Włodarczyk's common ambient dimension [Wlo09, §7.1]). The slice, read as a bundled submanifold (IsClosedSubmanifold.toAnalyticManifold, modelled on 𝕜^{n' − (n' − n)}), is diffeomorphic to the piece (modelled on 𝕜ⁿ) ACROSS MODELS — the two dimensions are propositionally, not definitionally, equal — so the transports of ideal-sheaf data that the comparison needs are stated here for a diffeomorphism g : M' → M between manifolds on ANY two models E', E:

• IdealSheaf.isReduced_pullback_diffeomorph, IdealSheaf.isNonzeroEverywhere_pullback_diffeomorph: the germ map of a diffeomorphism is a ring isomorphism of stalks (germMap_bijective_of_diffeomorph, the two-model form of germMap_bijective_of_isLocalDiffeomorphAt), and the pull-back's stalks are its images (IdealSheaf.stalkIdeal_pullback), so radical ideals and nonzero ideals transport. They supply the hypotheses DomBEDan and IsNonzeroEverywhere for the slice triple.
• IdealSheaf.pullback_symm_pullback: pulling back along g⁻¹ and then along g is the identity — the two-model form of the same-model IdealSheaf.pullback_pullback_symm (TransportBase.lean), by pullback_pullback, pullback_congr and pullback_id_eq_self, all of which already admit two models.
• isCompact_closure_preimage_diffeomorph: relatively compact opens pull back to relatively compact opens (a homeomorphism).
• The pull-back along h of a blow-up sequence is the fibre product X_i ×_X Y [Kol07, Definition 30.1], whose projections are injective when h is — injective_liftStep, BlowUpSequence.injective_pullbackLiftLast, the injective counterparts of surjective_liftStep and surjective_pullbackLiftLast (Kollár's printed remark concerns a surjective h; the injective case is immediate from the definition of the pull-back); hence the last-stage lift of a BIJECTIVE local analytic isomorphism is a diffeomorphism, BlowUpSequence.pullbackLiftLastDiffeomorphOfBijective (Mathlib's IsLocalDiffeomorph.toDiffeomorphOfBijective; the map restrictMap g U' (imageOpens g hg U') produced by the functoriality clause of IsEmbeddedDesing is the case used), and BlowUpSequence.pullbackLiftLastDiffeomorph for a diffeomorphism g, with their coercion lemmas coe_….

Not in the sources; routine transports along the pull-back of ideal sheaves and the lift of a local isomorphism to a blow-up sequence.

Transports along a diffeomorphism of two models

theorem Hironaka.Manifold.germMap_bijective_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {M' : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (b : M'.carrier) : Function.Bijective ⇑(Manifold.germMap ⇑g ⋯ b)

The germ map of a diffeomorphism of two models is bijective (the two-model form of germMap_bijective_of_isLocalDiffeomorphAt): the germ map of the inverse, read at g b through g⁻¹(g b) = b, is a two-sided inverse.

theorem Manifold.IdealSheaf.pullback_symm_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {M' : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (J : M'.IdealSheaf) : pullback ⇑g ⋯ (pullback ⇑g.symm ⋯ J) = J

Pulling back along g⁻¹ and then along g is the identity: the two-model form of IdealSheaf.pullback_pullback_symm (TransportBase.lean), which is this statement at g⁻¹ for a same-model diffeomorphism.

theorem Manifold.IdealSheaf.isReduced_pullback_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {M' : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) {J : M.IdealSheaf} (hJ : J.IsReduced) : AnalyticManifold.IdealSheaf.IsReduced (pullback ⇑g ⋯ J)

Reducedness of an ideal sheaf transports along a diffeomorphism of two models: the pull-back's stalks are the images of the stalks under the ring isomorphisms germMap, and a radical ideal maps to a radical ideal under a surjective ring homomorphism with trivial kernel (Ideal.map_radical_of_surjective).

theorem Manifold.IdealSheaf.isNonzeroEverywhere_pullback_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {M' : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) {J : M.IdealSheaf} (hJ : IsNonzeroEverywhere J) : (pullback ⇑g ⋯ J).IsNonzeroEverywhere

Nonvanishing at every stalk transports along a diffeomorphism of two models: the image of a nonzero ideal under an injective ring homomorphism is nonzero (Ideal.map_eq_bot_iff_of_injective).

theorem Hironaka.Manifold.isCompact_closure_preimage_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {M' : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) {U : Set M.carrier} (hU : IsCompact (closure U)) : IsCompact (closure (⇑g ⁻¹' U))

The preimage of a relatively compact open under a diffeomorphism is relatively compact (a homeomorphism carries closures to closures and compact sets to compact sets).

The last-stage lift of a diffeomorphism

theorem AnalyticManifold.BlowUpSequence.injective_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hi : Function.Injective ⇑h) : Function.Injective ⇑(liftStep h hh hY)

The lift of an injective local analytic isomorphism to the blowings-up is injective (injective_blowUpLift; the fibre product X₁ ×_X Y of [Kol07, Definition 30.1]) — the counterpart of surjective_liftStep.

theorem AnalyticManifold.BlowUpSequence.injective_pullbackLiftLast {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Function.Injective ⇑h → Function.Injective ⇑(L.pullbackLiftLast h hh)

The last-stage lift of an injective local analytic isomorphism is injective, by the list recursion of surjective_pullbackLiftLast (immediate from the definition of the pull-back of a blow-up sequence [Kol07, Definition 30.1], whose printed remark concerns a surjective h).

noncomputable def AnalyticManifold.BlowUpSequence.pullbackLiftLastDiffeomorphOfBijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hb : Function.Bijective ⇑h) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier (L.stage (Fin.last L.length)).carrier ⊤

The last-stage lift of a BIJECTIVE local analytic isomorphism, as a diffeomorphism ([Kol07, Definition 30.1]): pullbackLiftLast is a bijective local analytic isomorphism (isLocalDiffeomorph_pullbackLiftLast, injective_pullbackLiftLast, surjective_pullbackLiftLast), hence a diffeomorphism by Mathlib's IsLocalDiffeomorph.toDiffeomorphOfBijective. This is the form in which the functoriality clause of IsEmbeddedDesing is used: h is restrictMap g U' (imageOpens g hg U'), onto its image and injective when g is.

Equations

• L.pullbackLiftLastDiffeomorphOfBijective h hh hb = ⋯.toDiffeomorphOfBijective ⋯

theorem AnalyticManifold.BlowUpSequence.coe_pullbackLiftLastDiffeomorphOfBijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hb : Function.Bijective ⇑h) : ⇑(L.pullbackLiftLastDiffeomorphOfBijective h hh hb) = ⇑(L.pullbackLiftLast h hh)

The diffeomorphism of pullbackLiftLastDiffeomorphOfBijective is the lift on points (definitional).

noncomputable def AnalyticManifold.BlowUpSequence.pullbackLiftLastDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((L.pullback g.toAnalyticMap ⋯).stage (Fin.last (L.pullback g.toAnalyticMap ⋯).length)).carrier (L.stage (Fin.last L.length)).carrier ⊤

The last-stage lift of a diffeomorphism, as a diffeomorphism ([Kol07, Definition 30.1]): pullbackLiftLastDiffeomorphOfBijective at g read as an analytic map.

Equations

• L.pullbackLiftLastDiffeomorph g = L.pullbackLiftLastDiffeomorphOfBijective g.toAnalyticMap ⋯ ⋯

theorem AnalyticManifold.BlowUpSequence.coe_pullbackLiftLastDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) : ⇑(L.pullbackLiftLastDiffeomorph g) = ⇑(L.pullbackLiftLast g.toAnalyticMap ⋯)

The diffeomorphism is the lift on points (definitional).