The modified first step: the stopped locus and the restricted triple on H⁺

The modified first step of [Wlo09, Theorem 7.4.1]: if the transformed ideal I′ = (u) is the ideal of a smooth hypersurface of maximal contact, the algorithm stops; otherwise it restricts (I′, 1) to a hypersurface of maximal contact V(u₁) and recurses. At the mark 1 the element of maximal contact lies in the ideal ([Wlo09, Lemma 5.5.1 (1)]: H(I) = I for µ = 1), so I′ = (u) near x exactly when the restriction I′|_{V(u)} has zero stalk at x, and by the identity theorem the zero-stalk locus of a restriction is a union of connected components of V(u) (isClopen_setOf_stalkIdeal_eq_bot): the stopped locus is Kollár's Z_{-1} at the mark 1 (BD.Zminus1, the components of the member inside cosupp(𝓘, 1), from the proof of [Kol07, Lemma 102]). The modification of the algorithm is precisely not to blow Z_{-1} up (Kollár's isomorphic first blow-up) but to stop there.

This module builds the objects of the modified core: the stopped locus stopLocus T j; the closed hypersurface hplus T j = E^j ∖ Z_{-1} (a union of connected components of the member, hence closed in M: isClosedSubmanifold_hplus); the boundary E − E^j, in proper normal crossings with it (hasSncWithProper_hplus); and the restricted triple restrictedTripleMod T j on the bundled hypersurface H⁺ (toAnalyticManifold, modelled on 𝕜^{n−1}): the pull-back of 𝓘, nonzero everywhere by the identity theorem (isNonzeroEverywhere_hplusIdeal: a zero stalk of the restriction at a point of H⁺ would put its whole component into cosupp(𝓘, 1), i.e. into Z_{-1}), and the trace of E − E^j, with simple normal crossings as the trace of a proper family with simple normal crossings. The restricted triple lies in the marked class BMOClass 1 (bmoClass_restrictedTripleMod), the domain of the modified functor one dimension down.

The stopped locus and H⁺

@[reducible, inline]

abbrev Hironaka.Manifold.BMOmod.stopLocus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : Set M.carrier

The stopped locus of the member j at the mark 1: Kollár's Z_{-1} (BD.Zminus1, the proof of [Kol07, Lemma 102]), the points of E^j whose connected component in E^j lies in cosupp(𝓘, 1); at the mark 1 with maximal contact this is where 𝓘 = (u) ("the algorithm is stopped", [Wlo09, Theorem 7.4.1]).

Equations

• Hironaka.Manifold.BMOmod.stopLocus T j = Hironaka.Manifold.BD.Zminus1 T.I 1 (T.F.hyp j)

theorem Hironaka.Manifold.BMOmod.isClosed_stopLocus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : IsClosed (stopLocus T j)

def Hironaka.Manifold.BMOmod.hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : Set M.carrier

H⁺, the member E^j without its stopped components: the hypersurface on which the run one dimension down is performed ("otherwise we restrict", [Wlo09, Theorem 7.4.1]).

Equations

• Hironaka.Manifold.BMOmod.hplus T j = T.F.hyp j \ Hironaka.Manifold.BMOmod.stopLocus T j

theorem Hironaka.Manifold.BMOmod.hplus_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : hplus T j ⊆ T.F.hyp j

theorem Hironaka.Manifold.BMOmod.mem_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {x : M.carrier} : x ∈ hplus T j ↔ x ∈ T.F.hyp j ∧ x ∉ stopLocus T j

theorem Hironaka.Manifold.BMOmod.connectedComponentIn_subset_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {x : M.carrier} (hx : x ∈ hplus T j) : connectedComponentIn (T.F.hyp j) x ⊆ hplus T j

The connected component in E^j of a point of H⁺ lies in H⁺ (Z_{-1} is a union of components of E^j).

theorem Hironaka.Manifold.BMOmod.isClosed_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : IsClosed (hplus T j)

H⁺ is closed in M: its complement in E^j is Z_{-1}, a union of components of E^j, open in E^j (every point of Z_{-1} has an adapted chart of E^j meeting E^j only inside its component).

theorem Hironaka.Manifold.BMOmod.isAdaptedChart_hplus_restrOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {φ : OpenPartialHomeomorph M.carrier (Fin n → 𝕜)} {σ : Fin 1 ↪ Fin n} (h : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (T.F.hyp j) φ σ) : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (hplus T j) (φ.restrOpen (stopLocus T j)ᶜ ⋯) σ

An adapted chart of E^j, restricted to the complement of the stopped locus, is an adapted chart of H⁺.

theorem Hironaka.Manifold.BMOmod.isClosedSubmanifold_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (hplus T j) 1

H⁺ is a closed hypersurface of M (its charts are E^j's, restricted off Z_{-1}).

theorem Hironaka.Manifold.BMOmod.hasSncWithProper_hplus {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : Manifold.HypersurfaceFamily.HasSncWithProper (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (T.F.emptyMember j) (hplus T j) 1

The boundary E − E^j has simple normal crossings with H⁺ properly (Corollary 85's hypothesis for the trace): E^j's proper snc charts (hasSncWithProper_emptyMember), restricted off Z_{-1}.

The restriction of 𝓘 to H⁺ is nonzero everywhere

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.hplusIdeal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 (Fin (n - 1) → 𝕜) ⋯.toAnalyticManifold.carrier)

The restriction of 𝓘 to the bundled hypersurface H⁺ (the pull-back along the inclusion).

Equations

• Hironaka.Manifold.BMOmod.hplusIdeal T j = Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ T.I

theorem Hironaka.Manifold.BMOmod.isNonzeroEverywhere_hplusIdeal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : (hplusIdeal T j).IsNonzeroEverywhere

The restriction of 𝓘 to H⁺ is nonzero everywhere: a zero stalk at a point p of H⁺ puts the whole connected component of p (in H⁺, which is its component in E^j) into the zero-stalk locus (isClopen_setOf_stalkIdeal_eq_bot, the identity theorem), hence into cosupp(𝓘, 1) (cosupport_pullback), so p ∈ Z_{-1}, against p ∈ H⁺.

The restricted triple on H⁺

noncomputable def Hironaka.Manifold.BMOmod.restrictedTripleModOf {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S 1) (hSeq : S = hplus T j) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS.toAnalyticManifold

The restricted triple read on a closed hypersurface S propositionally equal to H⁺: the data on S, the proofs transported by substitution (restrictedTripleMod is its instance at H⁺).

Equations

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

noncomputable def Hironaka.Manifold.BMOmod.restrictedTripleMod {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold

The restricted triple on H⁺ ("we restrict (I′, 1) to a hypersurface of maximal contact V(u₁)", [Wlo09, Theorem 7.4.1], on the components which are not stopped; the counterpart of Kollár's (S, I_0|_S, E_S) of the proof of [Kol07, Lemma 102], BD.restrictedTriple, without the first blow-up): the pull-back of 𝓘 to the bundled hypersurface H⁺ (nonzero everywhere by isNonzeroEverywhere_hplusIdeal) and the trace of E − E^j (with simple normal crossings as the trace of a proper family, isSnc_traceFamily).

Equations

• Hironaka.Manifold.BMOmod.restrictedTripleMod T j = Hironaka.Manifold.BMOmod.restrictedTripleModOf T j ⋯ ⋯

@[simp]

theorem Hironaka.Manifold.BMOmod.restrictedTripleMod_I {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : (restrictedTripleMod T j).I = hplusIdeal T j

@[simp]

theorem Hironaka.Manifold.BMOmod.restrictedTripleMod_F {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) : (restrictedTripleMod T j).F = ⋯.traceFamily (T.F.emptyMember j)

theorem Hironaka.Manifold.BMOmod.bmoClass_restrictedTripleMod {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : Manifold.AnalyticTriple.BMOClass 1 (restrictedTripleMod T j)

The restricted triple lies in the marked class BMOClass 1 (the domain of the modified functor one dimension down): only finitely many trace members are nonempty, a nonempty trace member coming from a nonempty member of E.

theorem Hironaka.Manifold.BMOmod.bmoClass_restrictedTripleModOf {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (j : T.F.ι) (hT : Manifold.AnalyticTriple.BMOClass 1 T) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S 1) (hSeq : S = hplus T j) : Manifold.AnalyticTriple.BMOClass 1 (restrictedTripleModOf T j hS hSeq)

The restricted triple on S = H⁺ lies in the marked class BMOClass 1.