Step 1 of Theorem 103: transfer between the triple and its tuned triple

Step 1 of the proof of [Kol07, Theorem 103] replaces I by the maximal coefficient ideal W_s(I) ([Kol07, Definition 98]), for which order reduction is "equivalent to order reduction for (X, W(I), E)" ([Kol07, Corollary 101]). This module proves what the construction needs about the tuned triple of Tuned.lean:

• comap_tuning — the tuning commutes with pull-back along a local analytic isomorphism, h^*(W_s(J)) = W_s(h^* J). Stalkwise: the stalk of the pull-back is the image of the stalk under the germ algebra isomorphism, the stalk of W_s(J) is Kollár's sum ∑_{wt(e) ≥ s} ∏_j (D^j J)^{e_j}, the image of an ideal under a ring isomorphism distributes over sums, products and powers, and the derivative ideal sheaves commute with the pull-back ([Kol07, Lemma 74 (4)]).
• AnalyticTriple.tuned_pullback — the tuned triple of a pull-back is the pull-back of the tuned triple.
• AnalyticTriple.orderReduction_tuned_iff — Kollár's equivalence: a sequence of centres is a smooth blow-up sequence of order ≥ s for the tuned triple iff it is one of order ≥ m for the triple (tuning_orderReduction_equiv; the boundary is kept by the tuning).
• AnalyticTriple.ord_lt_of_tuned — the output clause transfers back: where the final transform of W_s(𝓘) has order < s, the final transform of 𝓘 has order < m. Along a sequence of order ≥ m for (𝓘, m) (of order ≥ s for (W_s(𝓘), s) by the equivalence) the controlled transforms are the weak transforms, because every centre has order exactly m, respectively s; the controlled transform of W_s(𝓘) lies in the tuning of the controlled transform of 𝓘 (markedTransformSeq_tuning_le), whose order is ≥ s exactly where the transform of 𝓘 has order ≥ m; and a smaller ideal sheaf has a larger order. So ord W_r < s forces ord I_r < m.

These lemmas carry Theorem 103 (1) and (2) from the tuned triple back to the triple for the local functor in the compatible-family form (LocalFunctorFam.lean).

theorem Hironaka.Manifold.comap_tuning {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (m s : ℕ) : Manifold.IdealSheaf.pullback ⇑h ⋯ (Manifold.IdealSheaf.tuning J m s) = (Manifold.IdealSheaf.pullback ⇑h ⋯ J).tuning m s

The tuning commutes with pull-back along a local analytic isomorphism, h^*(W_s(J)) = W_s(h^* J) ([Kol07, Definition 98] with [Kol07, Lemma 74 (4)]): stalkwise, Kollár's sum is carried by the germ algebra isomorphism term by term. Not in the sources; the ingredient of the functoriality of Step 1.

theorem Manifold.AnalyticTriple.tuned_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} {N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (hm : 1 ≤ m) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : (T.pullback h hh).tuned m hm = (T.tuned m hm).pullback h hh

The tuned triple of a pull-back along a local analytic isomorphism is the pull-back of the tuned triple (comap_tuning): Step 1 of the proof of [Kol07, Theorem 103] commutes with local analytic isomorphisms.

theorem Manifold.AnalyticTriple.orderReduction_tuned_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (T : AnalyticTriple ψ₀ M) (hT : BOClass m T) (L : AnalyticManifold.BlowUpSequence ψ₀ M) : L.toSuccession.IsOfOrderGe (T.tuned m ⋯).I (IsLocalRing.tuningParam m) (T.tuned m ⋯).F.idealSheaf ↔ L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf

Order reduction for (X, I, E) "is equivalent to order reduction for (X, W(I), E)" (Step 1 of the proof of [Kol07, Theorem 103]; [Kol07, Corollary 101]): a sequence of centres is a smooth blow-up sequence of order ≥ s for the tuned triple iff it is one of order ≥ m for the triple, s = tuningParam m (tuning_orderReduction_equiv; the boundary is kept by the tuning).

theorem Manifold.AnalyticTriple.ord_lt_of_tuned {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (T : AnalyticTriple ψ₀ M) (hT : BOClass m T) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) (x : (L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier) (hx : IdealSheaf.ord (L.toSuccession.weakTransformSeq (T.tuned m ⋯).I (Fin.last L.toSuccession.length)) x < ↑(IsLocalRing.tuningParam m)) : IdealSheaf.ord (L.toSuccession.weakTransformSeq T.I (Fin.last L.toSuccession.length)) x < ↑m

The output clause of Theorem 103 transfers from the tuned triple back to the triple: where the final transform of W_s(𝓘) has order < s, the final transform of 𝓘 has order < m. Along the sequence the controlled transforms are the weak transforms; the controlled transform of W_s(𝓘) lies in the tuning of the controlled transform of 𝓘 (markedTransformSeq_tuning_le), whose order is ≥ s exactly where the transform of 𝓘 has order ≥ m (le_ord_tuning_iff).