Lemma 102 (1): the transform of E^j misses the cosupport

Clause (1) of [Kol07, Lemma 102]: at the end of BD_{n,m,j}(X, I, E), the birational transform of E^j is disjoint from cosupp(I_r, m). Kollár's argument: the birational transform of E^j at the end is the last stage S_r of the sequence restricted to S = E^j, and along S_r the order of I_r is read by the restricted transforms ([Kol07, Corollary 89]: S_r ∩ cosupp(I_r, m) is the intersection of the cosupports of the restricted transforms of (D^j I|_S, m - j), in particular contained in cosupp(I_r|_{S_r}, m)), which clause (1) of the input functor makes empty. On the manifold side the first blow-up π_{-1} has centre Z_{-1} ⊆ E^j, so the transform of E^j after it lies in S_0 = π_{-1}^{-1}(E^j); the later stages carry it inside the transforms of S_0, which are the images of the stages of the pushed-forward sequence. The whole is proved for the tuned triple (M, W_s(𝓘), E), s = tuningParam m, and carried back to (𝓘, m) by ord_lt_of_tuned, and the empty first blow-up is transported along its isomorphism.

• strictTransformSet_mono, FiniteSuccession.strictTransformSeq_mono — the strict transform is monotone in the hypersurface.
• FiniteSuccession.cosupp_disjoint_cons — the clause for a sequence from the clause for its tail.
• BlowUpSequence.strictTransformSet_preimage_liftStep, BlowUpSequence.strictTransformSeq_pullback — the strict transforms along the pull-back of a sequence are the preimages of the strict transforms along the lifts (local analytic isomorphisms are open maps, so preimages commute with closures).
• BlowUpSequence.cosupp_disjoint_of_pullback — the clause descends along a surjective local analytic isomorphism; BlowUpSequence.cosupp_disjoint_map_emptyBlowUp — its transport along the isomorphism of an empty blow-up.
• BDan.cosupp_disjoint_pushforward_toSuccession — the clause for the pushed-forward tail ([Kol07, Corollary 89] against the clause (1) of the input).
• BDan.coreOfListOf_cosupp_disjoint_of_bridge, BDan_cosupp_disjoint_of_bridge — Lemma 102 (1) for the core over a sequence and for BDan, given the identification PushforwardBridge ψ₀ of BDCore.lean (discharged in BDBridge.lean).

theorem Hironaka.Manifold.strictTransformSet_mono {M' M : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) {H H' : Set M} (h : H ⊆ H') : Manifold.strictTransformSet π Y H ⊆ Manifold.strictTransformSet π Y H'

The strict transform of a hypersurface is monotone in the hypersurface.

theorem AnalyticManifold.FiniteSuccession.strictTransformSeqAux_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H H' : Set M.carrier} (h : H ⊆ H') (i : ℕ) (hi : i < S.length + 1) : S.strictTransformSeqAux H i hi ⊆ S.strictTransformSeqAux H' i hi

The strict transforms along a succession are monotone in the hypersurface (indexed by a natural number with a bound).

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H H' : Set M.carrier} (h : H ⊆ H') (i : Fin (S.length + 1)) : S.strictTransformSeq H i ⊆ S.strictTransformSeq H' i

The strict transforms along a succession are monotone in the hypersurface.

theorem AnalyticManifold.FiniteSuccession.cosupp_disjoint_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (J : M.IdealSheaf) (H : Set M.carrier) (s : ℕ) (h : Disjoint {x : ↑↧(rest.stage (Fin.last rest.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord (rest.weakTransformSeq (IdealSheaf.weakTransform (Manifold.blowUpπ ψ hY) J hY.idealSheaf) (Fin.last rest.length)) x} (rest.strictTransformSeq (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ hY)) Y H) (Fin.last rest.length))) : Disjoint {x : ↑↧((cons ψ hY rest).stage (Fin.last (cons ψ hY rest).length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((cons ψ hY rest).weakTransformSeq J (Fin.last (cons ψ hY rest).length)) x} ((cons ψ hY rest).strictTransformSeq H (Fin.last (cons ψ hY rest).length))

The clause (1) of [Kol07, Lemma 102] for a sequence cons hY rest from the clause for rest: the cosupport of the last weak transform of J misses the last strict transform of H along the whole sequence when it does so along rest for the transforms of J and H under the first blow-up.

theorem AnalyticManifold.BlowUpSequence.strictTransformSet_preimage_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (H : Set M.carrier) : Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ ⋯)) (⇑h ⁻¹' Y) (⇑h ⁻¹' H) = ⇑(liftStep h hh hY) ⁻¹' Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hY)) Y H

The strict transform of h^{-1}(H) under the blow-up of h^{-1}(Y) is the preimage, along the lift of h to the blow-ups, of the strict transform of H under the blow-up of Y: the lift is a local analytic isomorphism, hence an open continuous map, so preimages commute with closures.

theorem AnalyticManifold.BlowUpSequence.strictTransformSeqAux_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (H : Set M.carrier) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1) : (L.pullback h hh).toSuccession.strictTransformSeqAux (⇑h ⁻¹' H) i hi' = ⇑(L.pullbackLiftAux h hh i hi hi') ⁻¹' L.toSuccession.strictTransformSeqAux H i hi

The strict transforms along the pull-back h^* L of a sequence are the preimages of the strict transforms along L under the lifts of h to the stages (indexed by a natural number with a bound).

theorem AnalyticManifold.BlowUpSequence.strictTransformSeq_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (H : Set M.carrier) (i : Fin (L.length + 1)) : (L.pullback h hh).toSuccession.strictTransformSeq (⇑h ⁻¹' H) ⟨↑i, ⋯⟩ = ⇑(L.pullbackLift h hh i) ⁻¹' L.toSuccession.strictTransformSeq H i

The strict transforms along the pull-back h^* L of a sequence are the preimages of the strict transforms along L under the lifts of h to the stages.

theorem AnalyticManifold.BlowUpSequence.cosupp_disjoint_of_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) (J : M.IdealSheaf) (H : Set M.carrier) (s : ℕ) (hL : Disjoint {x : ↑↧((L.pullback h hh).toSuccession.stage (Fin.last (L.pullback h hh).toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((L.pullback h hh).toSuccession.weakTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) (Fin.last (L.pullback h hh).toSuccession.length)) x} ((L.pullback h hh).toSuccession.strictTransformSeq (⇑h ⁻¹' H) (Fin.last (L.pullback h hh).toSuccession.length))) : Disjoint {y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord (L.toSuccession.weakTransformSeq J (Fin.last L.toSuccession.length)) y} (L.toSuccession.strictTransformSeq H (Fin.last L.toSuccession.length))

The clause (1) of [Kol07, Lemma 102] descends along a surjective local analytic isomorphism: if along h^* L the cosupport of the last weak transform of h^* J misses the last strict transform of h^{-1}(H), then along L the cosupport of the last weak transform of J misses the last strict transform of H. Every point of the last stage of L lifts to the last stage of h^* L (surjective_pullbackLift), the order is read at the lift (ord_pullback_of_isLocalDiffeomorphAt), and the strict transforms pull back (strictTransformSeq_pullback).

theorem AnalyticManifold.BlowUpSequence.cosupp_disjoint_map_emptyBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) (P : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) {J : M.IdealSheaf} {H : Set M.carrier} {s : ℕ} (hP : Disjoint {x : ↑↧(P.toSuccession.stage (Fin.last P.toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord (P.toSuccession.weakTransformSeq (Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ₀ hY) ⋯ J) (Fin.last P.toSuccession.length)) x} (P.toSuccession.strictTransformSeq (⇑(Manifold.blowUpπ ψ₀ hY) ⁻¹' H) (Fin.last P.toSuccession.length))) : Disjoint {x : ↑↧((map (emptyBlowUpDiffeomorph hY hY₀) P).toSuccession.stage (Fin.last (map (emptyBlowUpDiffeomorph hY hY₀) P).toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((map (emptyBlowUpDiffeomorph hY hY₀) P).toSuccession.weakTransformSeq J (Fin.last (map (emptyBlowUpDiffeomorph hY hY₀) P).toSuccession.length)) x} ((map (emptyBlowUpDiffeomorph hY hY₀) P).toSuccession.strictTransformSeq H (Fin.last (map (emptyBlowUpDiffeomorph hY hY₀) P).toSuccession.length))

Transport of the clause (1) of [Kol07, Lemma 102] along the isomorphism of an empty blow-up ([Kol07, 32]), as isOfOrderGe_map_emptyBlowUp: the transported sequence is the pull-back along the inverse isomorphism, and the clause descends along it (cosupp_disjoint_of_pullback).

theorem Hironaka.Manifold.BDan.cosupp_disjoint_pushforward_toSuccession {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hT : BDClass s T) (P : ⋯.toAnalyticManifold.FiniteSuccession) (hPge : P.IsOfOrderGe (restrictedTriple T s j hT).I s (restrictedTriple T s j hT).F.idealSheaf) (hPlt : ∀ (y : ↑↧(P.stage (Fin.last P.length)).carrier), Manifold.IdealSheaf.ord (P.markedTransformSeq (restrictedTriple T s j hT).I s (Fin.last P.length)) y < ↑s) : Disjoint {x : ↑↧((AnalyticManifold.FiniteSuccession.pushforward ⋯ P).stage (Fin.last (AnalyticManifold.FiniteSuccession.pushforward ⋯ P).length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((AnalyticManifold.FiniteSuccession.pushforward ⋯ P).weakTransformSeq (weakTransformI T s j) (Fin.last (AnalyticManifold.FiniteSuccession.pushforward ⋯ P).length)) x} ((AnalyticManifold.FiniteSuccession.pushforward ⋯ P).strictTransformSeq (transformS T s j) (Fin.last (AnalyticManifold.FiniteSuccession.pushforward ⋯ P).length))

The clause (1) of [Kol07, Lemma 102] for the pushed-forward tail (the proof of the lemma: "such that Π^{-1}_{r*}(E^j) is disjoint from cosupp(I_r, m)"): along the push-forward of a sequence P on S_0 of order ≥ s for the restricted triple, the cosupport {ord ≥ s} of the last weak transform of I_0 misses the last transform S_r of S_0. By [Kol07, Corollary 89] (setOf_le_ord_markedTransformSeq_pushforward_inter_eq_iInter) a point of S_r where the controlled transform of (I_0, s) has order ≥ s is one where the controlled transform of (I_0|_{S_0}, s) along P has order ≥ s, and the clause (1) of the input (BMOanData.ord_lt) admits no such point. Along the push-forward the controlled and the weak transforms agree, the sequence having order exactly s.

theorem Hironaka.Manifold.BDan.coreOfListOf_cosupp_disjoint_of_bridge {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hbr : PushforwardBridge ψ₀) (hT : BDClass s T) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold) (hLne : L.NoEmptyCenters) (hL : L.toSuccession.IsOfOrderGe (restrictedTriple T s j hT).I s (restrictedTriple T s j hT).F.idealSheaf) (hlt : ∀ (y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier), Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq (restrictedTriple T s j hT).I s (Fin.last L.toSuccession.length)) y < ↑s) : Disjoint {x : ↑↧((coreOfListOf ⋯ ⋯ L).toSuccession.stage (Fin.last (coreOfListOf ⋯ ⋯ L).toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((coreOfListOf ⋯ ⋯ L).toSuccession.weakTransformSeq T.I (Fin.last (coreOfListOf ⋯ ⋯ L).toSuccession.length)) x} ((coreOfListOf ⋯ ⋯ L).toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last (coreOfListOf ⋯ ⋯ L).toSuccession.length))

Clause (1) of [Kol07, Lemma 102] for the core over a sequence, given the identification of the two push-forwards: if L has no empty centres, is a smooth blow-up sequence of order ≥ s for the restricted triple and its controlled transform at the last stage has order < s everywhere, then the strict transform of E^j at the end of the core over L is disjoint from cosupp(I_r, s). The first blow-up carries the transform of E^j into S_0 = π_{-1}^{-1}(E^j) (strictTransform_subset_preimage), the pushed-forward tail keeps it inside S_r and away from the cosupport (cosupp_disjoint_pushforward_toSuccession), and when the first blow-up is empty the clause is transported along its isomorphism.

theorem Hironaka.Manifold.BDan_cosupp_disjoint_of_bridge {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (hbr : PushforwardBridge ψ₀) (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) : Disjoint {x : ↑↧((BDan m inp T hT j).toSuccession.stage (Fin.last (BDan m inp T hT j).toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord ((BDan m inp T hT j).toSuccession.weakTransformSeq T.I (Fin.last (BDan m inp T hT j).toSuccession.length)) x} ((BDan m inp T hT j).toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last (BDan m inp T hT j).toSuccession.length))

The clause (1) of [Kol07, Lemma 102], given the identification of the two push-forwards: the birational transform of E^j at the end of BD_{n,m,j}(M, 𝓘, E) misses the cosupport {ord I_r ≥ m} of the last weak transform of 𝓘. The clause for the tuned triple (M, W_s(𝓘), E) at the mark s = tuningParam m (coreOfListOf_cosupp_disjoint_of_bridge at the value of the input functor) is carried back to (𝓘, m) by ord_lt_of_tuned, in the contrapositive, along the sequence of order m (BDan_isOfOrder_of_bridge).