The nerve of a realising piece family: faces, validity, the centres

The combinatorial layer of the geometric realisation. For a piece family Φ realising an snc boundary E (Realizes E e) on a smooth k-scheme of dimension ≤ n, the faces of its nerve are the sets of components with a common point, and they satisfy the six invariants of the combinatorial state, so that toState is defined (valid_of_realizes):

• mem_nerve_iff: a face is a nonempty set of live components with a common point;
• injOn_label_of_mem_nerve: the components of a face have distinct labels, because two pieces of one label are disjoint (Realizes.disjoint);
• card_le_of_mem_nerve: a face has at most n elements. Its labels are labels of members through a common point x, at most dim 𝒪_{X,x} of them by the injective assignment of coordinates in [Kol07, Definition 24] (3), and dim 𝒪_{X,x} ≤ n on a smooth scheme of relative dimension ≤ n;
• support_faceIdeal, support_centerOf, centerOf_ne_top: the centre of a finset of faces is the ideal sheaf of the union of their intersections Z_P, nonempty for faces of the nerve (so the blow-ups of the geometric Step 3 are never the empty blow-ups of [Kol07, 32]);
• eq_of_mem_faceSet_of_isCenter: the intersections Z_P, P ∈ S, of a centre of the state are pairwise disjoint. Two faces of a centre through a common point are equal (MonomialState.eq_of_isCenter_of_subset, the faces of a centre having a common label set).

Not in the sources; these are the facts that connect the combinatorial state to the geometry. The local structure of the pieces and centres is Hironaka/Resolution/Algebraic/Monomial/Geometric/Local.lean.

Faces

theorem Hironaka.Monomial.PieceFamily.faceSet_ne_bot_iff {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (T : Finset ℕ) : Φ.faceSet T ≠ ⊥ ↔ ∃ (x : ↥X), ∀ c ∈ T, x ∈ Φ.piece c

A face set is nonempty iff the components have a common point.

theorem Hironaka.Monomial.PieceFamily.mem_nerve_iff {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (T : Finset ℕ) : T ∈ Φ.nerve ↔ T ⊆ Finset.range Φ.nextComp ∧ T.Nonempty ∧ ∃ (x : ↥X), ∀ c ∈ T, x ∈ Φ.piece c

The nerve consists of the nonempty sets of live components with a common point.

theorem Hironaka.Monomial.PieceFamily.exists_mem_faceSet_of_mem_nerve {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {T : Finset ℕ} (hT : T ∈ Φ.nerve) : ∃ (x : ↥X), x ∈ Φ.faceSet T

theorem Hironaka.Monomial.PieceFamily.lt_nextComp_of_mem_nerve {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {T : Finset ℕ} (hT : T ∈ Φ.nerve) {c : ℕ} (hc : c ∈ T) : c < Φ.nextComp

theorem Hironaka.Monomial.PieceFamily.mem_nerve_of_mem_faceSet {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {T : Finset ℕ} (hT : T ⊆ Finset.range Φ.nextComp) (hne : T.Nonempty) {x : ↥X} (hx : x ∈ Φ.faceSet T) : T ∈ Φ.nerve

Realising families: labels and the dimension bound

theorem Hironaka.Monomial.PieceFamily.not_mem_piece_of_label_eq {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hΦ : Φ.Realizes E e) {c c' : ℕ} (hc : c < Φ.nextComp) (hc' : c' < Φ.nextComp) (hne : c ≠ c') (hlab : Φ.label c = Φ.label c') {x : ↥X} (hx : x ∈ Φ.piece c) (hx' : x ∈ Φ.piece c') : False

Two distinct pieces of one label have no common point (Realizes.disjoint).

theorem Hironaka.Monomial.PieceFamily.injOn_label_of_mem_nerve {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hΦ : Φ.Realizes E e) {T : Finset ℕ} (hT : T ∈ Φ.nerve) : Set.InjOn Φ.label ↑T

A face of the nerve has injective labels: its components have a common point, and two pieces of one label are disjoint.

theorem Hironaka.Monomial.PieceFamily.mem_support_component_of_mem_piece {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hΦ : Φ.Realizes E e) {c : ℕ} (hc : c < Φ.nextComp) {x : ↥X} (hx : x ∈ Φ.piece c) : x ∈ (E.component (e.symm ⟨Φ.label c, ⋯⟩)).support

A point of a piece lies on the member of the piece's label.

theorem Hironaka.Monomial.PieceFamily.card_filter_mem_support_le {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) {n' : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension n' f] (hE : E.IsSnc) (x : ↥X) : {i : E.ι | x ∈ (E.component i).support}.card ≤ n'

The number of members of an snc boundary through a point is at most the dimension of the local ring there (the injective assignment of coordinates, [Kol07, Definition 24] (3)), which is at most the relative dimension of a smooth scheme over a perfect field.

theorem Hironaka.Monomial.PieceFamily.card_le_of_mem_nerve {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [PerfectField k] (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {n : ℕ} (hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) {T : Finset ℕ} (hT : T ∈ Φ.nerve) : T.card ≤ n

A face of the nerve of a family realising an snc boundary on a scheme of dimension ≤ n has at most n elements: at most n = dim X members pass through a point, by c(i) ≠ c(i') in [Kol07, Definition 24] (3).

theorem Hironaka.Monomial.PieceFamily.valid_of_realizes {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [PerfectField k] (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {n m : ℕ} (hm : 1 ≤ m) (hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) : Φ.IsValid n m

Under the geometric hypotheses the family's data are Valid: faces are nonempty sets of live components (mem_nerve), labels are below nextLabel (label_lt), the nerve is down-closed (a subset of a face has a larger face set, faceSet_anti), faces have at most n elements (card_le_of_mem_nerve) and injective labels (injOn_label_of_mem_nerve).

Centres: supports

theorem Hironaka.Monomial.PieceFamily.support_faceIdeal {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (P : Finset ℕ) : (Φ.faceIdeal P).support = Φ.faceSet P

The support of the ideal of a face is its face set Z_P.

theorem Hironaka.Monomial.PieceFamily.support_centerOf {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (S : Finset (Finset ℕ)) : (Φ.centerOf S).support = S.sup Φ.faceSet

The support of the center of a finset of faces is the union of their intersections.

theorem Hironaka.Monomial.PieceFamily.mem_support_centerOf_iff {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) (S : Finset (Finset ℕ)) (x : ↥X) : x ∈ (Φ.centerOf S).support ↔ ∃ P ∈ S, x ∈ Φ.faceSet P

theorem Hironaka.Monomial.PieceFamily.faceSet_le_support_centerOf {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {S : Finset (Finset ℕ)} {P : Finset ℕ} (hP : P ∈ S) : Φ.faceSet P ≤ (Φ.centerOf S).support

theorem Hironaka.Monomial.PieceFamily.centerOf_ne_top {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {S : Finset (Finset ℕ)} (hS : S ⊆ Φ.nerve) (hne : S.Nonempty) : Φ.centerOf S ≠ ⊤

The centre of a nonempty finset of faces of the nerve is a nonempty closed subscheme: the blow-ups of the procedure are not the empty blow-ups of [Kol07, 32].

Centres of the state: the faces are pairwise disjoint

theorem Hironaka.Monomial.PieceFamily.eq_of_mem_faceSet_of_isCenter {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {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) {x : ↥X} (hxP : x ∈ Φ.faceSet P) (hxQ : x ∈ Φ.faceSet Q) : P = Q

Two faces of a centre of the state through a common point are equal: their union is a face, and MonomialState.eq_of_isCenter_of_subset applies (the faces of a centre have a common label set and faces have injective labels).

theorem Hironaka.Monomial.PieceFamily.existsUnique_mem_faceSet_of_isCenter {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) {x : ↥X} (hx : x ∈ (Φ.centerOf S).support) : ∃! P : Finset ℕ, P ∈ S ∧ x ∈ Φ.faceSet P

A point of the centre of a centre of the state lies on exactly one of its faces.