Corollary 85: going up and down

[Kol07, Corollary 85]: for I D-balanced with m = max-ord I, E simple normal crossing, H a smooth hypersurface of maximal contact ([Kol07, Definition 78]) with E + H simple normal crossing and no irreducible component of H in cosupp(I, m), pushing forward from H to X is a one-to-one correspondence between the smooth blow-up sequences of order ≥ m starting with (H, I|_H, m, E|_H) and those of order m starting with (X, I, E). Kollár's proof says that this follows from Theorems 84 and 80 except for the role of E:

• well defined: [Kol07, Theorem 84] (going up) with the divisor family carried (IsDBalanced.isOrderSeq_pushforward of Hironaka/Resolution/Algebraic/Kol07/GoingUp.lean);
• injective: pushforward_injective;
• onto: going down (isOrderGeSeq_pullback_of_strictTransformSeq_le of Hironaka/Resolution/Algebraic/MaximalContact/GoingDown.lean) with j_* j^* B = B (pushforward_pullback_of_strictTransformSeq_le), the centres of an order-m sequence for (X, I, E) lying in the strict transforms H_i by Definition 78 read on X itself (strictTransformSeq_le_center_of_isDynamicMaximalContact). Definition 78 is stated for the empty divisor family, so the sequence's family is first dropped (IsOrderSeq.empty_of_isOrderSeq): the exceptional divisors form a sub-family of the induced family E_i at every stage (exists_isSubfamilyVia_totalTransformSeq), and simple normal crossings with a family pass to its sub-families (hasSncWith_of_isSubfamilyVia).

The static instance (IsDBalanced.bijOn_pushforward_of_isMaximalContact, with H of maximal contact in the sense of [Kol07, Theorem 80 (1)] and 1 ≤ m) takes the containment of the centres from IsOrderSeq.strictTransformSeq_le_center_of_le_MC instead.

Convention. The hypothesis _hHc, that no irreducible component of H lies in cosupp(I, m), is part of Kollár's statement of Corollary 85 (as S ⊄ cosupp(I, m) is of his Theorem 84) and is kept in both theorems so that they read as printed. The proofs do not need it: the correspondence is assembled from the library's Theorem 84 (IsDBalanced.isOrderSeq_pushforward), which is stated and proved without that hypothesis (the sheaf-level Lemma 62 it iterates, markedTransform_comap_blowUpMap_of_pow_dvd, needs only F^m ∣ π^* I), and from going down, which uses only that the centres lie in the H_i. The sub-family lemmas of the first section are also used by Hironaka/Resolution/Algebraic/Tuning/Corollary101.lean.

Sub-families and simple normal crossings

def Hironaka.Sequence.IsSubfamilyVia {X : AlgebraicGeometry.Scheme} (F' F : X.DivisorFamily) (σ : F'.ι → F.ι) : Prop

F' is a sub-family of F via σ: an injection of indices matching the components.

Equations

• Hironaka.Sequence.IsSubfamilyVia F' F σ = (Function.Injective σ ∧ ∀ (a : F'.ι), F.component (σ a) = F'.component a)

theorem Hironaka.Sequence.hasSncWith_of_isSubfamilyVia {X : AlgebraicGeometry.Scheme} {F' F : X.DivisorFamily} {σ : F'.ι → F.ι} (hσ : IsSubfamilyVia F' F σ) {Z : X.IdealSheafData} (h : F.HasSncWith Z) : F'.HasSncWith Z

Simple normal crossings with a family pass to its sub-families: the same adapted coordinates, the index map composed with the inclusion of indices.

theorem Hironaka.Sequence.isSubfamilyVia_totalTransform {X : AlgebraicGeometry.Scheme} {F' F : X.DivisorFamily} {σ : F'.ι → F.ι} (hσ : IsSubfamilyVia F' F σ) (D : X.IdealSheafData) : IsSubfamilyVia (F'.totalTransform D) (F.totalTransform D) fun (a : (F'.totalTransform D).ι) => toLex (Sum.map σ id (ofLex a))

The total transform of a sub-family is a sub-family of the total transform (the exceptional divisor is matched with itself).

theorem Hironaka.Sequence.exists_isSubfamilyVia_totalTransformSeq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {F' F : X.DivisorFamily} (σ : F'.ι → F.ι) (hσ : IsSubfamilyVia F' F σ) (i : Fin (S.length + 1)) : ∃ (τ : (S.totalTransformSeq F' i).ι → (S.totalTransformSeq F i).ι), IsSubfamilyVia (S.totalTransformSeq F' i) (S.totalTransformSeq F i) τ

Along a blow-up sequence, the induced family of a sub-family is a sub-family of the induced family at every stage.

theorem Hironaka.Sequence.empty_isSubfamilyVia {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : IsSubfamilyVia (AlgebraicGeometry.Scheme.DivisorFamily.empty X) E fun (a : (AlgebraicGeometry.Scheme.DivisorFamily.empty X).ι) => PEmpty.elim a

The empty family is a sub-family of every family.

theorem Hironaka.Sequence.IsOrderSeq.empty_of_isOrderSeq {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) {S : X.BlowUpSequence} (h : S.IsOrderSeq f I E m) : S.IsOrderSeq f I (AlgebraicGeometry.Scheme.DivisorFamily.empty X) m

Dropping the divisor family: a smooth blow-up sequence of order m for (X, I, E) is one for (X, I) with the empty family — its centres have simple normal crossings with the exceptional divisors, a sub-family of the induced families E_i.

Corollary 85

theorem Hironaka.Sequence.IsDBalanced.bijOn_pushforward {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (H : X.IdealSheafData) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced f I m) (hmax : I.maxOrd = ↑m) (hH : AlgebraicGeometry.IsSmoothDivisor H) (hE : (E.append H).IsSnc) (hMC : AlgebraicGeometry.Scheme.IdealSheafData.IsDynamicMaximalContact f I m H) (_hHc : ∀ η ∈ H.support.genericPoints, I.ord η < ↑m) : Set.BijOn (fun (T : H.subscheme.BlowUpSequence) => T.pushforward H.subschemeι) {T : H.subscheme.BlowUpSequence | T.IsOrderGeSeq (CategoryTheory.CategoryStruct.comp H.subschemeι f) (I.comap H.subschemeι) m (E.comap H.subschemeι)} {B : X.BlowUpSequence | B.IsOrderSeq f I E m}

[Kol07, Corollary 85] (going up and down): X a smooth variety, I D-balanced with m = max-ord I, E simple normal crossing, H ⊂ X a smooth hypersurface of maximal contact ([Kol07, Definition 78]) with E + H simple normal crossing and no irreducible component of H in cosupp(I, m); pushing forward from H to X is a one-to-one correspondence between the smooth blow-up sequences of order ≥ m starting with (H, I|_H, m, E|_H) and those of order m starting with (X, I, E): well defined by [Kol07, Theorem 84] with E carried, injective by pushforward_injective, onto by going down and j_* j^* B = B, the centres lying in the H_i by Definition 78 read on X itself after dropping E. The hypothesis _hHc on the components of H is part of Kollár's statement and is kept so that the theorem reads as printed; the proof does not need it, because IsDBalanced.isOrderSeq_pushforward and isOrderGeSeq_pullback_of_strictTransformSeq_le are both proved without it (module docstring, Convention).

theorem Hironaka.Sequence.IsDBalanced.bijOn_pushforward_of_isMaximalContact {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (H : X.IdealSheafData) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced f I m) (hmax : I.maxOrd = ↑m) (hm : 1 ≤ m) (hH : AlgebraicGeometry.IsSmoothDivisor H) (hE : (E.append H).IsSnc) (hMC : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact f I m H) (_hHc : ∀ η ∈ H.support.genericPoints, I.ord η < ↑m) : Set.BijOn (fun (T : H.subscheme.BlowUpSequence) => T.pushforward H.subschemeι) {T : H.subscheme.BlowUpSequence | T.IsOrderGeSeq (CategoryTheory.CategoryStruct.comp H.subschemeι f) (I.comap H.subschemeι) m (E.comap H.subschemeι)} {B : X.BlowUpSequence | B.IsOrderSeq f I E m}

[Kol07, Corollary 85] with H of maximal contact in the static sense of [Kol07, Theorem 80 (1)], 𝒪_X(−H) ⊆ MC(I), and 1 ≤ m; the centres of an order-m sequence lie in the H_i by IsOrderSeq.strictTransformSeq_le_center_of_le_MC. The hypothesis _hHc on the components of H is part of Kollár's statement and is kept so that the theorem reads as printed; the proof does not need it, for the reason given in the module docstring (Convention).