Lemma 102 in the compatible-family form: compatibility under restriction

The values of BD_{n,m,j} on the relatively compact open subsets (BDanFam, BDFam.lean) form a compatible family: for U ≤ V the value on U is the pull-back of the value on V along the open inclusion with its empty blow-ups deleted (BDanFam_compat; the compatibility clause of [Wlo09, Theorem 2.0.3 (4)] with [Wlo09, Definition 3.2.6], and the second clause of [Kol07, 34.1] for the open embedding U ⊆ V). Both sides are cores over transported values (coreFamOn_eq_coreOfListOf, coreOfListOf_pullback_eraseEmpty): the centres and the transforms agree as sets, because the lift of U ⊆ V ⊆ M to the blowings-up is the composite of the lifts (uniqueness of lifts, eq_of_comm_blowUp), and the transported values are the input family's values at the traces U_S ≤ V_S, identified by the family's own compatibility and the behaviour of the core over a sequence under pull-back (BDFamPullback.lean).

• piOpen_mono, preimageOpens_piOpen_mono — π_{-1}^{-1} and the trace on S_0 are monotone;
• liftStep_inclusion_eq_comp, transformSU_pullback_eq — the lifts compose, and the transform of E^j pulls back to the transform of the restricted data;
• coreFamOn_compat, BDanFam_compat — the compatibility for the core on an open and for the value of BD_{n,m,j}.

This is the compat field of the compatible family bdanFam in BOanFamOfInput.lean.

theorem Hironaka.Manifold.BDan.piOpen_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : piOpen T s j U ≤ piOpen T s j V

π_{-1}^{-1} is monotone on open sets.

theorem Hironaka.Manifold.BDan.preimageOpens_piOpen_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : ⋯.preimageOpens (piOpen T s j U) ≤ ⋯.preimageOpens (piOpen T s j V)

The trace on S_0 of π_{-1}^{-1} is monotone on open sets.

theorem Hironaka.Manifold.BDan.liftStep_inclusion_eq_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : ⇑(AnalyticManifold.BlowUpSequence.liftStep (M.inclusion U) ⋯ ⋯) = ⇑(AnalyticManifold.BlowUpSequence.liftStep (M.inclusion V) ⋯ ⋯) ∘ ⇑(AnalyticManifold.BlowUpSequence.liftStep (M.restrictLE hUV) ⋯ ⋯)

The lift of the inclusion U ⊆ M to the blowings-up is the lift of V ⊆ M after the lift of U ⊆ V (uniqueness of lifts, eq_of_comm_blowUp).

theorem Hironaka.Manifold.BDan.transformSU_pullback_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : ⇑(AnalyticManifold.BlowUpSequence.liftStep (M.restrictLE hUV) ⋯ ⋯) ⁻¹' ⇑(liftIncl T s j V) ⁻¹' ⇑((Manifold.blowUp ψ₀ ⋯).inclusion (piOpen T s j V)) ⁻¹' transformS T s j = ⇑(Manifold.blowUpπ ψ₀ ⋯) ⁻¹' ⇑(M.inclusion U) ⁻¹' T.F.hyp j

The transform of E^j pulled back along the lift of U ⊆ V is the transform of the data restricted to U.

theorem Hironaka.Manifold.BDan.coreFamOn_compat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) : coreFamOn T s j inp hT U hU = ((coreFamOn T s j inp hT V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The core on an open is compatible under restriction: for U ≤ V the core on U is the pull-back of the core on V along the open inclusion with its empty blow-ups deleted (the second clause of [Kol07, 34.1]; [Wlo09, Theorem 2.0.3 (4)]). Both cores are cores over transported values on the same centre and transform; the transported values agree because the input family is compatible at the traces U_S ≤ V_S and the lift of U ⊆ M is the lift of V ⊆ M after the lift of U ⊆ V.

theorem Hironaka.Manifold.BDanFam_compat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (inp : BMOanFam 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) {U V : TopologicalSpace.Opens M.carrier} (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : BDanFam m inp T hT j U hU = ((BDanFam m inp T hT j V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The values of BD_{n,m,j} on the relatively compact open subsets are compatible under restriction ([Wlo09, Theorem 2.0.3 (4)]; the second clause of [Kol07, 34.1]): for U ≤ V the value on U is the pull-back of the value on V along the open inclusion with its empty blow-ups deleted. This is coreFamOn_compat at the tuned triple.