The modified first step: the modified core commutes with local analytic isomorphisms

The functoriality argument in the proof of [Kol07, Lemma 102] (the restriction of a smooth surjection to the member is again a smooth surjection, and pull-back and restriction commute) for the modified first step of [Wlo09, Theorem 7.4.1]: for a local analytic isomorphism g : N → M and the pulled-back triple g^*T, the modified core of g^*T on a relatively compact open U' is the modified core of T on g(U') pulled back along g|_{U'}, up to empty blow-ups. This is the counterpart of BDan.coreFamOn_commutesWithLocalIsos without the first blow-up.

The argument, step by step:

• the stopped locus and H⁺ pull back (hplus_pullback: H⁺(g^*T) = g⁻¹(H⁺(T)), by BD.Zminus1_comap: a component of g⁻¹(E^j) lies in cosupp(g^*𝓘, 1) iff the component of E^j it maps into lies in cosupp(𝓘, 1));
• the restricted triple of g^*T on g⁻¹(H⁺) is the pull-back of the restricted triple of T along the restriction g|_{H⁺} : g⁻¹(H⁺) → H⁺ (restrictedTripleModOf_isPullbackOf: pullback_inclusionMap_pullback for the ideal, emptyMember_comap for the boundary), itself a local analytic isomorphism (IsClosedSubmanifold.isLocalDiffeomorph_restrictMap);
• the functor R one dimension down commutes with it (its commutation with local isomorphisms, a hypothesis here) at the trace U' ∩ g⁻¹(H⁺), whose image is the trace g(U') ∩ H⁺ (imageOpens_hplusRestrictMap_preimageOpens);
• the push-forward on each open commutes with the pull-back along g|_{U'} ([Kol07, Definition 30, 30.3]; PushforwardStage.pushforwardAux_pullback at the two restriction stages, the general form of pushforwardRestrict_pullback_restrictLE: pushforwardRestrict_pullback_restrictMap), and the deletions of empty blow-ups commute with both.

The transport from H⁺(g^*T) to the propositionally equal g⁻¹(H⁺(T)) reads the constructions on an arbitrary closed hypersurface S with S = H⁺ (restrictedTripleModOf, coreModOn_eq_of_eq, as coreFamOn_eq_of_eq does).

Generic tools: the per-open push-forward under a local analytic isomorphism

theorem Manifold.IsClosedSubmanifold.image_restrictMap_preimageOpens_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : IsClosedSubmanifold ψ S s) (g : AnalyticMap N M) (hS' : IsClosedSubmanifold ψ (⇑g ⁻¹' S) s) {U' : TopologicalSpace.Opens N.carrier} {W : TopologicalSpace.Opens M.carrier} (hUW : ⇑g '' ↑U' ⊆ ↑W) : ⇑(hS'.restrictMap hS ⇑g ⋯ ⋯) '' ↑(hS'.preimageOpens U') ⊆ ↑(hS.preimageOpens W)

The restriction g|_{g⁻¹(S)} : g⁻¹(S) → S maps the trace U' ∩ g⁻¹(S) into the trace W ∩ S when g(U') ⊆ W.

theorem AnalyticManifold.BlowUpSequence.pushforwardRestrict_pullback_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S s) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hS' : Manifold.IsClosedSubmanifold ψ (⇑g ⁻¹' S) s) (U' : TopologicalSpace.Opens N.carrier) (W : TopologicalSpace.Opens M.carrier) (hUW : ⇑g '' ↑U' ⊆ ↑W) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.toAnalyticManifold.restrict (hS.preimageOpens W))) : (pushforwardRestrict hS W L).pullback (Hironaka.Manifold.AnalyticMap.restrictMap g U' W hUW) ⋯ = pushforwardRestrict hS' U' (L.pullback (Hironaka.Manifold.AnalyticMap.restrictMap (hS'.restrictMap hS ⇑g ⋯ ⋯) (hS'.preimageOpens U') (hS.preimageOpens W) ⋯) ⋯)

The push-forward on each open commutes with the pull-back along a local analytic isomorphism g|_{U'} : U' → W (g(U') ⊆ W), as in the proof of [Kol07, Lemma 102] with the push-forward of [Kol07, Definition 30, 30.3]: pushforwardAux_pullback at the two restriction stages, the square being g|_{U'} ∘ (U' ∩ g⁻¹(S) ⊆ U') = (W ∩ S ⊆ W) ∘ g|_{g⁻¹(S)}. The general form of pushforwardRestrict_pullback_restrictLE.

theorem Hironaka.Manifold.CompatibleFamily.pullback_restrictMap_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {A B : AnalyticManifold 𝕜 E} {X : Manifold.AnalyticTriple ψ A} (C : CompatibleFamily X) (f : AnalyticMap B A) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (V : TopologicalSpace.Opens B.carrier) {W W' : TopologicalSpace.Opens A.carrier} (e : W = W') (hW : IsCompact (closure ↑W)) (hW' : IsCompact (closure ↑W')) (h1 : ⇑f '' ↑V ⊆ ↑W) (h2 : ⇑f '' ↑V ⊆ ↑W') : (C.seqOn W hW).pullback (AnalyticMap.restrictMap f V W h1) ⋯ = (C.seqOn W' hW').pullback (AnalyticMap.restrictMap f V W' h2) ⋯

Pull-backs of the values of a compatible family on two equal opens, along the restrictions of the same map, are equal (a substitution).

Commutation with a local analytic isomorphism

theorem Hironaka.Manifold.BMOmod.hplus_pullback {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : hplus (T.pullback g hg) j = ⇑g ⁻¹' hplus T j

The stopped locus and H⁺ pull back (Zminus1_comap; the functoriality argument in the proof of [Kol07, Lemma 102]): H⁺(g^*T) = g⁻¹(H⁺(T)).

theorem Hironaka.Manifold.BMOmod.isClosedSubmanifold_preimage_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (⇑g ⁻¹' hplus T j) 1

g⁻¹(H⁺) is a closed hypersurface of N (the preimage of a closed hypersurface under a local analytic isomorphism, preimage_of_isLocalDiffeomorph).

@[reducible, inline]

abbrev Hironaka.Manifold.BMOmod.hplusRestrictMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : AnalyticMap ⋯.toAnalyticManifold ⋯.toAnalyticManifold

The restriction g|_{H⁺} : g⁻¹(H⁺) → H⁺ (Kollár's h|_{E^j_Y} in the proof of [Kol07, Lemma 102]) between the bundled hypersurfaces.

Equations

• Hironaka.Manifold.BMOmod.hplusRestrictMap T j g hg = ⋯.restrictMap ⋯ ⇑g ⋯ ⋯

theorem Hironaka.Manifold.BMOmod.isLocalDiffeomorph_hplusRestrictMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) ⊤ ⇑(hplusRestrictMap T j g hg)

theorem Hironaka.Manifold.BMOmod.restrictedTripleModOf_isPullbackOf {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : (restrictedTripleModOf (T.pullback g hg) j ⋯ ⋯).IsPullbackOf (restrictedTripleMod T j) (hplusRestrictMap T j g hg)

The restricted triple of g^*T on g⁻¹(H⁺) is the pull-back of the restricted triple of T along g|_{H⁺} (pull-back and restriction commute, the proof of [Kol07, Lemma 102]): the ideal by pullback_inclusionMap_pullback, the boundary by emptyMember_comap (the trace of the pulled-back boundary is the pull-back of the trace, member by member).

theorem Hironaka.Manifold.BMOmod.imageOpens_hplusRestrictMap_preimageOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) : AnalyticMap.imageOpens (hplusRestrictMap T j g hg) ⋯ (⋯.preimageOpens U') = ⋯.preimageOpens (AnalyticMap.imageOpens g hg U')

The image under g|_{H⁺} of the trace U' ∩ g⁻¹(H⁺) is the trace g(U') ∩ H⁺.

theorem Hironaka.Manifold.BMOmod.coreModOn_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) (hT : Manifold.AnalyticTriple.BMOClass 1 T) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BMOClass 1 (T.pullback g hg)) (hRc : R.CommutesWithLocalIsos) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : coreModOn R (T.pullback g hg) j hT' U' hU' = ((coreModOn R T j hT (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

The modified core commutes with local analytic isomorphisms (the functoriality argument in the proof of [Kol07, Lemma 102]; [Wlo09, Theorem 7.4.1]; the counterpart of coreFamOn_commutesWithLocalIsos without the first blow-up): the modified core of g^*T on U' is the modified core of T on g(U') pulled back along g|_{U'}, with empty blow-ups deleted, given that the functor R one dimension down commutes with local analytic isomorphisms.

theorem Hironaka.Manifold.BMOmod.coreModFam_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) (hT : Manifold.AnalyticTriple.BMOClass 1 T) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BMOClass 1 (T.pullback g hg)) (hRc : R.CommutesWithLocalIsos) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : (coreModFam R (T.pullback g hg) j hT').seqOn U' hU' = (((coreModFam R T j hT).seqOn (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

coreModOn_commutesWithLocalIsos for the compatible family coreModFam (the shape the alignment of the links of the maximal-contact step takes).