The centres of the monomial procedure are closed submanifolds

A centre of the combinatorial state is a set S of faces of the nerve with a common label tuple L (Hironaka.Monomial.MonomialState.IsCenter); Kollár's choice at level r in [Kol07, 111, Step 3] is one (MonomialState.isCenter_choice). This file proves that its locus centerOf S = ⋃_{P ∈ S} ⋂_{c ∈ P} piece c is a closed submanifold of codimension r, the number of labels, having simple normal crossings with the boundary family, and that the monomial ideal has order ≥ m along it when every face of S has exponent sum ≥ m, as the order clause of [Kol07, Definition 66 (4′)] requires of a centre.

The locus is a clopen part of the r-fold intersection ⋂_{ℓ ∈ L} E^{e ℓ} of the members of the tuple: through a point of the intersection passes exactly one piece of each label, so the point lies in the locus of exactly one face with labels L, and the faces with labels L outside S cut out a closed set whose complement is the open part. The intersection is a closed submanifold of codimension r with simple normal crossings with the family (in a chart of simple normal crossings it is a coordinate subspace), hence so is the clopen part. Near a point of the locus of P ∈ S the locus is contained in every piece of P, so each 𝓘_{piece c}, c ∈ P, has order ≥ 1 along it and the monomial ideal has order at least the exponent sum of P.

Faces of a centre

theorem Hironaka.Manifold.BMO.PieceFamily.subset_nerve_of_isCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) : S ⊆ Φ.nerve

The faces of a centre of the state are faces of the nerve.

theorem Hironaka.Manifold.BMO.PieceFamily.labels_eq_of_isCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) {P Q : Finset ℕ} (hP : P ∈ S) (hQ : Q ∈ S) : Φ.labels P = Φ.labels Q

The faces of a centre have a common label tuple.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.eq_of_labels_eq_of_mem_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) {P Q : Finset ℕ} (hP : P ∈ Φ.nerve) (hQ : Q ∈ Φ.nerve) (hl : Φ.labels P = Φ.labels Q) {x : N.carrier} (hxP : x ∈ Φ.faceSet P) (hxQ : x ∈ Φ.faceSet Q) : P = Q

Two faces of the nerve with the same labels and a common point are equal, since through a point passes at most one piece with a given label.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.eq_of_mem_faceSet_of_isCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) {P Q : Finset ℕ} (hP : P ∈ S) (hQ : Q ∈ S) {x : N.carrier} (hxP : x ∈ Φ.faceSet P) (hxQ : x ∈ Φ.faceSet Q) : P = Q

A point of the locus of a centre lies in the locus of exactly one of its faces.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.card_eq_faceCard_of_isCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) {P : Finset ℕ} (hP : P ∈ S) : P.card = faceCard S

All faces of a nonempty centre have the cardinality faceCard S.

theorem Hironaka.Manifold.BMO.PieceFamily.centerOf_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) (hne : S.Nonempty) : (Φ.centerOf S).Nonempty

A nonempty centre of the state has a nonempty locus.

The locus as a clopen part of the members' intersection

theorem Hironaka.Manifold.BMO.PieceFamily.mem_meetLocus_subfamily_card_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {F : Manifold.HypersurfaceFamily N.carrier} (Ls : Finset F.ι) {x : N.carrier} : x ∈ (F.subfamily fun (x : F.ι) => x ∈ Ls).meetLocus Ls.card ↔ ∀ j ∈ Ls, x ∈ F.hyp j

The card-fold meet locus of a finite subfamily is the intersection of its members.

theorem Hironaka.Manifold.BMO.PieceFamily.meetLocus_subfamily_card_succ_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {F : Manifold.HypersurfaceFamily N.carrier} (Ls : Finset F.ι) : (F.subfamily fun (x : F.ι) => x ∈ Ls).meetLocus (Ls.card + 1) = ∅

No point lies on card + 1 members of a finite subfamily.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.exists_centerOf_eq_meetLocus_inter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hne : S.Nonempty) : ∃ (Ls : Finset F.ι) (O : Set N.carrier), Ls.card = faceCard S ∧ IsOpen O ∧ Φ.centerOf S = (F.subfamily fun (x : F.ι) => x ∈ Ls).meetLocus Ls.card ∩ O

The locus of a nonempty centre of the state is a clopen part of the intersection of the members of its label tuple: it is the intersection of the members Ls of the tuple with the open complement of the loci of the faces with the same labels that are not in the centre.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.isClosedSubmanifold_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)

The locus of a centre of the state is a closed submanifold whose codimension is the common cardinality of its faces ([Kol07, 111, Step 3]: the centre E^{j₁} ∩ ⋯ ∩ E^{j_r} is smooth of codimension r).

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.hasSncWith_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) : Manifold.HypersurfaceFamily.HasSncWith ψ₀ F (Φ.centerOf S) (faceCard S)

The boundary family has simple normal crossings with the locus of a centre of the state, the condition [Kol07, Definition 66 (3′)] imposes on a centre.

The order of the monomial ideal along the locus

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.exists_mem_nhds_centerOf_inter_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) {P : Finset ℕ} (hP : P ∈ S) {x : N.carrier} (hx : x ∈ Φ.faceSet P) : ∃ U ∈ nhds x, Φ.centerOf S ∩ U ⊆ Φ.faceSet P

Near a point of the locus of the face P ∈ S, the locus of the centre S is contained in the locus of P: the other faces of the centre miss the point.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.le_ordAlongIdeal_monomialIdeal_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) (hge : ∀ P ∈ S, m ≤ Φ.total P) {x : N.carrier} (hx : x ∈ Φ.centerOf S) : ↑m ≤ hZ.idealSheaf.ordAlongIdeal (Φ.monomialIdeal hF hΦ) x

The monomial ideal has order ≥ m along the locus of a centre at every point of the locus, when every face of the centre has exponent sum ≥ m ([Kol07, Definition 66 (4′)]): near a point of the locus of P the locus lies in every piece of P, so each factor 𝓘_{piece c}^{a c}, c ∈ P, has order ≥ a c along it.