Lemma 102 in the compatible-family form: the order clause and clause (1)

The two clauses of [Kol07, Lemma 102] about the sequence itself, for the value BDanFam on a relatively compact open U (BDFam.lean): it is a smooth blow-up sequence of order m starting with the restricted triple (BDanFam_isOfOrder), and at its end the strict transform of E^j misses cosupp(I_r, m) (BDanFam_cosupp_disjoint, clause (1)). By coreFamOn_eq_coreOfListOf (BDFamTransport.lean) the core on U is the core over the input's value transported to the restricted data, so the clauses are those of the core over a sequence (Hironaka/Resolution/Analytic/OrderReduction/BD.lean) once the input family's clauses on its open are transported along the two local analytic isomorphisms of the transport, the bundle diffeomorphism and the restricted lift, and the restricted triple of the restricted data is identified with the pull-back of the restricted triple along the composite (restrictedTripleOf_restrict_eq; the proof of Lemma 102: restricting and pulling back commute). The clauses hold first at the mark s = tuningParam m for the tuned triple, on which BDanFam runs, and are carried back to (𝓘, m) by orderReduction_tuned_iff and ord_lt_of_tuned (TunedLemmas.lean), as for BDan in BDCore.lean and BDCosupp.lean.

• Zminus1_restrict, transformSU_eq — the centre and the transform of the restricted data are the restrictions of Z_{-1} and S_0;
• noEmptyCenters_transportedValue, isOfOrderGe_transportedValue, ord_lt_transportedValue — the transported value inherits the input's three properties;
• coreFamOn_isOfOrderGe, coreFamOn_cosupp_disjoint — the clauses for the core on U;
• BDanFam_isOfOrder, BDanFam_cosupp_disjoint — the clauses for the value of BD_{n,m,j} on U.

These are the isOfOrder and cosupp_disjoint fields of Lemma 102's family data bdanFamDataOfInput in BOanFamOfInput.lean.

theorem Hironaka.Manifold.BDan.Zminus1_restrict {𝕜 : 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 : TopologicalSpace.Opens M.carrier) : ⇑(M.inclusion U) ⁻¹' BD.Zminus1 T.I s (T.F.hyp j) = BD.Zminus1 (T.pullback (M.inclusion U) ⋯).I s ((T.pullback (M.inclusion U) ⋯).F.hyp j)

The centre of the restricted data is the restriction of Z_{-1} (BD.Zminus1_comap for the inclusion of U).

theorem Hironaka.Manifold.BDan.transformSU_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 : TopologicalSpace.Opens M.carrier) : ⇑(liftIncl T s j U) ⁻¹' ⇑((Manifold.blowUp ψ₀ ⋯).inclusion (piOpen T s j U)) ⁻¹' transformS T s j = transformSOf (T.pullback (M.inclusion U) ⋯) j ⋯

The transform of E^j in the restricted blowing-up is the transform of the restricted data.

theorem Hironaka.Manifold.BDan.noEmptyCenters_transportedValue {𝕜 : 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.ι) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (transportedValue T s j inp hT U hU).NoEmptyCenters

The transported value has no empty centres: it is the input's value, which has none, pulled back twice along surjective local analytic isomorphisms.

theorem Hironaka.Manifold.BDan.inclusion_comp_bundleInv_comp_liftInclS {𝕜 : 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 : TopologicalSpace.Opens M.carrier) : (ContMDiffMap.comp (⋯.toAnalyticManifold.inclusion (⋯.preimageOpens (piOpen T s j U))) (bundleInv T s j U)).comp (liftInclS T s j U) = ⋯.restrictMap ⋯ ⇑(AnalyticManifold.BlowUpSequence.liftStep (M.inclusion U) ⋯ ⋯) ⋯ ⋯

The composite of the two transport maps followed by the inclusion of the trace is the restriction of the lift of the inclusion to the transforms of E^j (equal on the underlying points).

theorem Hironaka.Manifold.BDan.restrictedTripleOf_restrict_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.ι) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hT' : BDClass s (T.pullback (M.inclusion U) ⋯)) : restrictedTripleOf (T.pullback (M.inclusion U) ⋯) s j ⋯ ⋯ hT' ⋯ ⋯ = (((restrictedTriple T s j hT).pullback (⋯.toAnalyticManifold.inclusion (⋯.preimageOpens (piOpen T s j U))) ⋯).pullback (bundleInv T s j U) ⋯).pullback (liftInclS T s j U) ⋯

The restricted triple of the restricted data is the pull-back of the restricted triple of T along the composite transport map ("we get the same result" whether one first pulls back or first restricts, the proof of [Kol07, Lemma 102]; restrictedTripleOf_isPullbackOf).

theorem Hironaka.Manifold.BDan.ord_lt_last_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M) (m : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hge : L.toSuccession.IsOfOrderGe T'.I m T'.F.idealSheaf) (hlt : ∀ (y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier), Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq T'.I m (Fin.last L.toSuccession.length)) y < ↑m) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (y' : ↑↧((L.pullback h hh).toSuccession.stage (Fin.last (L.pullback h hh).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((L.pullback h hh).toSuccession.markedTransformSeq (T'.pullback h hh).I m (Fin.last (L.pullback h hh).toSuccession.length)) y' < ↑m

The clause "the controlled transform at the last stage has order < m" pulls back along a local analytic isomorphism: the controlled transform of the pull-back at the last stage is the pull-back of the controlled transform along the last lift, and the order is read at the image.

theorem Hironaka.Manifold.BDan.isOfOrderGe_transportedValue {𝕜 : 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.ι) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hT' : BDClass s (T.pullback (M.inclusion U) ⋯)) : (transportedValue T s j inp hT U hU).toSuccession.IsOfOrderGe (restrictedTripleOf (T.pullback (M.inclusion U) ⋯) s j ⋯ ⋯ hT' ⋯ ⋯).I s (restrictedTripleOf (T.pullback (M.inclusion U) ⋯) s j ⋯ ⋯ hT' ⋯ ⋯).F.idealSheaf

The transported value is a smooth blow-up sequence of order ≥ s for the restricted triple of the restricted data: the input family's clause on its open, pulled back twice.

theorem Hironaka.Manifold.BDan.ord_lt_transportedValue {𝕜 : 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.ι) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hT' : BDClass s (T.pullback (M.inclusion U) ⋯)) (y : ↑↧((transportedValue T s j inp hT U hU).toSuccession.stage (Fin.last (transportedValue T s j inp hT U hU).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((transportedValue T s j inp hT U hU).toSuccession.markedTransformSeq (restrictedTripleOf (T.pullback (M.inclusion U) ⋯) s j ⋯ ⋯ hT' ⋯ ⋯).I s (Fin.last (transportedValue T s j inp hT U hU).toSuccession.length)) y < ↑s

The controlled transform of the transported value at the last stage has order < s everywhere: the input family's clause on its open, pulled back twice.

theorem Hironaka.Manifold.BDan.coreFamOn_isOfOrderGe {𝕜 : 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.ι) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hT' : BDClass s (T.pullback (M.inclusion U) ⋯)) : (coreFamOn T s j inp hT U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The order clause for the core on U at the mark s: it is a smooth blow-up sequence of order ≥ s for the restricted triple (coreOfListOf_isOfOrderGe at the transported value).

theorem Hironaka.Manifold.BDan.coreFamOn_cosupp_disjoint {𝕜 : 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.ι) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hT' : BDClass s (T.pullback (M.inclusion U) ⋯)) : Disjoint {x : ↑↧((coreFamOn T s j inp hT U hU).toSuccession.stage (Fin.last (coreFamOn T s j inp hT U hU).toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((coreFamOn T s j inp hT U hU).toSuccession.weakTransformSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (coreFamOn T s j inp hT U hU).toSuccession.length)) x} ((coreFamOn T s j inp hT U hU).toSuccession.strictTransformSeq ((T.pullback (M.inclusion U) ⋯).F.hyp j) (Fin.last (coreFamOn T s j inp hT U hU).toSuccession.length))

Clause (1) of [Kol07, Lemma 102] for the core on U at the mark s: the strict transform of E^j at the end misses cosupp(I_r, s) (coreOfListOf_cosupp_disjoint at the transported value).

theorem Hironaka.Manifold.bdClass_tuned_pullback_inclusion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens M.carrier) : BDan.BDClass (IsLocalRing.tuningParam m) ((T.tuned m ⋯).pullback (M.inclusion U) ⋯)

The tuned triple restricted to U lies in the class of the core (the tuning commutes with the restriction, tuned_pullback).

theorem Hironaka.Manifold.BDanFam_isOfOrder {𝕜 : 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 : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (BDanFam m inp T hT j U hU).toSuccession.IsOfOrder (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F.idealSheaf m

The order clause of [Kol07, Lemma 102] ("a smooth blow-up sequence functor BD_{n,m,j} of order m") for the value on U: BDanFam m inp T hT j U hU is a smooth blow-up sequence of order exactly m starting with the restricted triple. The core's clause at the mark s = tuningParam m on the tuned triple is carried back to (𝓘, m) by orderReduction_tuned_iff; the order is exactly m because ord 𝓘 ≤ m everywhere.

theorem Hironaka.Manifold.BDanFam_cosupp_disjoint {𝕜 : 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 : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Disjoint {x : ↑↧((BDanFam m inp T hT j U hU).toSuccession.stage (Fin.last (BDanFam m inp T hT j U hU).toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord ((BDanFam m inp T hT j U hU).toSuccession.weakTransformSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (BDanFam m inp T hT j U hU).toSuccession.length)) x} ((BDanFam m inp T hT j U hU).toSuccession.strictTransformSeq ((T.pullback (M.inclusion U) ⋯).F.hyp j) (Fin.last (BDanFam m inp T hT j U hU).toSuccession.length))

Clause (1) of [Kol07, Lemma 102], "cosupp(I_r, m) ∩ Π^{-1}_*(E^j) = ∅", for the value on U: the strict transform of E^j at the end of BDanFam m inp T hT j U hU misses cosupp(I_r, m). The core's clause at the mark s = tuningParam m on the tuned triple is carried back to (𝓘, m) by ord_lt_of_tuned.