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

Clause (2) of [Kol07, Lemma 102], commutation with smooth morphisms, has two parts in [Kol07, 34.1]: the functor commutes with smooth surjections, and along an arbitrary smooth morphism its value at the pull-back is the pull-back of its value with the empty blow-ups deleted. This module completes the first for BDan, the analytic BD_{n,m,j}, once the identification BlowUpSequence.pushforward_pullback of the pull-back of a pushed-forward list with the push-forward of the pulled-back list is available (Hironaka/Manifold/FiniteSuccession/Functor/PushforwardPullback.lean); both parts in the compatible-family form are BDanFam_commutesWithLocalIsos (BDFamComm.lean).

• pushforwardPullback — the identification, so that BDan_pullback_of_surjective (the first bullet, BDOf.lean) holds outright.
• AnalyticTriple.bmoClass_pullback — the marked class is closed under pull-back along local analytic isomorphisms (a nonempty pulled-back member comes from a nonempty member).

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

The pull-back along a local analytic isomorphism of the push-forward of a list of centres on a closed hypersurface is the push-forward of the pull-back along the restricted map: BlowUpSequence.pushforward_pullback at codimension one (which proof of local analyticity is given for the restricted map does not matter).

theorem Manifold.AnalyticTriple.bmoClass_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {s : ℕ} {T : AnalyticTriple ψ M} (hT : BMOClass s T) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : BMOClass s (T.pullback g hg)

The marked class BMOClass s is closed under pull-back along local analytic isomorphisms: a member of the pulled-back boundary is nonempty only if the member it comes from is.

theorem Hironaka.Manifold.BDan_pullback_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (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]: BD_{n,m,j} commutes with surjective local analytic isomorphisms — BDan_pullback_of_surjective_of_pushforwardPullback with the identification pushforwardPullback supplied.