Lemma 102 on analytic manifolds: the construction of the functor BD

Kollár's Lemma 102 ([Kol07, Lemma 102]) is the first ingredient of order reduction for ideals: for a triple (X, I, E) with max-ord I ≤ m and a member E^j of the boundary, assuming order reduction for marked ideals in dimension n - 1, it produces a smooth blow-up sequence functor BD_{n,m,j} of order m after which the cosupport cosupp(I_r, m) is disjoint from the birational transform of E^j. Its proof first replaces I by the D-balanced ideal W_{m!}(I) ([Kol07, Corollary 101]; here W_s(𝓘) with s = tuningParam m, Tuned.lean) and then, with S := E^j, blows up the union Z_{-1} of the components of E^j contained in cosupp(I, m), restricts the weak transform I_0 and the boundary E - E^j to S, applies the marked functor BMO_{n-1,m} to the restricted triple and pushes the result forward ([Kol07, 30.3]): BD_{n,m,j}(X, I, E) := τ_* BMO_{n-1,m}(S, I_0|_S, m, E_S) ∘ π_{-1}. This module carries the construction out on analytic manifolds, in two layers as in the proof: a core on D-balanced triples, and the functor itself on the tuned triple.

• HypersurfaceFamily.emptyMember F j — Kollár's E - E^j, with the index set kept and the j-th member replaced by the empty hypersurface; IsSnc.emptyMember, and IsSnc.hasSncWithProper_emptyMember: the other members have simple normal crossings with E^j properly (at a point of E^j, the chart of the simple normal crossings has E^j as a coordinate hyperplane and the other members through the point on other coordinates).
• HypersurfaceFamily.HasSncWithProper.comap — proper simple normal crossings pull back along a local analytic isomorphism (the charts are transported along the local inverses).
• isLocalDiffeomorph_blowUpπ_of_codimOne — blowing up a hypersurface is a local analytic isomorphism ([Kol07, Warning 20]: a trivial blow-up is an isomorphism).
• BDan.BDClass s — the class of the core: the triples of BOClass s whose ideal sheaf is D-balanced at the mark s.
• BDan.transformS, BDan.weakTransformI, BDan.boundaryMinus, BDan.restrictedTriple — the transform S_0 = π_{-1}^{-1}(E^j) of E^j, the weak transform I_0 of 𝓘, the pulled-back E - E^j, and the triple (S_0, I_0|_{S_0}, (E - E^j)|_{S_0}) on the hypersurface S_0 regarded as a manifold modelled on 𝕜^{n-1}; its ideal sheaf is nonzero everywhere because I_0 is D-balanced, and its boundary has simple normal crossings as the trace of a family having proper simple normal crossings with S_0. It lies in the marked class BMOClass s. They are the instances at Z_{-1} of BDan.transformSOf, BDan.weakTransformIOf, BDan.boundaryMinusOf, BDan.restrictedTripleOf, over an arbitrary closed hypersurface Z (and S').
• BDan.coreOfListOf hZ hS' L — the core over a sequence: the blow-up of a closed hypersurface Z, followed by the push-forward of a sequence L on a closed hypersurface S' of the blow-up, with empty blow-ups deleted ([Kol07, 32]); BDan.core s T j inp hT — the core: coreOfListOf at Z_{-1} and S_0 over the value of the input functor inp : BMOanData 𝕜 (n - 1) s on the restricted triple (the first blow-up is empty when no component of E^j lies in cosupp(𝓘, s)).
• BDan m inp T hT j — the functor BD_{n,m,j} on the class BOClass m: the core at the mark s = tuningParam m on the tuned triple (M, W_s(𝓘), E) (Tuned.lean), the input being BMO_{n-1,s}.

The clauses of Lemma 102 for BDan — order m with respect to E, the disjointness (1) and the functoriality (2) — are proved in BDCore.lean, BDCosupp.lean, BDBridge.lean, BDOf.lean, BDErase.lean and BDIndiff.lean, and carried over to the compatible-family form of BDFam.lean, whose data bdanFamDataOfInput (BOanFamOfInput.lean) is the input of Steps 2.1 and 2.2 of the proof of Theorem 103.

The push-forward inside the core is the push-forward of a list of centres; its identification with the push-forward of the corresponding succession of blow-ups (BlowUpSequence.toSuccession_pushforward) holds for lists without empty centres and is what makes [Kol07, Corollary 85] available for the clauses.

E − E^j: emptying a member

def Manifold.HypersurfaceFamily.emptyMember {M : Type u} (F : HypersurfaceFamily M) (j : F.ι) : HypersurfaceFamily M

Kollár's E - E^j (the proof of [Kol07, Lemma 102], "E_S := (E - E^j)|_S"): the family with the same index set, the j-th member replaced by the empty hypersurface and the others unchanged. Keeping the index set lets the member be named by its index throughout.

Equations

• F.emptyMember j = { ι := F.ι, countable := ⋯, linearOrder := F.linearOrder, hyp := fun (k : F.ι) => if k = j then ∅ else F.hyp k }

@[simp]

theorem Manifold.HypersurfaceFamily.emptyMember_hyp_self {M : Type u} (F : HypersurfaceFamily M) (j : F.ι) : (F.emptyMember j).hyp j = ∅

theorem Manifold.HypersurfaceFamily.emptyMember_hyp_of_ne {M : Type u} (F : HypersurfaceFamily M) {j k : F.ι} (h : k ≠ j) : (F.emptyMember j).hyp k = F.hyp k

theorem Manifold.HypersurfaceFamily.emptyMember_hyp_subset {M : Type u} (F : HypersurfaceFamily M) (j k : F.ι) : (F.emptyMember j).hyp k ⊆ F.hyp k

theorem Manifold.HypersurfaceFamily.ne_of_mem_emptyMember {M : Type u} {F : HypersurfaceFamily M} {j k : F.ι} {a : M} (ha : a ∈ (F.emptyMember j).hyp k) : k ≠ j

theorem Manifold.HypersurfaceFamily.mem_of_mem_emptyMember {M : Type u} {F : HypersurfaceFamily M} {j k : F.ι} {a : M} (ha : a ∈ (F.emptyMember j).hyp k) : a ∈ F.hyp k

theorem Manifold.HypersurfaceFamily.IsSncChartAt.emptyMember {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} {ψ : E ≃L[𝕜] Fin n → 𝕜} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { k : F.ι // a ∈ F.hyp k } → Fin n} (h : IsSncChartAt ψ F φ a c) (j : F.ι) : IsSncChartAt ψ (F.emptyMember j) φ a fun (k : { j_1 : (F.emptyMember j).ι // a ∈ (F.emptyMember j).hyp j_1 }) => c ⟨↑k, ⋯⟩

A chart of the simple normal crossings of F at a is one of E - E^j at a: the members through a other than E^j keep their coordinates.

theorem Manifold.HypersurfaceFamily.IsSnc.emptyMember {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} {ψ : E ≃L[𝕜] Fin n → 𝕜} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (j : F.ι) : IsSnc ψ (F.emptyMember j)

E - E^j has simple normal crossings when E does.

theorem Manifold.HypersurfaceFamily.IsSnc.hasSncWithProper_emptyMember {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} {ψ : E ≃L[𝕜] Fin n → 𝕜} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (j : F.ι) : HasSncWithProper ψ (F.emptyMember j) (F.hyp j) 1

The members of E other than E^j have simple normal crossings with E^j properly: at a point of E^j, a chart of the simple normal crossings of E has E^j as the coordinate hyperplane of the j-th index and is adapted to E^j, while the other members through the point use other coordinates (the indices are injective). This is the hypothesis "E + H has simple normal crossings" of [Kol07, Corollary 85] for H := E^j, needed for the restriction of E - E^j to S = E^j in the proof of [Kol07, Lemma 102].

Proper simple normal crossings pull back along local analytic isomorphisms

theorem Manifold.HypersurfaceFamily.HasSncWithProper.comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} {Y : Set M.carrier} {s : ℕ} (hFY : HasSncWithProper ψ₀ F Y s) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : HasSncWithProper ψ₀ (HypersurfaceFamily.comap (⇑h) F) (⇑h ⁻¹' Y) s

Proper simple normal crossings pull back along a local analytic isomorphism h : N → M: the adapted chart and the chart of the simple normal crossings at h a are transported along a local inverse of h, with the same coordinate indices.

theorem Hironaka.Manifold.isLocalDiffeomorph_blowUpπ_of_codimOne {𝕜 : 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) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(Manifold.blowUpπ ψ₀ hZ)

Blowing up a closed hypersurface is a local analytic isomorphism ([Kol07, Warning 20]: the blow-up of a Cartier divisor is an isomorphism): the blow-up map is a diffeomorphism (IsBlowUp.exists_diffeomorph_of_codim_one).

Lemma 102's core

def Hironaka.Manifold.BDan.BDClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] (s : ℕ) {M : AnalyticManifold 𝕜 E} : Manifold.AnalyticTriple ψ₀ M → Prop

The class of the core of Lemma 102 (the proof of [Kol07, Lemma 102], "from now on we assume that I is D-balanced"): the triples of BOClass s whose ideal sheaf is D-balanced at the mark s; the tuned triples of Tuned.lean belong to it.

Equations

• Hironaka.Manifold.BDan.BDClass s T = (Manifold.AnalyticTriple.BOClass s T ∧ Manifold.IdealSheaf.IsDBalanced T.I s)

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BDan.piMinusOne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : AnalyticMap (Manifold.blowUp ψ₀ ⋯) M

The first blow-up π_{-1} : X_0 → X of the proof of [Kol07, Lemma 102], with centre Z_{-1}.

Equations

• Hironaka.Manifold.BDan.piMinusOne T s j = Manifold.blowUpπ ψ₀ ⋯

theorem Hironaka.Manifold.BDan.isLocalDiffeomorph_piMinusOne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(piMinusOne T s j)

π_{-1} is a local analytic isomorphism ([Kol07, Warning 20]; its centre is a hypersurface).

The data of the core over an arbitrary closed hypersurface

def Hironaka.Manifold.BDan.transformSOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) : Set (Manifold.blowUp ψ₀ hZ).carrier

The transform π^{-1}(E^j) of the member E^j under the blowing-up of a closed hypersurface Z (transformS at Z = Z_{-1}).

Equations

• Hironaka.Manifold.BDan.transformSOf T j hZ = ⇑(Manifold.blowUpπ ψ₀ hZ) ⁻¹' T.F.hyp j

noncomputable def Hironaka.Manifold.BDan.weakTransformIOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) : (Manifold.blowUp ψ₀ hZ).IdealSheaf

The weak transform of 𝓘 under the blowing-up of a closed hypersurface Z (weakTransformI at Z = Z_{-1}).

Equations

• Hironaka.Manifold.BDan.weakTransformIOf T hZ = Manifold.IdealSheaf.weakTransformOf hZ ⋯ T.I

noncomputable def Hironaka.Manifold.BDan.boundaryMinusOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) : Manifold.HypersurfaceFamily (Manifold.blowUp ψ₀ hZ).carrier

E - E^j pulled back along the blowing-up of a closed hypersurface Z (boundaryMinus at Z = Z_{-1}).

Equations

• Hironaka.Manifold.BDan.boundaryMinusOf T j hZ = Manifold.HypersurfaceFamily.comap (⇑(Manifold.blowUpπ ψ₀ hZ)) (T.F.emptyMember j)

def Hironaka.Manifold.BDan.transformS {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : Set (Manifold.blowUp ψ₀ ⋯).carrier

The transform S_0 = π_{-1}^{-1}(E^j) of the member E^j under the isomorphism π_{-1}, the hypersurface S := E^j of the proof of [Kol07, Lemma 102] read on X_0.

Equations

• Hironaka.Manifold.BDan.transformS T s j = Hironaka.Manifold.BDan.transformSOf T j ⋯

theorem Hironaka.Manifold.BDan.isClosedSubmanifold_transformS {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : Manifold.IsClosedSubmanifold ψ₀ (transformS T s j) 1

S_0 is a closed hypersurface of the blown-up manifold.

noncomputable def Hironaka.Manifold.BDan.weakTransformI {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : (Manifold.blowUp ψ₀ ⋯).IdealSheaf

The weak transform I_0 of 𝓘 under π_{-1} (the proof of [Kol07, Lemma 102], "we get a new ideal sheaf I_0").

Equations

• Hironaka.Manifold.BDan.weakTransformI T s j = Hironaka.Manifold.BDan.weakTransformIOf T ⋯

noncomputable def Hironaka.Manifold.BDan.boundaryMinus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : Manifold.HypersurfaceFamily (Manifold.blowUp ψ₀ ⋯).carrier

The family E - E^j pulled back along the isomorphism π_{-1} (the proof of [Kol07, Lemma 102], "E_S := (E - E^j)|_S", before the restriction to S).

Equations

• Hironaka.Manifold.BDan.boundaryMinus T s j = Hironaka.Manifold.BDan.boundaryMinusOf T j ⋯

theorem Hironaka.Manifold.BDan.isSnc_boundaryMinus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (boundaryMinus T s j)

The pulled-back E - E^j has simple normal crossings.

theorem Hironaka.Manifold.BDan.hasSncWithProper_boundaryMinus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) : Manifold.HypersurfaceFamily.HasSncWithProper ψ₀ (boundaryMinus T s j) (transformS T s j) 1

The pulled-back E - E^j has simple normal crossings with S_0 properly (the hypothesis of [Kol07, Corollary 85] on the boundary, for H := S_0).

noncomputable def Hironaka.Manifold.BDan.restrictedTripleOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS'.toAnalyticManifold

The restricted triple (S, I_0|_S, E_S) of the proof of [Kol07, Lemma 102] over an arbitrary closed hypersurface Z and an arbitrary closed hypersurface S' of its blow-up, with the identifications Z = Z_{-1} and S' = S_0 as hypotheses used only in the proof fields (the pulled back centre and transform are only propositionally Z_{-1} and S_0): the restriction of the weak transform of 𝓘, nonzero everywhere because 𝓘 is D-balanced with ord 𝓘 ≤ s (BD.isNonzeroEverywhere_pullback_weakTransformOf), and the trace of the pulled-back E - E^j, with simple normal crossings as the trace of a family having proper simple normal crossings with S_0.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hironaka.Manifold.BDan.restrictedTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hT : BDClass s T) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold

The restricted triple (S, I_0|_S, E_S) of the proof of [Kol07, Lemma 102], on the hypersurface S_0 regarded as a manifold modelled on 𝕜^{n-1} with the standard chart: restrictedTripleOf at Z_{-1} and S_0.

Equations

• Hironaka.Manifold.BDan.restrictedTriple T s j hT = Hironaka.Manifold.BDan.restrictedTripleOf T s j ⋯ ⋯ hT ⋯ ⋯

theorem Hironaka.Manifold.BDan.bmoClass_restrictedTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hT : BDClass s T) : Manifold.AnalyticTriple.BMOClass s (restrictedTriple T s j hT)

The restricted triple lies in the marked class BMOClass s: only finitely many of its members are nonempty, since a nonempty member of the trace comes from a nonempty member of E.

noncomputable def Hironaka.Manifold.BDan.coreOfListOf {𝕜 : 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) : AnalyticManifold.BlowUpSequence ψ₀ M

The core over a sequence, over an arbitrary closed hypersurface Z of M and a closed hypersurface S' of its blowing-up: the blowing-up of Z, then the push-forward of a sequence of centres L on S' regarded as a manifold ([Kol07, Definition 30 (3)]), with empty blow-ups deleted ([Kol07, 32]).

Equations

• Hironaka.Manifold.BDan.coreOfListOf hZ hS' L = (AnalyticManifold.BlowUpSequence.cons hZ (AnalyticManifold.BlowUpSequence.pushforward hS' L)).eraseEmpty

noncomputable def Hironaka.Manifold.BDan.core {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (inp : BMOanData 𝕜 (n - 1) s) (hT : BDClass s T) : AnalyticManifold.BlowUpSequence ψ₀ M

The core of Lemma 102 (the proof of [Kol07, Lemma 102]: the value BMO_{n-1,m}(S, I_0|_S, m, (E - E^j)|_S) is pushed forward ([Kol07, 30.3]) and composed "on the right with our first blow-up π_{-1}"): the core over the value of the input functor on the restricted triple, at Z_{-1} and S_0 (the first blow-up is empty when no component of E^j lies in cosupp(𝓘, s)).

Equations

• Hironaka.Manifold.BDan.core T s j inp hT = Hironaka.Manifold.BDan.coreOfListOf ⋯ ⋯ (inp.functor.seq (Hironaka.Manifold.BDan.restrictedTriple T s j hT) ⋯)

theorem Hironaka.Manifold.BDan.noEmptyCenters_core {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (inp : BMOanData 𝕜 (n - 1) s) (hT : BDClass s T) : (core T s j inp hT).NoEmptyCenters

The value of the core has no empty centres ([Kol07, 32]).

noncomputable def Hironaka.Manifold.BDan {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (m : ℕ) (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) : AnalyticManifold.BlowUpSequence ψ₀ M

The functor BD_{n,m,j} of [Kol07, Lemma 102] on analytic manifolds: on a triple of the class BOClass m, the core at the mark s = tuningParam m applied to the tuned triple (M, W_s(𝓘), E) (the proof's first step, the tuning to a D-balanced ideal with the same order reduction, [Kol07, Corollary 101], at the mark s in place of Kollár's m!), with the input functor BMO_{n-1,s}, a BMOanData 𝕜 (n - 1) (tuningParam m). The member is named by its index j : T.F.ι, which every pull-back keeps.

Equations

• Hironaka.Manifold.BDan m inp T hT j = Hironaka.Manifold.BDan.core (T.tuned m ⋯) (IsLocalRing.tuningParam m) j inp ⋯

theorem Hironaka.Manifold.noEmptyCenters_BDan {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (m : ℕ) (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) : (BDan m inp T hT j).NoEmptyCenters

The value of BD_{n,m,j} has no empty centres ([Kol07, 32]).