Simple normal crossings families of closed subspaces and their divisors

The boundary predicate of the resolution theorem, ClosedSubspace.IsSncBoundary, is Kollár's Definition 24 read on the stalks of a locally finite family of closed subspaces [Kol07, Definition 24]: the inverse image of the singular locus is the support of a simple normal crossings divisor E of the resolving space ([Kol07, Theorem 45 (3)]; [Wlo09, Theorem 2.0.1 (2)]). This module names the family behind that definition and builds its divisor, so that a boundary is produced from a family by one application:

• ClosedSubspace.IsSncFamily H: a family H : ι → ClosedSubspace X is locally finite and, at every point x, a regular system of parameters of 𝒪_{X,x} cuts out each member through x by one parameter, distinct members by distinct parameters — the inner clauses of IsSncBoundaryWith without the product clause on E and the clause on D;
• ClosedSubspace.divisorOf H hH: the reduced divisor of a locally finite family — the ideal sheaf with stalk at x the product of the members' stalk ideals over the finitely many members through x (IdealSheaf.ofStalks), Kollár's E = Σ Eᵢ;
• the snc condition presupposes a regular system of parameters at every point, so an snc family lives on a non-singular space (IsSncBoundary.space_isNonsingular, Hironaka/AnalyticSpace/SncBoundaryChart.lean).

The support of the divisor, its boundary predicate, the bridge to the hypersurface families of a manifold, transport along morphisms and locality are in Hironaka/AnalyticSpace/SncFamilyDivisor.lean, SncFamilyManifold.lean, SncFamilyTransport.lean and SncBoundaryChart.lean. Used by Hironaka/AnalyticSpace/Glue/OverFamily.lean and the modules just named.

def Manifold.IdealSheaf.stalkIdealMonoidHom {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (x : ↑X) : IdealSheaf 𝒪 →* Ideal ↑(𝒪.presheaf.stalk x)

The stalk ideal at x as a monoid homomorphism IdealSheaf 𝒪 →* Ideal 𝒪ₓ: 1 = ⊤ and products go to products (stalkIdeal_one, stalkIdeal_mul, Hironaka/Manifold/IdealSheaf/).

Equations

• Manifold.IdealSheaf.stalkIdealMonoidHom x = { toFun := fun (J : Manifold.IdealSheaf 𝒪) => J.stalkIdeal x, map_one' := ⋯, map_mul' := ⋯ }

def AnalyticSpace.ClosedSubspace.IsSncFamily {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} (H : ι → X.ClosedSubspace) : Prop

A simple normal crossings family of closed subspaces ([Kol07, Definition 24 (1)–(3)]; Hironaka's normal crossings on global components, [Hir64, Ch. 0, §5, Definition 2]): the family is locally finite, and at every point x a regular system of parameters z₁, …, zₙ of 𝒪_{X,x} (n generators of the maximal ideal, n the Krull dimension) cuts out each member through x by one parameter, distinct members by distinct parameters. The body of IsSncBoundaryWith without its product clause on the divisor E and its clause on D: the family behind the boundary predicate, exposed as data.

Equations

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

theorem AnalyticSpace.ClosedSubspace.hasLocalGenerators_prod_of_locallyFinite {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} (H : ι → X.ClosedSubspace) (hH : LocallyFinite fun (j : ι) => Manifold.IdealSheaf.support (H j)) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑X.toTopCat) => ∏ j ∈ ⋯.toFinset, Manifold.IdealSheaf.stalkIdeal (H j) x

The stalk ideals of the members through a point have local generators: the finite product of the members' local generators on a neighbourhood meeting finitely many members.

noncomputable def AnalyticSpace.ClosedSubspace.divisorOf {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} (H : ι → X.ClosedSubspace) (hH : LocallyFinite fun (j : ι) => Manifold.IdealSheaf.support (H j)) : X.ClosedSubspace

The reduced divisor of a locally finite family of closed subspaces (Kollár's E = Σ Eᵢ, [Kol07, Definition 24]): the ideal sheaf whose stalk at x is the product of the stalk ideals of the finitely many members through x (IdealSheaf.ofStalks); the empty family gives the unit ideal ⊤ (the empty subspace).

Equations

• AnalyticSpace.ClosedSubspace.divisorOf H hH = Manifold.IdealSheaf.ofStalks X.𝒪 (fun (x : ↑X.toTopCat) => ∏ j ∈ ⋯.toFinset, Manifold.IdealSheaf.stalkIdeal (H j) x) ⋯

theorem AnalyticSpace.ClosedSubspace.stalkIdeal_divisorOf {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} (H : ι → X.ClosedSubspace) (hH : LocallyFinite fun (j : ι) => Manifold.IdealSheaf.support (H j)) (x : ↑↑X.toPresheafedSpace) : Manifold.IdealSheaf.stalkIdeal (divisorOf H hH) x = ∏ j ∈ ⋯.toFinset, Manifold.IdealSheaf.stalkIdeal (H j) x

The stalk of the divisor at x is the product over the members through x.

theorem AnalyticSpace.ClosedSubspace.divisorOf_of_isEmpty {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} [IsEmpty ι] (H : ι → X.ClosedSubspace) (hH : LocallyFinite fun (j : ι) => Manifold.IdealSheaf.support (H j)) : divisorOf H hH = ⊤

The boundary case: the empty family has the unit ideal — the empty subspace — as its divisor.

noncomputable def Manifold.HypersurfaceFamily.toClosedSubspaces {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : AnalyticManifold K E} (F : HypersurfaceFamily M.carrier) (h : ∀ (j : F.ι), IsClosedSubmanifold ψ (F.hyp j) 1) : F.ι → (AnalyticSpace.toSpace ψ M).ClosedSubspace

The members of a hypersurface family as closed subspaces of Sp(M), through their ideal sheaves.

Equations

• F.toClosedSubspaces h j = ⋯.idealSheaf