The monomial ideal of a piece family

For a piece family realising a boundary family with simple normal crossings, every piece is a closed hypersurface, a clopen part of its member, and so has a reduced ideal sheaf 𝓘_{piece c}. The monomial ideal of the family is the finite product ∏_{c < nextComp} 𝓘_{piece c}^{a c}, Kollár's 𝒪(−∑ aⱼ Eʲ) of [Kol07, 111, Step 3] with the exponents read on the connected components of the members as in [Kol07, Definition–Lemma 110] (the form used by BMO/MonomialPart.lean). Its order at a point is the exponent sum of the face through the point (ord_monomialIdeal): the stalk is generated by the monomial ∏_{c ∋ x} z_c^{a c} in generators of the pieces' stalks, each of order one, and the order function of the regular analytic stalk is multiplicative. The file also derives the invariants of the combinatorial state from the geometry (valid_of_realizes): the faces are nonempty sets of pieces with a common point, closed under nonempty subsets, of cardinality at most the dimension n (at most n members of a family with simple normal crossings pass through a point, [Kol07, Definition 24]), with pairwise distinct labels.

A hypersurface's stalk ideal is principal with a generator of order one

theorem Manifold.IsClosedSubmanifold.exists_generator_stalkIdeal_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {S : Set N.carrier} (hS : IsClosedSubmanifold ψ₀ S 1) {x : N.carrier} (hx : x ∈ S) : ∃ (f : ↑((structureSheaf 𝕜 E N.carrier).presheaf.stalk x)), hS.idealSheaf.stalkIdeal x = Ideal.span {f} ∧ IsLocalRing.ordElem f = 1

At a point of a closed hypersurface the stalk of its ideal sheaf is generated by one element of order exactly one, the coordinate of a chart adapted to the hypersurface.

theorem Hironaka.Manifold.BMO.ordElem_finset_prod_pow {R : Type u_2} [CommRing R] [IsLocalRing R] (hmul : ∀ (f g : R), IsLocalRing.ordElem (f * g) = IsLocalRing.ordElem f + IsLocalRing.ordElem g) {ι : Type u_3} (s : Finset ι) (f : ι → R) (a : ι → ℕ) : IsLocalRing.ordElem (∏ i ∈ s, f i ^ a i) = ∑ i ∈ s, ↑(a i) * IsLocalRing.ordElem (f i)

The order of a finite product of powers, when the order function is multiplicative.

Live pieces are closed hypersurfaces

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.exists_isOpen_piece_eq {𝕜 : 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) {c : ℕ} (hc : c < Φ.nextComp) : ∃ (O : Set N.carrier), IsOpen O ∧ Φ.piece c = F.hyp (e ⟨Φ.label c, ⋯⟩) ∩ O

A piece is the trace of its member on the open complement of the other pieces with the same label.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.isClosedSubmanifold_piece {𝕜 : 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.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (c : Fin Φ.nextComp) : Manifold.IsClosedSubmanifold ψ₀ (Φ.piece ↑c) 1

A piece of a family realising a boundary family with simple normal crossings is a closed hypersurface, being a clopen part of its member.

The monomial ideal

noncomputable def Hironaka.Manifold.BMO.PieceFamily.pieceIdeal {𝕜 : 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.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (c : Fin Φ.nextComp) : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E N.carrier)

The reduced ideal sheaf 𝓘_{piece c} of a piece.

Equations

• Φ.pieceIdeal hF hΦ c = ⋯.idealSheaf

noncomputable def Hironaka.Manifold.BMO.PieceFamily.monomialIdeal {𝕜 : 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.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E N.carrier)

The monomial ideal of the family, ∏_{c < nextComp} 𝓘_{piece c}^{a c}: Kollár's monomial ideal 𝒪(−∑ aⱼ Eʲ) of [Kol07, 111, Step 3], with the exponents read on the connected components of the members ([Kol07, Definition–Lemma 110]).

Equations

• Φ.monomialIdeal hF hΦ = ∏ c : Fin Φ.nextComp, Φ.pieceIdeal hF hΦ c ^ Φ.a ↑c

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_pieceIdeal_of_notMem {𝕜 : 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.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) {c : Fin Φ.nextComp} {x : N.carrier} (hx : x ∉ Φ.piece ↑c) : (Φ.pieceIdeal hF hΦ c).stalkIdeal x = ⊤

theorem Hironaka.Manifold.BMO.PieceFamily.exists_generator_stalkIdeal_pieceIdeal {𝕜 : 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.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) {c : Fin Φ.nextComp} {x : N.carrier} (hx : x ∈ Φ.piece ↑c) : ∃ (f : ↑((Manifold.structureSheaf 𝕜 E N.carrier).presheaf.stalk x)), (Φ.pieceIdeal hF hΦ c).stalkIdeal x = Ideal.span {f} ∧ IsLocalRing.ordElem f = 1

theorem Hironaka.Manifold.BMO.PieceFamily.total_faceAt_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (x : N.carrier) : Φ.total (Φ.faceAt x) = ∑ c : Fin Φ.nextComp with x ∈ Φ.piece ↑c, Φ.a ↑c

The exponent sum of the face through x, as a sum over the pieces containing x.

theorem Hironaka.Manifold.BMO.PieceFamily.ord_monomialIdeal {𝕜 : 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.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (x : N.carrier) : (Φ.monomialIdeal hF hΦ).ord x = ↑(Φ.total (Φ.faceAt x))

The order of the monomial ideal at x is the exponent sum of the face through x: the stalk is generated by ∏_{c ∋ x} z_c^{a c} with each z_c of order one, and the order function of the analytic stalk is multiplicative.

The six invariants of the state from the geometry

theorem Hironaka.Manifold.BMO.PieceFamily.valid_of_realizes {𝕜 : 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.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) {m : ℕ} (hm : 1 ≤ m) : Φ.IsValid n m

A family realising a boundary family with simple normal crossings satisfies the invariants of the combinatorial state for every mark m ≥ 1: in particular a face has at most n pieces, since at most n members of a family with simple normal crossings pass through a point (Kol07, Definition 24).