The centre of the monomial phase at the mark 1: the positive locus of the latest member

The modified algorithm of [Wlo09, Theorem 7.4.1] resolves the monomial marked ideal (M(𝓘), 1) "by blow-ups at exceptional divisors for which ρ(x) is maximal". The monomial case of the resolution, [Wlo09, §6, Step 2b], orders the divisors of E (the linear order of the boundary family, Kollár's ordered index set [Kol07, Definition 65]; the total transform appends the new member last, so the order is the order of birth), compares subsets lexicographically, and takes ρ(x) to be the maximal subset whose exponents sum to at least µ with every proper sub-sum below µ. At µ = 1 with natural exponents the admissible subsets are the singletons {D} of components through x with exponent a_D ≥ 1, so ρ(x) is the singleton of the latest-born such component, and the centre of a step is the locus of the positive-exponent components of the latest-born member which has one: "the maximal locus of ρ determines at most one maximal component of supp(I, µ) through each x", and here that locus is the positive locus of the top member, taken whole.

A component D ⊆ E^j has exponent a_D = ord_D 𝓘 ≥ 1 iff 𝓘 vanishes along D, i.e. D ⊆ cosupp(𝓘, 1), so the positive locus of E^j is Kollár's Z_{-1} of the proof of [Kol07, Lemma 102] at the mark 1 ("the union of those irreducible components E^{jk} ⊂ E^j that are contained in cosupp(I, m)"), BD.Zminus1 T.I 1 (T.F.hyp j). Its closed-submanifold witness (isClosedSubmanifold_Zminus1), its simple normal crossings with E (hasSncWith_Zminus1, hence clause (3′) of [Kol07, Definition 66] through HasSncWith.hasOnlyNormalCrossingsWith_idealSheaf) and the order clause (1′) at the mark 1 (Zminus1_subset_cosupp) are reused from there. The identification with the fine exponents of componentExponent is proved in Step2bLocal.lean.

This module provides the objects of the rule: positiveLocus (Kollár's Z_{-1} at the mark 1), activeMembers (the members with a nonempty positive locus, finitely many by the finiteness clause of the class), topMember (the latest-born active member, the maximum in the linear order) and step2bCenter, with the two head clauses of isOfOrderGe_cons_iff for the centre. The blow-up step (the marked transform at the mark 1 and the total transform) is Step2bStep.lean, the phase by recursion Step2bPhase.lean, the exponents after a step Step2bExponent.lean. A centre of codimension one is a legal member of a CenterList (the constructor takes any codimension; the blow-up is then an isomorphism, cons_codimOne_exists_diffeomorph, as in the remarks after [Wlo09, Theorem 2.0.3]).

The positive locus of a member: Kollár's Z_{-1} at the mark 1

def Hironaka.Manifold.BMOmod.positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) : Set M.carrier

The positive locus of the member E^j: the union of the connected components of E^j along which 𝓘 vanishes (exponent a_D = ord_D 𝓘 ≥ 1), Kollár's Z_{-1} of the proof of [Kol07, Lemma 102] at the mark 1 (BD.Zminus1); the singletons of [Wlo09, §6, Step 2b] at µ = 1.

Equations

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

theorem Hironaka.Manifold.BMOmod.positiveLocus_def {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) : positiveLocus T j = BD.Zminus1 T.I 1 (T.F.hyp j)

theorem Hironaka.Manifold.BMOmod.positiveLocus_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) : positiveLocus T j ⊆ T.F.hyp j

The positive locus lies in its member ("E^{jk} ⊂ E^j", the proof of [Kol07, Lemma 102]).

theorem Hironaka.Manifold.BMOmod.isClosedSubmanifold_positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) : Manifold.IsClosedSubmanifold ψ₀ (positiveLocus T j) 1

The positive locus of a member is a closed submanifold of codimension 1 (isClosedSubmanifold_Zminus1).

theorem Hironaka.Manifold.BMOmod.hasSncWith_positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) : Manifold.HypersurfaceFamily.HasSncWith ψ₀ T.F (positiveLocus T j) 1

The positive locus has simple normal crossings with E (hasSncWith_Zminus1; the proof of [Kol07, Lemma 102] at the mark 1).

theorem Hironaka.Manifold.BMOmod.hasOnlyNormalCrossingsWith_positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (j : T.F.ι) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith T.F.idealSheaf ⋯.idealSheaf

Clause (3′) of [Kol07, Definition 66] for the positive locus as a centre: the reduced boundary ideal sheaf has only normal crossings with the ideal sheaf of the centre.

theorem Hironaka.Manifold.BMOmod.one_le_ord_of_mem_positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {j : T.F.ι} {x : M.carrier} (hx : x ∈ positiveLocus T j) : ↑1 ≤ Manifold.IdealSheaf.ord T.I x

𝓘 vanishes on the positive locus (Z_{-1} ⊆ cosupp(𝓘, 1)).

theorem Hironaka.Manifold.BMOmod.one_le_ordAlong_of_mem_positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {j : T.F.ι} {a : M.carrier} (ha : a ∈ positiveLocus T j) : ↑1 ≤ ⋯.idealSheaf.ordAlongIdeal T.I a

Clause (1′) of [Kol07, Definition 66] for the positive locus as a centre at the mark 1: the order of 𝓘 along the positive locus is at least 1 at each of its points (stalkIdeal_le_pow_of_eventually_le_ord applied to Z_{-1} ⊆ cosupp(𝓘, 1)).

The active members and the top member

def Hironaka.Manifold.BMOmod.activeMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : Set T.F.ι

The active members: those with a nonempty positive locus, i.e. carrying a component of positive exponent.

Equations

• Hironaka.Manifold.BMOmod.activeMembers T = {j : T.F.ι | (Hironaka.Manifold.BMOmod.positiveLocus T j).Nonempty}

theorem Hironaka.Manifold.BMOmod.activeMembers_subset_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : activeMembers T ⊆ {j : T.F.ι | T.F.hyp j ≠ ∅}

theorem Hironaka.Manifold.BMOmod.activeMembers_finite {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : (activeMembers T).Finite

Finitely many members are active (the finiteness clause of BMOClass: finitely many nonempty members).

noncomputable def Hironaka.Manifold.BMOmod.topMember {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : T.F.ι

The top member: the largest active member in the linear order of the family (Kollár's ordered index set [Kol07, Definition 65], the order of birth along the total transforms). At µ = 1 this is the maximal subset of [Wlo09, §6, Step 2b]: the singleton of the latest-born component of positive exponent.

Equations

• Hironaka.Manifold.BMOmod.topMember T hfin hne = hfin.toFinset.max' ⋯

theorem Hironaka.Manifold.BMOmod.topMember_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : topMember T hfin hne ∈ activeMembers T

theorem Hironaka.Manifold.BMOmod.le_topMember {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {j : T.F.ι} (hj : j ∈ activeMembers T) : j ≤ topMember T hfin hne

The Step 2b centre

def Hironaka.Manifold.BMOmod.step2bCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Set M.carrier

The centre of a step of the monomial phase ([Wlo09, Theorem 7.4.1] with [Wlo09, §6, Step 2b] at µ = 1): the positive locus of the top member, blown up as one centre (its components may be infinitely many on a non-compact stage; the number of steps at a member is its maximal exponent, not the number of components).

Equations

• Hironaka.Manifold.BMOmod.step2bCenter T hfin hne = Hironaka.Manifold.BMOmod.positiveLocus T (Hironaka.Manifold.BMOmod.topMember T hfin hne)

theorem Hironaka.Manifold.BMOmod.isClosedSubmanifold_step2bCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.IsClosedSubmanifold ψ₀ (step2bCenter T hfin hne) 1

The centre is a closed submanifold of codimension 1 (a legal member of a CenterList, cons_codimOne_exists_diffeomorph).

theorem Hironaka.Manifold.BMOmod.step2bCenter_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : (step2bCenter T hfin hne).Nonempty

The centre is nonempty (the top member is active): no empty blow-up [Kol07, 32].

theorem Hironaka.Manifold.BMOmod.step2bCenter_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : step2bCenter T hfin hne ⊆ T.F.hyp (topMember T hfin hne)

The centre lies in the top member, inside the support of the boundary ("blow-ups at exceptional divisors", [Wlo09, Theorem 7.4.1]).

theorem Hironaka.Manifold.BMOmod.step2bCenter_subset_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : step2bCenter T hfin hne ⊆ T.F.support

theorem Hironaka.Manifold.BMOmod.hasSncWith_step2bCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.HypersurfaceFamily.HasSncWith ψ₀ T.F (step2bCenter T hfin hne) 1

The centre has simple normal crossings with E (the proof of [Kol07, Lemma 102]).

theorem Hironaka.Manifold.BMOmod.hasOnlyNormalCrossingsWith_step2bCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith T.F.idealSheaf ⋯.idealSheaf

Clause (3′) of [Kol07, Definition 66] for the centre, the first head clause of isOfOrderGe_cons_iff.

theorem Hironaka.Manifold.BMOmod.one_le_ordAlong_step2bCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (a : M.carrier) : a ∈ step2bCenter T hfin hne → ↑1 ≤ ⋯.idealSheaf.ordAlongIdeal T.I a

Clause (1′) of [Kol07, Definition 66] at the mark 1 for the centre, the second head clause of isOfOrderGe_cons_iff.