Lemma 102 in the compatible-family form: the construction

The functor BD_{n,m,j} of [Kol07, Lemma 102] is built in BD.lean from the marked order-reduction functor BMO_{n-1,m} one dimension down: blow up the union Z_{-1} of the components of E^j inside cosupp(I, m), restrict the weak transform I_0 and the boundary E - E^j to the transform S_0 of E^j, apply the input functor to the restricted triple and push the result forward, BD_{n,m,j}(X, I, E) := τ_* BMO_{n-1,m}(S, I_0|_S, m, E_S) ∘ π_{-1}. This module repeats the construction with the input in the compatible-family form: inp : BMOanFam 𝕜 (n - 1) s (Functor/Family.lean), whose values are finite blow-up sequences on the relatively compact open subsets, compatible under inclusion ([Wlo09, Theorem 2.0.3 (1), (4)]; the remark after [BM97, Theorem 1.6] on locally finite sequences), in place of the structure BMOanData. The constructions of BD.lean on the whole manifold are reused: the centre Z_{-1} and its blowing-up π_{-1} (BD.Zminus1, BDan.piMinusOne), the transform S_0 = π_{-1}^{-1}(E^j) (BDan.transformS), the restricted triple (S_0, I_0|_{S_0}, E_S) (BDan.restrictedTriple).

• isCompact_closure_preimageOpens_of_isProperMap — the preimage of a relatively compact open under a proper analytic map is relatively compact.
• BDan.piOpenOf, BDan.isCompact_closure_piOpenOf — the preimage π^{-1}(U) of an open U under the blowing-up of a closed hypersurface Z, relatively compact when U is (the blowing-up is proper); BDan.piOpen at Z = Z_{-1}.
• BDan.liftInclOf, BDan.isLocalDiffeomorph_liftInclOf — the lift of the inclusion U ⊆ M to the blowing-up of Z ∩ U, corestricted onto π^{-1}(U): a local analytic isomorphism onto that open, since the restriction of a blowing-up over an open is the blowing-up of the restricted centre; BDan.liftIncl at Z = Z_{-1}.
• BDan.coreFamOn T s j inp hT U hU — the core on the relatively compact open U, for a triple whose ideal sheaf is D-balanced: the blowing-up of Z_{-1} ∩ U, followed by the value of the input family on the restricted triple read at the trace of π_{-1}^{-1}(U) on S_0, pushed forward to the open π_{-1}^{-1}(U) of the blown-up manifold ([Kol07, Definition 30 (3)]) and pulled back along the corestricted lift of the inclusion, with empty blow-ups deleted ([Kol07, 32]).
• BDanFam m inp T hT j U hU — the value of BD_{n,m,j} on U for a triple of the class BOClass m: the core at the mark s = tuningParam m applied to the tuned triple (M, W_s(𝓘), E) (Step 1 of Kollár's proof, "by (101) … we assume that I is D-balanced"; Tuned.lean), the input being the marked family at the mark s.

The clauses of Lemma 102 for these values (the order clause, clause (1), the commutation with local analytic isomorphisms, the indifference to empty members, the value at an empty member) and the compatibility under restriction are proved in BDFamClauses.lean, BDFamOrder.lean, BDFamCompat.lean, BDFamIndiff.lean and BDFamComm.lean, and assembled into the compatible family bdanFam and the data bdanFamDataOfInput : BDanFamData ψ₀ (tuningParam m) in BOanFamOfInput.lean, the input of Steps 2.1 and 2.2 of the proof of Theorem 103 in this form.

theorem Hironaka.Manifold.isCompact_closure_preimageOpens_of_isProperMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (hf : IsProperMap ⇑f) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : IsCompact (closure ↑(Manifold.preimageOpens ⇑f ⋯ U))

The preimage of a relatively compact open under a proper analytic map is relatively compact: the closure of the preimage lies in the preimage of the closure, which is compact.

The preimage of an open and the corestricted lift over an arbitrary closed hypersurface

noncomputable def Hironaka.Manifold.BDan.piOpenOf {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) : TopologicalSpace.Opens (Manifold.blowUp ψ₀ hZ).carrier

The preimage π^{-1}(U) of an open under the blowing-up of a closed hypersurface Z (piOpen at Z = Z_{-1}).

Equations

• Hironaka.Manifold.BDan.piOpenOf hZ U = Manifold.preimageOpens ⇑(Manifold.blowUpπ ψ₀ hZ) ⋯ U

theorem Hironaka.Manifold.BDan.isCompact_closure_piOpenOf {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : IsCompact (closure ↑(piOpenOf hZ U))

π^{-1}(U) is relatively compact when U is: the blowing-up is a proper map.

theorem Hironaka.Manifold.BDan.range_liftStep_inclusion_subsetOf {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) : Set.range ⇑(AnalyticManifold.BlowUpSequence.liftStep (M.inclusion U) ⋯ hZ) ⊆ ↑(piOpenOf hZ U)

The lift of the inclusion U ⊆ M to the blowing-ups of Z (BlowUpSequence.liftStep) lands in π^{-1}(U).

noncomputable def Hironaka.Manifold.BDan.liftInclOf {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) : AnalyticMap (Manifold.blowUp ψ₀ ⋯) ((Manifold.blowUp ψ₀ hZ).restrict (piOpenOf hZ U))

The lift of the inclusion U ⊆ M to the blowing-up of Z ∩ U, corestricted onto the open π^{-1}(U) of the blowing-up of Z (liftIncl at Z = Z_{-1}). It is a local analytic isomorphism onto that open (isLocalDiffeomorph_liftInclOf; surjective by surjective_liftIncl in BDFamTransport.lean): the restriction of a blowing-up over an open is the blowing-up of the restricted centre.

Equations

• Hironaka.Manifold.BDan.liftInclOf hZ U = Hironaka.Manifold.AnalyticMap.corestrict (AnalyticManifold.BlowUpSequence.liftStep (M.inclusion U) ⋯ hZ) (Hironaka.Manifold.BDan.piOpenOf hZ U) ⋯

theorem Hironaka.Manifold.BDan.isLocalDiffeomorph_liftInclOf {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(liftInclOf hZ U)

The corestricted lift of the inclusion is a local analytic isomorphism.

noncomputable def Hironaka.Manifold.BDan.piOpen {𝕜 : 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.ι) (U : TopologicalSpace.Opens M.carrier) : TopologicalSpace.Opens (Manifold.blowUp ψ₀ ⋯).carrier

The preimage π_{-1}^{-1}(U) of an open U of M in the blowing-up of Z_{-1}.

Equations

• Hironaka.Manifold.BDan.piOpen T s j U = Hironaka.Manifold.BDan.piOpenOf ⋯ U

noncomputable def Hironaka.Manifold.BDan.liftIncl {𝕜 : 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.ι) (U : TopologicalSpace.Opens M.carrier) : AnalyticMap (Manifold.blowUp ψ₀ ⋯) ((Manifold.blowUp ψ₀ ⋯).restrict (piOpen T s j U))

The lift of the inclusion U ⊆ M to the blowing-up of Z_{-1} ∩ U, corestricted onto the open π_{-1}^{-1}(U) of the blowing-up of Z_{-1} (liftInclOf at Z_{-1}).

Equations

• Hironaka.Manifold.BDan.liftIncl T s j U = Hironaka.Manifold.BDan.liftInclOf ⋯ U

noncomputable def Hironaka.Manifold.BDan.coreFamOn {𝕜 : 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 : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)

The core of the proof of [Kol07, Lemma 102] on a relatively compact open U, for a triple of BOClass s with D-balanced ideal sheaf and the input BMO_{n-1,s} in the compatible-family form: the blowing-up of Z_{-1} ∩ U, then the input family's value on the restricted triple (S_0, I_0|_{S_0}, E_S) read at the trace of π_{-1}^{-1}(U) on S_0, pushed forward to the open π_{-1}^{-1}(U) ([Kol07, Definition 30 (3)]; BlowUpSequence.pushforwardRestrict) and pulled back along the corestricted lift of the inclusion, with empty blow-ups deleted ([Kol07, 32]).

Equations

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

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

The core on U has no empty centres ([Kol07, 32]): they are deleted.

noncomputable def Hironaka.Manifold.BDanFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {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)) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)

The value of BD_{n,m,j} on a relatively compact open U ([Kol07, Lemma 102], in the compatible-family form): for 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 tuning that opens the proof of Lemma 102, Tuned.lean), with the input BMO_{n-1,s} in the compatible-family form. The member E^j is named by its index j.

Equations

• Hironaka.Manifold.BDanFam m inp T hT j U hU = Hironaka.Manifold.BDan.coreFamOn (T.tuned m ⋯) (IsLocalRing.tuningParam m) j inp ⋯ U hU

theorem Hironaka.Manifold.noEmptyCenters_BDanFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {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).NoEmptyCenters

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