The dimension cast: the functoriality clause across two models of propositionally equal

dimension

Kollár's proof of Theorem 36 increases the ambient dimension freely ("we are allowed to increase n anytime by taking a further embedding 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ") and reads the resolution of the padded embedding on the coordinate slice through the weak commutation with closed embeddings ([Kol07, Theorem 36, proof] and [Kol07, 34.4]). Here the slice is a bundled submanifold, modelled on 𝕜^{n' − (n' − n)}, while the piece is modelled on 𝕜ⁿ: the two dimensions are PROPOSITIONALLY equal (Nat.sub_sub_self), so the functoriality clause of IsEmbeddedDesing (CommutesWithLocalIsos, the commutation with smooth morphisms of [Kol07, 34.1], stated for two manifolds on ONE model) cannot be applied between them, and bed.fam k, bed.fam n are related only by substituting the variable k. This module provides the device once:

• BEDanFamStar.exists_diffeomorph_last_of_cast: for a variable k with hk : k = n, a diffeomorphism g : N' → N ACROSS the models 𝕜ⁿ, 𝕜ᵏ (Mathlib's Diffeomorph allows two models), ideals with I' = g^* I (IdealSheaf.pullback, two models) in the empty-divisor triples of the domain class of the functor, and relatively compact opens U' = g⁻¹(U): the final stages of the two values are diffeomorphic OVER g (the square through the open inclusions and the composite blow-downs), and the final ideal-theoretic strict transforms (strictTransformSubspaceSeq) correspond under the diffeomorphism. The statement is cross-model; its proof is subst hk, after which g is a same-model diffeomorphism and the functoriality clause applies verbatim — the value on U' is the pull-back of the value on g(U') = U along g|_{U'} with the empty blow-ups deleted — then strictTransformSubspaceSeq_last_pullback_eraseEmpty for the strict transforms and the last-stage lift of a bijective local isomorphism as a diffeomorphism (pullbackLiftLastDiffeomorphOfBijective). It is applied at k := n' − (n' − n) by instantiating the variable, never by a subst at a compound term.
• BlowUpSequence.exists_diffeomorph_last_of_pullback_eraseEmpty: the same-model content — the diffeomorphism pullbackLiftLast ∘ eraseEmptyLast⁻¹ of the last stages of (L.pullback h).eraseEmpty and L over the bijective h, its square (stageMap_last_pullbackLiftLast, stageMap_last_eraseEmptyLast) and the strict-transform identity (strictTransformSubspaceSeq_last_pullback_eraseEmpty).

Not in the sources; bookkeeping on the functoriality clause and the transports of StrictSubspaceSeqTransport.lean. The padding whose slice is compared here is Włodarczyk's passage to a common ambient dimension [Wlo09, §7.1].

theorem AnalyticManifold.BlowUpSequence.exists_diffeomorph_last_of_pullback_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N N' : AnalyticManifold 𝕜 E} (g : N'.carrier → N.carrier) {U : TopologicalSpace.Opens N.carrier} {U' : TopologicalSpace.Opens N'.carrier} (L : BlowUpSequence ψ₀ (N.restrict U)) (h : AnalyticMap (N'.restrict U') (N.restrict U)) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hb : Function.Bijective ⇑h) (hsq : ∀ (p : (N'.restrict U').carrier), (N.inclusion U) (h p) = g ((N'.inclusion U') p)) (J : (N.restrict U).IdealSheaf) (J' : (N'.restrict U').IdealSheaf) (hJ' : J' = Manifold.IdealSheaf.pullback ⇑h ⋯ J) : ∃ (G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((L.pullback h hh).eraseEmpty.stage (Fin.last (L.pullback h hh).eraseEmpty.length)).carrier (L.stage (Fin.last L.length)).carrier ⊤), (∀ (p : ((L.pullback h hh).eraseEmpty.stage (Fin.last (L.pullback h hh).eraseEmpty.length)).carrier), (N.inclusion U) (L.toSuccession.composite (G p)) = g ((N'.inclusion U') ((L.pullback h hh).eraseEmpty.toSuccession.composite p))) ∧ (L.pullback h hh).eraseEmpty.toSuccession.strictTransformSubspaceSeq J' (Fin.last (L.pullback h hh).eraseEmpty.toSuccession.length) = Manifold.IdealSheaf.pullback ⇑G ⋯ (L.toSuccession.strictTransformSubspaceSeq J (Fin.last L.toSuccession.length))

The same-model content of the dimension cast (the pull-back of a blow-up sequence and the deletion of its empty blow-ups, [Kol07, Definition 30.1] and [Kol07, 34.1]): for a bijective local analytic isomorphism h : N'|U' → N|U lying over g and a list L over N|U, the last stages of (L.pullback h).eraseEmpty and of L are diffeomorphic through pullbackLiftLast ∘ eraseEmptyLast⁻¹, over g (the composites commute with the lifts, stageMap_last_pullbackLiftLast, stageMap_last_eraseEmptyLast), and the final strict transforms correspond under the diffeomorphism (strictTransformSubspaceSeq_last_pullback_eraseEmpty).

theorem Hironaka.Manifold.BEDanFamStar.exists_diffeomorph_last_of_cast {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (hcomm : ∀ (m : ℕ), AnalyticFamilyFunctor.CommutesWithLocalIsos (bed.fam m)) {k n : ℕ} (hk : k = n) {N : AnalyticManifold 𝕜 (Fin k → 𝕜)} {N' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) N'.carrier N.carrier ⊤) (I : N.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (I' : N'.IdealSheaf) (hI' : Manifold.IdealSheaf.IsNonzeroEverywhere I') (hII' : I' = Manifold.IdealSheaf.pullback ⇑g ⋯ I) (hT : DomBEDan 𝕜 { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ }) (hT' : DomBEDan 𝕜 { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ }) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) (U' : TopologicalSpace.Opens N'.carrier) (hU' : IsCompact (closure ↑U')) (hUU' : ↑U' = ⇑g ⁻¹' ↑U) : ∃ (G : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').stage (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').length)).carrier ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).stage (Fin.last (((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).length)).carrier ⊤), (∀ (p : ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').stage (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').length)).carrier), (N.inclusion U) ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.composite (G p)) = g ((N'.inclusion U') ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.composite p))) ∧ (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.strictTransformSubspaceSeq (I'.restrict U') (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.length) = Manifold.IdealSheaf.pullback ⇑G ⋯ ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (I.restrict U) (Fin.last (((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.length))

The dimension cast (Kollár's free enlargement of the ambient dimension and the commutation of the resolution with smooth morphisms, [Kol07, Theorem 36, proof] and [Kol07, 34.1]; Włodarczyk's common ambient dimension [Wlo09, §7.1]): for a family functor that commutes with local analytic isomorphisms in every dimension, and a diffeomorphism g : N' → N between a manifold modelled on 𝕜ⁿ and one modelled on 𝕜ᵏ with k = n PROPOSITIONALLY (the slice of a padding: k = n' − (n' − n)), whose ideals correspond (I' = g^* I, the triples with the empty divisor), the final stages of the values on corresponding relatively compact opens U' = g⁻¹(U) are diffeomorphic over g, and the final ideal-theoretic strict transforms correspond under the diffeomorphism. The statement is cross-model (Diffeomorph and IdealSheaf.pullback allow two models); the proof is subst hk, the functoriality clause (whose IsPullbackOf is ⟨hII', empty_comap⟩), and BlowUpSequence.exists_diffeomorph_last_of_pullback_eraseEmpty at h := g|_{U'}.