Lemma 102 (2): commutation with surjective local analytic isomorphisms

Clause (2) of [Kol07, Lemma 102] says that BD_{n,m,j} commutes with smooth morphisms; its proof reads that the functoriality of BD_{n,m,j}(X, I, E) follows "from the corresponding functoriality properties" of BMO_{n-1,m}(S, I_0|_S, E_S). For a surjective local analytic isomorphism h : N → M (the analytic counterpart of a smooth surjection), pulling back by h and restricting to h^{-1}(E^j) is the same as restricting to E^j and pulling back by the restriction of h, so the value of the input on the restricted triple pulls back (BMOanData.commutesWithLocalIsos), hence so does its push-forward, and the first blow-up pulls back since Z_{-1} does (BD.Zminus1_comap).

The identification of the pull-back of a pushed-forward list with the push-forward of the pulled-back list along the restricted map, BlowUpSequence.pushforward_pullback, enters here as the hypothesis PushforwardPullback ψ₀; it is supplied in BDErase.lean, where the clause is stated unconditionally (BDan_pullback_of_surjective).

The first centre of the pulled-back data is only propositionally the preimage of the first centre (BD.Zminus1_comap), and likewise the transform of E^j; the dependent types are handled by reading BDan.core over an arbitrary closed hypersurface Z and an arbitrary hypersurface S' of its blow-up, with the identifications Z = Z_{-1}, S' = S_0 as hypotheses (core_eq_of_eq, a substitution: the core over the input's value on restrictedTripleOf).

• PushforwardPullback ψ₀ — the identification as a hypothesis.
• BDan.bmoClass_restrictedTripleOf, BDan.core_eq_of_eq, BDan.core_congr — the core over an arbitrary Z and S' (BDan.restrictedTripleOf, BD.lean).
• HypersurfaceFamily.emptyMember_comap — emptying a member commutes with the inverse image.
• BDan.restrictedTripleOf_isPullbackOf — the restricted triple of the pulled-back data is the pull-back of the restricted triple along the restriction of h (the proof of [Kol07, Lemma 102]: pulling back by h and then restricting to E^j_Y gives "the same result" as restricting to E^j and then pulling back by h|_{E^j_Y}).
• BDan.core_pullback_of_surjective_of_pushforwardPullback, BDan_pullback_of_surjective_of_pushforwardPullback — the clause for the core and for BDan, given the identification.

def Hironaka.Manifold.PushforwardPullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] (ψ : E ≃L[𝕜] Fin n → 𝕜) : Prop

The pull-back along a local analytic isomorphism g of the push-forward of a list of centres on a closed hypersurface S is the push-forward, on g^{-1}(S), of the pull-back of the list along the restriction of g to g^{-1}(S) → S; as a hypothesis on the model (it is BlowUpSequence.pushforward_pullback, supplied in BDErase.lean). The proof of [Kol07, Lemma 102] uses it when it pulls back the pushed-forward sequence.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.HypersurfaceFamily.emptyMember_comap {M N : Type u} (F : HypersurfaceFamily M) (h : N → M) (j : F.ι) : (comap h F).emptyMember j = comap h (F.emptyMember j)

Emptying the member j commutes with the inverse image of a family.

The core over an arbitrary closed hypersurface

theorem Hironaka.Manifold.BDan.bmoClass_restrictedTripleOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) : Manifold.AnalyticTriple.BMOClass s (restrictedTripleOf T s j hZ hS' hT hZeq hSeq)

The restricted triple over Z and S' lies in the marked class BMOClass s.

theorem Hironaka.Manifold.BDan.core_eq_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (inp : BMOanData 𝕜 (n - 1) s) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) : core T s j inp hT = coreOfListOf hZ hS' (inp.functor.seq (restrictedTripleOf T s j hZ hS' hT hZeq hSeq) ⋯)

BDan.core read over any closed hypersurface Z = Z_{-1} and any hypersurface S' = S_0 of its blow-up (a substitution): the core over the input's value on restrictedTripleOf.

theorem Hironaka.Manifold.BDan.core_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (s : ℕ) (inp : BMOanData 𝕜 (n - 1) s) {T₁ T₂ : Manifold.AnalyticTriple ψ₀ M} (e : T₁ = T₂) (j₁ : T₁.F.ι) (j₂ : T₂.F.ι) (hj : j₁ ≍ j₂) (h₁ : BDClass s T₁) (h₂ : BDClass s T₂) : core T₁ s j₁ inp h₁ = core T₂ s j₂ inp h₂

The core respects equality of triples, with the member index and the proof of membership in the class transported.

The restricted triple of the pulled-back data

theorem Hironaka.Manifold.BDan.preimage_liftStep_transformS {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh ⋯) ⁻¹' transformS T s j = transformSOf (T.pullback h hh) j ⋯

The transform of h^{-1}(E^j) under the blow-up of h^{-1}(Z_{-1}) is the preimage, under the lift of h to the blow-ups, of the transform S_0 of E^j.

theorem Hironaka.Manifold.BDan.weakTransformIOf_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : weakTransformIOf (T.pullback h hh) ⋯ = Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh ⋯) ⋯ (weakTransformI T s j)

The weak transform of h^* 𝓘 under the blow-up of h^{-1}(Z_{-1}) is the pull-back of I_0 along the lift of h to the blow-ups.

theorem Hironaka.Manifold.BDan.boundaryMinusOf_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : boundaryMinusOf (T.pullback h hh) j ⋯ = Manifold.HypersurfaceFamily.comap (⇑(AnalyticManifold.BlowUpSequence.liftStep h hh ⋯)) (boundaryMinus T s j)

The family E - E^j of the pulled-back data, pulled back along the blow-up of h^{-1}(Z_{-1}), is the pull-back along the lift of h of the family (E - E^j)|_{X_0}.

theorem Hironaka.Manifold.BDan.restrictedTripleOf_isPullbackOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hT : BDClass s T) (hT' : BDClass s (T.pullback h hh)) : (restrictedTripleOf (T.pullback h hh) s j ⋯ ⋯ hT' ⋯ ⋯).IsPullbackOf (restrictedTriple T s j hT) (⋯.restrictMap ⋯ ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh ⋯) ⋯ ⋯)

The proof of [Kol07, Lemma 102] (pulling back by h and then restricting to E^j_Y gives "the same result" as restricting to E^j and then pulling back by h|_{E^j_Y}): the restricted triple of the pulled-back data, over h^{-1}(Z_{-1}) and the preimage of S_0 under the lift of h, is the pull-back of the restricted triple along the restriction of the lift of h to the hypersurfaces (BD.pullback_inclusionMap_pullback, BD.comap_inclusionMap_comap).

theorem Hironaka.Manifold.BDan.core_pullback_of_surjective_of_pushforwardPullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hpp : PushforwardPullback ψ₀) (inp : BMOanData 𝕜 (n - 1) s) (hs : Function.Surjective ⇑h) (hT : BDClass s T) (hT' : BDClass s (T.pullback h hh)) : core (T.pullback h hh) s j inp hT' = (core T s j inp hT).pullback h hh

[Kol07, Lemma 102 (2)] for the core at the mark s, along a surjective local analytic isomorphism h, given the identification PushforwardPullback: the core of the pulled-back data is the pull-back of the core. The first centre pulls back by BD.Zminus1_comap; the pushed-forward tail pulls back by the identification and by the commutation of the input functor with the restriction of the lift of h, a surjective local analytic isomorphism between the restricted triples (restrictedTripleOf_isPullbackOf).

theorem Hironaka.Manifold.BDan_pullback_of_surjective_of_pushforwardPullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (hpp : PushforwardPullback ψ₀) (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) (hT : Manifold.AnalyticTriple.BOClass m T) (hT' : Manifold.AnalyticTriple.BOClass m (T.pullback h hh)) (j : T.F.ι) : BDan m inp (T.pullback h hh) hT' j = (BDan m inp T hT j).pullback h hh

[Kol07, Lemma 102 (2)], the first bullet of [Kol07, 34.1], given the identification PushforwardPullback: BD_{n,m,j} commutes with surjective local analytic isomorphisms. It is the clause for the core at the tuned triple, tuning commuting with pull-back (AnalyticTriple.tuned_pullback).