Step 2.4 of order reduction: the marked triple on the hypersurface

Step 2.4 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.4]) proves clause (3): for a smooth hypersurface τ : Y ↪ X and an ideal sheaf J ⊂ 𝒪_Y, nonzero on every irreducible component of Y, with τ_*(𝒪_Y/J) = 𝒪_X/I, the ideal I contains the local equations of Y and so has order 1, whence I = W(I); for E = ∅, Step 2.1 does nothing and Step 2.2 may take H = Y, so that clause (3) of Theorem 103 follows from clause (3) of [Kol07, Lemma 102].

Clause (3) of [Kol07, Lemma 102] (Hironaka.BD.hypersurfaceTriple and Hironaka.BD.eq_pushforward_of_quotient in Hironaka/Resolution/Algebraic/BoundaryClearing/) forms its marked triple on a member of the boundary of the triple to which BD_{n,1,j} is applied. For Step 2.4 that triple is the Step 2.2 input (X_r, I_r, F_r + Y_r) (step22Triple at the mark 1 with H := Y), whose boundary has Y_r at position 0, Kollár's E^0 := H; its exceptional part F_r is empty because E = ∅ and Step 2.1 is the empty sequence. This module provides:

• maxOrd_le_one_of_eq_map_smoothDivisor, isMaximalContact_one_of_eq_map and bOClass_one_of_eq_map, the consequences of I = τ_*J that put (X, I, ∅) in the class of BO_{n,1} with Y a hypersurface of maximal contact ("I contains the local equations of Y, and so it has order 1"), derived from I = τ_*J rather than assumed;
• zero_lt_card_step22Triple (position 0 of the Step 2.2 boundary exists) and subscheme_nth_zero_step22Triple (for E = ∅ the member at position 0 is Y as a subscheme: Step 2.1 is the empty sequence, card F_r.ι = 0, nth_append_last);
• closedEmbeddingTriple, the marked triple (Y_r, J, 1, (F_r − Y_r)|_{Y_r} + ⊤) of clause (3) of Lemma 102 on the Step 2.2 triple, with J transported along the identification e of Y_r with Y, and its dimension bound hasDimLE_closedEmbeddingTriple (≤ n − 1).

The triple is formed on the Step 2.2 triple rather than directly on Y because the fields of an abstract blow-up sequence functor relate its values only across IsPullbackOf and IsBaseChangeOf, which preserve the index type of the boundary, and because the value of maxContactCase unfolds to the pushforward of clause (3) of Lemma 102 on the Step 2.2 triple; Hironaka/Resolution/Algebraic/OrderReduction/ClosedEmbedding.lean proves that identity.

theorem Hironaka.BO.maxOrd_le_one_of_eq_map_smoothDivisor {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {Y : T.X.left.IdealSheafData} (hY : AlgebraicGeometry.IsSmoothDivisor Y) {J : Y.subscheme.IdealSheafData} (hIJ : T.I = J.map Y.subschemeι) : T.I.maxOrd ≤ ↑1

If I = τ_*J for a smooth hypersurface τ : Y ↪ X, then max-ord I ≤ 1 (Kol07, 104, Step 2.4: "I contains the local equations of Y, and so it has order 1"): I contains the ideal of Y, of order 1 along Y, and is the unit ideal off Y.

theorem Hironaka.BO.isMaximalContact_one_of_eq_map {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {Y : T.X.left.IdealSheafData} (J : Y.subscheme.IdealSheafData) (hIJ : T.I = J.map Y.subschemeι) : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 Y

Under I = τ_*J, Y is a hypersurface of maximal contact for (I, 1): MC(I, 1) = D⁰(I) = I ⊇ 𝒪_X(−Y) ([Kol07, 104, Step 2.4] with [Kol07, Theorem 80]); neither the smoothness of Y nor the nonvanishing of J enters.

theorem Hironaka.BO.bOClass_one_of_eq_map {k : Type u} [Field k] {n : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) {Y : T.X.left.IdealSheafData} (hY : AlgebraicGeometry.IsSmoothDivisor Y) {J : Y.subscheme.IdealSheafData} (hIJ : T.I = J.map Y.subschemeι) : AlgebraicGeometry.Triple.BOClass n 1 T

Under I = τ_*J, (X, I, E) lies in the class of BO_{n,1} when dim X ≤ n ([Kol07, 104, Step 2.4]).

theorem Hironaka.BO.isNonzeroEverywhere_comap_eqToHom {X Y : AlgebraicGeometry.Scheme} (e : X = Y) (J : Y.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : (J.comap (CategoryTheory.eqToHom e)).IsNonzeroEverywhere

Nonvanishing on every component is preserved by transport along an equality of schemes.

theorem Hironaka.BO.zero_lt_card_step22Triple {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : 0 < Fintype.card (step22Triple T hn hmax bd hm hH hle).E.ι

The Step 2.2 boundary F_r + H_r has a member at position 0.

theorem Hironaka.BO.subscheme_nth_zero_step22Triple {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (hE : IsEmpty T.E.ι) : ((step22Triple T hn hmax bd hm hH hle).E.nth ⟨0, ⋯⟩).subscheme = H.subscheme

For an empty boundary the member at position 0 of the Step 2.2 boundary F_r + H_r is H as a subscheme ([Kol07, 104, Step 2.4]: "if E = ∅ then Step 2.1 does nothing, and in Step 2.2 we can choose H = Y"): Step 2.1 is the empty sequence, F_r is empty and H_r = H (nth_append_last at card F_r.ι = 0).

noncomputable def Hironaka.BO.closedEmbeddingTriple {k : Type u} [Field k] [CharZero k] {n : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑1) (bd : (m j : ℕ) → BDData n m j) {Y : T.X.left.IdealSheafData} (hY : AlgebraicGeometry.IsSmoothDivisor Y) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 Y) (hE : IsEmpty T.E.ι) (J : Y.subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : MarkedTriple k

The marked triple of the closed-embedding case ([Kol07, 104, Step 2.4]; clause (3) of [Kol07, Lemma 102]): Hironaka.BD.hypersurfaceTriple on the Step 2.2 triple (X_r, I_r, F_r + Y_r) at the mark 1 (step22Triple with H := Y), at the position 0 of Y_r (Kollár's E^0 := H), with J transported along the identification of Y_r with Y (subscheme_nth_zero_step22Triple; Step 2.1 is the empty sequence). Its boundary is (F_r − Y_r)|_{Y_r} + ⊤, propositionally ∅ + ⊤, the appended empty member in the convention of hypersurfaceTriple.

Equations

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

theorem Hironaka.BO.hasDimLE_closedEmbeddingTriple {k : Type u} [Field k] [CharZero k] {n : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑1) (bd : (m j : ℕ) → BDData n m j) {Y : T.X.left.IdealSheafData} (hY : AlgebraicGeometry.IsSmoothDivisor Y) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 Y) (hE : IsEmpty T.E.ι) (J : Y.subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : (closedEmbeddingTriple T hn hmax bd hY hle hE J hJ).HasDimLE (n - 1)

The marked triple of the closed-embedding case has dimension ≤ n − 1 when X has dimension ≤ n ([Kol07, 104, Step 2.4]: the functor BMO_{n−1,1}), by Hironaka.BD.hasDimLE_hypersurfaceTriple on the Step 2.2 triple, of dimension ≤ n by bdClass_step22Triple.