The local structure of a realising piece family and of its centres

At a point x of a piece piece c of a family realising an snc boundary E (Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean), the piece is the member E^{label c} near x: the other pieces of that label are closed and miss x (exists_affineOpens_piece_eq), so the vanishing ideal of the piece has, at x, the stalk of the member, the prime (z_c) in Kollár's coordinates (stalkIdeal_vanishingIdeal_piece). At a point of the centre of a centre S of the state exactly one face P ∈ S passes (Hironaka/Resolution/Algebraic/Monomial/Geometric/Nerve.lean), so the stalk of the centre is the stalk of the ideal of P, generated by the coordinates z_{c(i)} of the members of the pieces of P (exists_stalkIdeal_centerOf_eq_span): the centre has simple normal crossings with E in the sense of [Kol07, Definition 24] (4) (hasSncWith_centerOf) and is smooth over k (smooth_centerOf, Kollár's "in particular, Z is smooth"). These are conditions (2) and (3) of a smooth blow-up sequence of order ≥ m, [Kol07, Definition 66], for the blow-ups of Step 3; not in the sources as statements, Kollár taking them as evident for the intersections E^{j₁} ∩ ⋯ ∩ E^{j_r}.

Two general facts are used: the stalk of the vanishing ideal of a closed set depends only on the trace of the set on an affine neighbourhood (stalkIdeal_vanishingIdeal_congr), and a point outside a finite union of closed sets has an affine neighbourhood outside it (exists_affineOpens_of_not_mem_sup), both from Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/Center.lean.

A piece is its member near each of its points

def Hironaka.Monomial.PieceFamily.memberOf {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} (e : E.ι ≃o Fin Φ.nextLabel) (c : ℕ) (hc : c < Φ.nextComp) : E.ι

The member of the label of a live component.

Equations

• Φ.memberOf e c hc = e.symm ⟨Φ.label c, ⋯⟩

@[simp]

theorem Hironaka.Monomial.PieceFamily.coe_apply_memberOf {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} (e : E.ι ≃o Fin Φ.nextLabel) (c : ℕ) (hc : c < Φ.nextComp) : ↑(e (Φ.memberOf e c hc)) = Φ.label c

theorem Hironaka.Monomial.PieceFamily.exists_affineOpens_piece_eq {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) : ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∀ y ∈ ↑U, y ∈ Φ.piece c ↔ y ∈ (E.component (Φ.memberOf e c hc)).support

Near a point of a piece, the piece is the member of its label: an affine neighbourhood of the point avoiding the other pieces of the label (closed, and missing the point since two pieces of one label are disjoint).

theorem Hironaka.Monomial.PieceFamily.stalkIdeal_vanishingIdeal_piece {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {c : ℕ} (hc : c < Φ.nextComp) {x : ↥X} (hx : x ∈ Φ.piece c) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Φ.piece c)).stalkIdeal x = (E.component (Φ.memberOf e c hc)).stalkIdeal x

At a point of a piece, the vanishing ideal of the piece has the stalk of the member of its label: the piece is the member near the point, and the member's stalk is prime (the member is a regular subscheme, [Kol07, Definition 24] (1)), its own radical.

theorem Hironaka.Monomial.PieceFamily.exists_stalkIdeal_vanishingIdeal_piece_eq_span {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {c : ℕ} (hc : c < Φ.nextComp) {x : ↥X} (hx : x ∈ Φ.piece c) {nx : ℕ} {z : Fin nx → ↑(X.presheaf.stalk x)} (hz : E.IsSncAt x z) : ∃ (j : Fin nx), (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Φ.piece c)).stalkIdeal x = Ideal.span {z j}

Kollár's coordinate of a piece through x: with the snc coordinates z at x, the vanishing ideal of a piece through x has stalk (z_j) for the coordinate j of its member.

The stalk of a center

theorem Hironaka.Monomial.PieceFamily.exists_stalkIdeal_faceIdeal_eq_span {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {P : Finset ℕ} (hP : ∀ c ∈ P, c < Φ.nextComp) {x : ↥X} (hx : x ∈ Φ.faceSet P) {nx : ℕ} {z : Fin nx → ↑(X.presheaf.stalk x)} (hz : E.IsSncAt x z) : ∃ (s : Finset (Fin nx)), (Φ.faceIdeal P).stalkIdeal x = Ideal.span (z '' ↑s) ∧ (∀ c ∈ P, ∃ j ∈ s, (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Φ.piece c)).stalkIdeal x = Ideal.span {z j}) ∧ ∀ j ∈ s, ∃ c ∈ P, (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (Φ.piece c)).stalkIdeal x = Ideal.span {z j}

The ideal of a face P through x has, at x, the stalk generated by the coordinates of the members of the pieces of P (the computation of exists_stalkIdeal_disjoinCenter_eq_span in Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/Center.lean).

theorem Hironaka.Monomial.PieceFamily.stalkIdeal_centerOf_eq_faceIdeal {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) {P : Finset ℕ} (hP : P ∈ S) {x : ↥X} (hx : x ∈ Φ.faceSet P) : (Φ.centerOf S).stalkIdeal x = (Φ.faceIdeal P).stalkIdeal x

At a point of Z_P, P a face of a center S of the state, the stalk of the center is the stalk of the ideal of P: every other face of S misses the point (eq_of_mem_faceSet_of_isCenter), so its factor has the unit stalk.

theorem Hironaka.Monomial.PieceFamily.exists_stalkIdeal_centerOf_eq_span {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} {hV : Φ.IsValid n m} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) {x : ↥X} (hx : x ∈ (Φ.centerOf S).support) {nx : ℕ} {z : Fin nx → ↑(X.presheaf.stalk x)} (hz : E.IsSncAt x z) : ∃ (s : Finset (Fin nx)), (Φ.centerOf S).stalkIdeal x = Ideal.span (z '' ↑s)

At a point of the centre of a centre of the state, the stalk of the centre is generated by Kollár's coordinates of the pieces of the unique face through the point, as [Kol07, Definition 24] (4) requires.

theorem Hironaka.Monomial.PieceFamily.hasSncWith_centerOf {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} {hV : Φ.IsValid n m} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) : E.HasSncWith (Φ.centerOf S)

The centre of a centre of the state has simple normal crossings with E, [Kol07, Definition 24] (4); this is condition (1) of a smooth blow-up of order m in [Kol07, Definition 65].

theorem Hironaka.Monomial.PieceFamily.smooth_centerOf {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} {hV : Φ.IsValid n m} [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (hE : E.IsSnc) (hΦ : Φ.Realizes E e) {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hV).IsCenter S) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (Φ.centerOf S).subschemeι f)

The centre of a centre of the state is smooth over k (Kollár's "in particular, Z is smooth" after [Kol07, Definition 24]; smooth_of_hasSncWith of Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/Center.lean).