The core over a sequence under pull-back and under deletion of empty blow-ups

Three general facts about the core over a sequence coreOfListOf (BDFamTransport.lean), the core of Lemma 102 over an arbitrary sequence of centres on the transform of E^j:

• coreOfListOf_pullback_eraseEmpty — it pulls back along a local analytic isomorphism to the core over the pulled-back sequence on the pulled-back data, up to the deletion of empty blow-ups (the functoriality of the construction, the proof of [Kol07, Lemma 102 (2)]; the deletion of empty blow-ups commutes with pull-back, BlowUpSequence.eraseEmpty_pullback_eraseEmpty, and so does the push-forward, BlowUpSequence.pushforward_pullback);
• coreOfListOf_eraseEmpty — it does not see the empty blow-ups of the sequence (BlowUpSequence.eraseEmpty_pushforward_eraseEmpty);
• coreOfListOf_congr — it depends only on the sets of the centre and of the transform, the transform being given as the preimage of a fixed hypersurface under the blowing-up.

These carry the compatibility and the commutation clauses of BDanFam (BDFamCompat.lean, BDFamComm.lean).

theorem Hironaka.Manifold.BDan.coreOfListOf_pullback_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS'.toAnalyticManifold) (ρ : AnalyticMap N M) (hρ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ) : ((coreOfListOf hZ hS' L).pullback ρ hρ).eraseEmpty = coreOfListOf ⋯ ⋯ (L.pullback (⋯.restrictMap hS' ⇑(AnalyticManifold.BlowUpSequence.liftStep ρ hρ hZ) ⋯ ⋯) ⋯)

The pull-back of the core over a sequence along a local analytic isomorphism ρ, with its empty blow-ups deleted, is the core over the sequence pulled back along the restricted lift of ρ to the transforms, on the pulled-back centre and transform (the functoriality in the proof of [Kol07, Lemma 102 (2)]).

theorem Hironaka.Manifold.BDan.coreOfListOf_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS'.toAnalyticManifold) : coreOfListOf hZ hS' L.eraseEmpty = coreOfListOf hZ hS' L

The core over a sequence does not see the empty blow-ups of the sequence: deleting them commutes with the push-forward (BlowUpSequence.eraseEmpty_pushforward_eraseEmpty).

theorem Hironaka.Manifold.BDan.coreOfListOf_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {C H Z₁ Z₂ : Set M.carrier} (hZ₁ : Manifold.IsClosedSubmanifold ψ₀ Z₁ 1) (hZ₂ : Manifold.IsClosedSubmanifold ψ₀ Z₂ 1) {S₁ : Set (Manifold.blowUp ψ₀ hZ₁).carrier} {S₂ : Set (Manifold.blowUp ψ₀ hZ₂).carrier} (hS₁ : Manifold.IsClosedSubmanifold ψ₀ S₁ 1) (hS₂ : Manifold.IsClosedSubmanifold ψ₀ S₂ 1) (hZeq₁ : Z₁ = C) (hZeq₂ : Z₂ = C) (hSeq₁ : S₁ = ⇑(Manifold.blowUpπ ψ₀ hZ₁) ⁻¹' H) (hSeq₂ : S₂ = ⇑(Manifold.blowUpπ ψ₀ hZ₂) ⁻¹' H) (L₁ : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS₁.toAnalyticManifold) (L₂ : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS₂.toAnalyticManifold) (hL : L₁ ≍ L₂) : coreOfListOf hZ₁ hS₁ L₁ = coreOfListOf hZ₂ hS₂ L₂

The core over a sequence depends only on the sets of the centre and of the transform (given as the preimage of a fixed hypersurface H under the blowing-up) and on the sequence.

theorem Hironaka.Manifold.BDan.heq_pullback_of_heq_bundled {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 E} {c : ℕ} {A : AnalyticManifold 𝕜 (Fin (n - c) → 𝕜)} {S₁ S₂ : Set X.carrier} (e : S₁ = S₂) (h₁ : Manifold.IsClosedSubmanifold ψ₀ S₁ c) (h₂ : Manifold.IsClosedSubmanifold ψ₀ S₂ c) (Z : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - c) → 𝕜)) A) (f₁ : AnalyticMap h₁.toAnalyticManifold A) (f₂ : AnalyticMap h₂.toAnalyticManifold A) (hf₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ ⇑f₁) (hf₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) ⊤ ⇑f₂) (hf : ∀ (x : X.carrier) (hx₁ : x ∈ S₁) (hx₂ : x ∈ S₂), f₁ ⟨x, hx₁⟩ = f₂ ⟨x, hx₂⟩) : Z.pullback f₁ hf₁ ≍ Z.pullback f₂ hf₂

Pull-backs of a sequence along maps out of the bundled closed submanifolds of two equal sets, agreeing pointwise, are equal (as heterogeneous equality, the two domains being equal only propositionally).

theorem Hironaka.Manifold.BDan.coreOfListOf_pullback_pullback_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) {A B : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (X : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) A) (a : AnalyticMap B A) (ha : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) ⊤ ⇑a) (b : AnalyticMap hS'.toAnalyticManifold B) (hb : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) ⊤ ⇑b) : coreOfListOf hZ hS' ((X.eraseEmpty.pullback a ha).pullback b hb) = coreOfListOf hZ hS' ((X.pullback a ha).pullback b hb)

The core over a sequence does not see the empty blow-ups of the sequence when two pull-backs are interposed (the two-step form of coreOfListOf_eraseEmpty).