The monomial part of an ideal sheaf with respect to a boundary family

For a triple (X, I, E), Kollár writes I = M(I) · N(I) with M(I) = 𝒪_X(−∑ cᵢ Eⁱ) the monomial part, a product of powers of the ideal sheaves of the members Eⁱ of the boundary, and N(I) the nonmonomial part, whose cosupport contains no member [Kol07, Definition–Lemma 110]. This file defines the monomial part on an analytic manifold, for an ideal sheaf I and a boundary family F with simple normal crossings, in a finer form: the product runs over the connected components D of the members E^j, each contributing 𝓘_D^{ord_D I}, where 𝓘_D is the reduced ideal sheaf of D and ord_D I is the order of I along D (constant along the connected component; it is read at one point). Kollár's members are not assumed irreducible, and on a manifold a member need not be connected; reading the exponent on each component separately is what makes the monomial part commute with restriction to open subsets and with local analytic isomorphisms, as the functor of [Kol07, Theorem 107 (2)] requires.

The components are indexed by ComponentIndex F = Σ j, ConnectedComponents (E^j). A member may have infinitely many components, but the family of all component sets is locally finite (componentSet_locallyFinite), so M(I) is the locally finite product of the component factors (IdealSheaf.locallyFiniteProduct, BMO/LocallyFiniteProduct.lean) rather than a finite product. The analytic counterpart of Hironaka.BMO.monomialPart.

@[reducible, inline]

abbrev Hironaka.Manifold.BMO.ComponentIndex {M : Type u} [TopologicalSpace M] (F : Manifold.HypersurfaceFamily M) : Type u

The index type of the factors of the monomial part: a member j of the boundary family together with one of the connected components of E^j. These are the components D of [Kol07, Definition–Lemma 110], taken one connected component at a time.

Equations

• Hironaka.Manifold.BMO.ComponentIndex F = ((j : F.ι) × ConnectedComponents ↑(F.hyp j))

def Hironaka.Manifold.BMO.componentSet {M : Type u} [TopologicalSpace M] (F : Manifold.HypersurfaceFamily M) (i : ComponentIndex F) : Set M

The underlying set of the component i = ⟨j, C⟩: the image in M of the connected component C of the member E^j (the preimage of {C} under ConnectedComponents.mk).

Equations

• Hironaka.Manifold.BMO.componentSet F i = Subtype.val '' ConnectedComponents.mk ⁻¹' {i.snd}

theorem Hironaka.Manifold.BMO.componentSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (i : ComponentIndex F) : Manifold.IsClosedSubmanifold ψ (componentSet F i) 1

Each component i = ⟨j, C⟩ of a boundary family with simple normal crossings is a closed submanifold of M of codimension one: the member is one, and a connected component of a closed submanifold is again a closed submanifold.

noncomputable def Hironaka.Manifold.BMO.componentIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (i : ComponentIndex F) : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)

The reduced ideal sheaf 𝓘_D of the component D = i.

Equations

• Hironaka.Manifold.BMO.componentIdeal F hF i = ⋯.idealSheaf

noncomputable def Hironaka.Manifold.BMO.componentExponent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (i : ComponentIndex F) : ℕ

The exponent ord_D I of the component D = i: the order of I along D, which is constant along the connected component and is read at the representative i.2.out, as a natural number. For an ideal sheaf that is nonzero at every point (every ideal of a triple is, [Kol07, Definition 31]) the order along D is finite, so passing to ℕ loses nothing; for a zero stalk the value ⊤ would be read as 0.

Equations

• Hironaka.Manifold.BMO.componentExponent F hF I i = ((Hironaka.Manifold.BMO.componentIdeal F hF i).genericOrdAlong I ↑(Quotient.out i.snd)).toNat

noncomputable def Hironaka.Manifold.BMO.componentFactor {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (i : ComponentIndex F) : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)

The factor 𝓘_D ^ (ord_D I) of the monomial part at the component D = i.

Equations

• Hironaka.Manifold.BMO.componentFactor F hF I i = Hironaka.Manifold.BMO.componentIdeal F hF i ^ Hironaka.Manifold.BMO.componentExponent F hF I i

theorem Hironaka.Manifold.BMO.componentSet_locallyFinite {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) : LocallyFinite (componentSet F)

The component sets form a locally finite family of subsets of M: the members E^j are locally finite, the connected components of each member are locally finite in M, and each component lies in its member (locallyFinite_sigma). This is the finiteness that makes the monomial part an ideal sheaf on a non-compact manifold, where a member may have infinitely many components.

theorem Hironaka.Manifold.BMO.componentFactor_stalkIdeal_top_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (i : ComponentIndex F) (x : M) (hx : x ∉ componentSet F i) : (componentFactor F hF I i).stalkIdeal x = ⊤

Off its component, the factor 𝓘_D ^ (ord_D I) is the unit ideal, since the ideal sheaf of a closed submanifold is the unit ideal off the submanifold. This is the controlling-set hypothesis of the locally finite product.

noncomputable def Hironaka.Manifold.BMO.monomialPart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)

The monomial part M(I) = ∏_D 𝓘_D ^ (ord_D I) of I with respect to the boundary family F with simple normal crossings: the locally finite product of the component factors over all components D of the members of F ([Kol07, Definition–Lemma 110], with the exponents read on the connected components of the members; see the module docstring). The same decomposition I = M(I) · N(I) appears in [BM08, (5.2)] and in [Wlo05, Proposition 3.0.8, Step 2 of the proof]. The analytic counterpart of Hironaka.BMO.monomialPart.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hironaka.Manifold.BMO.stalkIdeal_monomialPart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (x : M) : (monomialPart F hF I).stalkIdeal x = ∏ i ∈ Manifold.IdealSheaf.activeFinset (componentSet F) ⋯ x, (componentFactor F hF I i).stalkIdeal x

The stalk of the monomial part at x is the finite product of the factors of the components passing through x.