Clause (5) of the principalization family: closed embeddings with F = ∅

Clause (5) of [Kol07, Theorem 35] ([Kol07, 34.3]; [Kol07, Claim 71.2], proved in [Kol07, 108]), per open, in the form CommutesWithClosedEmbeddingsOfEmptyDivisorFam: for F = ∅ the value of the principalization functor in dimension n on U is the restricted push-forward of the value in dimension n − s on U ∩ S, for a closed submanifold S of codimension s. The route: for F = ∅ the principalization value is the input's value (principalizationValue_empty) — the disjoining bound is 0 (no nonempty member, Nat.card_of_isEmpty), the disjoining list is nil (valueOf_disjoinList_eq moves the value to the bound 0), the disjoined triple has the restricted ideal (pullback_id_eq_self) and a boundary whose members are all empty (the collapse of the empty family), so the input's indifferentToEmptyMembers reads it on the empty family, its commutesWithLocalIsos along the inclusion of the shrinking open and its compat along U ≤ image bring the value back to U, the eraseEmptys collapsing by eraseEmpty_pullback_eraseEmpty and eraseEmpty_of_noEmptyCenters. Clause (5) is then the input family's commutation hbmo rewritten on both sides (principalizationFam_closedEmbedding). Kollár's remark that (71.2) only makes sense for the marking m = 1 [Kol07, Claim 71.2] is why the input is taken at mark 1.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.emptyTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M

The triple (M, 𝓘, ∅).

Equations

• Hironaka.Manifold.emptyTriple I hI = { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ }

theorem Hironaka.Manifold.emptyTriple_bmoClass {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : Manifold.AnalyticTriple.BMOClass 1 (emptyTriple I hI)

(M, 𝓘, ∅) lies in the marked class at mark 1.

theorem Hironaka.Manifold.disjoinBound_emptyTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (W : TopologicalSpace.Opens M.carrier) : disjoinBound (emptyTriple I hI) W = 0

With no member, the disjoining bound is 0.

theorem Hironaka.Manifold.meetLocus_one_restrictTriple_emptyTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (W : TopologicalSpace.Opens M.carrier) : (restrictTriple (emptyTriple I hI) W).F.meetLocus (0 + 1) = ∅

The one-point locus of the restricted empty family is empty.

def Hironaka.Manifold.emptyOrderEmbedding {X : Type u} (G : Manifold.HypersurfaceFamily X) : (Manifold.HypersurfaceFamily.empty X).ι ↪o G.ι

The order embedding of the empty family into any family.

Equations

• Hironaka.Manifold.emptyOrderEmbedding G = { toFun := fun (j : (Manifold.HypersurfaceFamily.empty X).ι) => PEmpty.elim j, inj' := ⋯, map_rel_iff' := ⋯ }

theorem Hironaka.Manifold.collapsedFamilyOf_nil_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (X : AnalyticManifold 𝕜 (Fin n → 𝕜)) (F : Manifold.HypersurfaceFamily X.carrier) (hF : IsEmpty F.ι) (k : (collapsedFamilyOf (AnalyticManifold.BlowUpSequence.nil X) F).ι) : (collapsedFamilyOf (AnalyticManifold.BlowUpSequence.nil X) F).hyp k = ∅

Every member of the collapse of a memberless family along the empty disjoining list is empty.

theorem Hironaka.Manifold.principalizationValue_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hT : Manifold.AnalyticTriple.BMOClass 1 (emptyTriple I hI)) : principalizationValue bmo (emptyTriple I hI) U hU = (bmo.functor.fam (emptyTriple I hI) hT).seqOn U hU

For the empty divisor the principalization value on U is the input's value on U ([Kol07, 72] with E = ∅: no disjoining blow-up): the disjoined triple is the restricted triple up to an empty boundary member, and the input's indifferentToEmptyMembers, commutesWithLocalIsos (along the inclusion of the shrinking open) and compat (along U ≤ image) bring its value on the reading open back to U.

theorem Hironaka.Manifold.principalizationFam_closedEmbedding {𝕜 : Type} [RCLike 𝕜] (bmo : (n : ℕ) → BMOanFam 𝕜 n 1) (hbmo : ∀ (n s : ℕ), (bmo n).functor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam (bmo (n - s)).functor) (n s : ℕ) : (principalizationFam (bmo n)).CommutesWithClosedEmbeddingsOfEmptyDivisorFam (principalizationFam (bmo (n - s)))

Clause (5) of [Kol07, Theorem 35] ([Kol07, 34.3; Claim 71.2; 108]): the principalization functors commute with closed embeddings of empty divisor between the models 𝕜ⁿ and 𝕜^{n−s} whenever the input family does (hbmo) — for F = ∅ both values are the input's values (principalizationValue_empty).