Simple normal crossings divisors: constructions and the elementary lemmas

The constructions on the data of a hypersurface family — the empty family (HypersurfaceFamily.empty), Kollár's total transform under a blowing-up (HypersurfaceFamily.totalTransform: the strict transforms of the components, strictTransformSet, followed by the exceptional divisor, appended last in the order [Kol07, Definition 25]; Włodarczyk's exceptional divisor of a composite of blow-ups [Wlo09, Remark (1) after Theorem 2.0.3]) and the restriction to a subset (HypersurfaceFamily.restrict, Kollár's E|_Z [Kol07, Definition 24]) — and the elementary lemmas: the projections of IsSnc and IsSncChartAt (the clauses of Kollár's definition of a simple normal crossing divisor, [Kol07, Definition 24]), the closedness of the support and the finiteness of the components meeting a compact set (local finiteness), the empty divisor (snc, and every closed submanifold has simple normal crossings with it), the components of the total transform [Kol07, Definition 25] and of the restriction, the position of the exceptional divisor in the order, the support of the total transform (the set of points of Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) is f⁻¹(E) ∪ f⁻¹(D), [Hir64, Main Theorem II'(N) (iii), p. 156]), from the inclusions between the strict transform and the preimage, and the restriction of an snc chart to an open set. These are the lemmas the rest of Hironaka/Manifold/Snc/ and the boundary bookkeeping of the blow-up sequences rest on.

It also states Hironaka's normal crossings [Hir64, Definition 2, p. 141] at the level of stalks, HasOnlyNormalCrossingsWith and HasOnlyNormalCrossings, which read the irreducible components through the minimal primes of the stalk (the local branches); the analytic main theorems state their boundary clauses through the global components instead (IdealSheaf.IsSncBoundary).

The empty family, the total transform, the restriction

def Manifold.HypersurfaceFamily.empty (M : Type u) : HypersurfaceFamily M

The empty divisor E = ∅ (no components).

Equations

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

def Manifold.HypersurfaceFamily.totalTransform {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) (F : HypersurfaceFamily M) : HypersurfaceFamily M'

The total transform of the family F under the blowing-up π : M' → M with centre Y ([Kol07, Definition 25]; [Wlo09, Remark (1) after Theorem 2.0.3]): the strict transforms of the components (strictTransformSet) followed by the exceptional divisor π⁻¹(Y), appended last in the order.

Equations

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

def Manifold.HypersurfaceFamily.restrict {M : Type u} (F : HypersurfaceFamily M) (H : Set M) : HypersurfaceFamily ↑H

The restriction F|_H = (E^j ∩ H)_j of the family to a subset H, as a family on the subspace H (Kollár's E|_Z, [Kol07, Definition 24]).

Equations

• F.restrict H = { ι := F.ι, countable := ⋯, linearOrder := F.linearOrder, hyp := fun (j : F.ι) => Subtype.val ⁻¹' F.hyp j }

The components of the total transform and of the restriction

theorem Manifold.HypersurfaceFamily.totalTransform_hyp_inl {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) (F : HypersurfaceFamily M) (j : F.ι) : (totalTransform π Y F).hyp (toLex (Sum.inl j)) = strictTransformSet π Y (F.hyp j)

The components of the total transform indexed by F are the strict transforms of the components of F [Kol07, Definition 25].

theorem Manifold.HypersurfaceFamily.totalTransform_hyp_inr {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) (F : HypersurfaceFamily M) : (totalTransform π Y F).hyp (toLex (Sum.inr PUnit.unit)) = π ⁻¹' Y

The last component of the total transform is the exceptional divisor π⁻¹(Y) [Kol07, Definition 25].

theorem Manifold.HypersurfaceFamily.totalTransform_inl_lt_inr {M : Type u} (F : HypersurfaceFamily M) (j : F.ι) : toLex (Sum.inl j) < toLex (Sum.inr PUnit.unit)

The exceptional divisor comes after every strict transform in the order of the total transform.

theorem Manifold.HypersurfaceFamily.restrict_hyp {M : Type u} (F : HypersurfaceFamily M) (H : Set M) (j : F.ι) : (F.restrict H).hyp j = Subtype.val ⁻¹' F.hyp j

The components of the restriction are the traces of the components.

The projections of IsSnc and IsSncChartAt

theorem Manifold.HypersurfaceFamily.IsSnc.isClosedSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (j : F.ι) : IsClosedSubmanifold ψ (F.hyp j) 1

The components of an snc divisor are closed smooth hypersurfaces [Kol07, Definition 24].

theorem Manifold.HypersurfaceFamily.IsSnc.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 : HypersurfaceFamily M} (hF : IsSnc ψ F) : LocallyFinite F.hyp

The components of an snc divisor form a locally finite family.

theorem Manifold.HypersurfaceFamily.IsSnc.exists_isSncChartAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (a : M) : ∃ (φ : OpenPartialHomeomorph M E) (c : { j : F.ι // a ∈ F.hyp j } → Fin n), IsSncChartAt ψ F φ a c

Every point has an snc chart [Kol07, Definition 24 (1)–(3)].

theorem Manifold.HypersurfaceFamily.IsSncChartAt.mem_maximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (h : IsSncChartAt ψ F φ a c) : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M

An snc chart lies in the maximal analytic atlas.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.mem_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (h : IsSncChartAt ψ F φ a c) : a ∈ φ.source

An snc chart at a contains a in its source.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.mem_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (h : IsSncChartAt ψ F φ a c) (j : { j : F.ι // a ∈ F.hyp j }) {x : M} (hx : x ∈ φ.source) : x ∈ F.hyp ↑j ↔ ψ (↑φ x) (c j) = 0

On the source of an snc chart at a, a component through a is the coordinate hyperplane of its index [Kol07, Definition 24 (2)].

theorem Manifold.HypersurfaceFamily.IsSncChartAt.injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (h : IsSncChartAt ψ F φ a c) : Function.Injective c

Distinct components through a have distinct coordinate indices [Kol07, Definition 24 (3)].

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

The support of an snc divisor is closed: a locally finite union of closed sets.

theorem Manifold.HypersurfaceFamily.IsSnc.finite_of_isCompact {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {K : Set M} (hK : IsCompact K) : {j : F.ι | (F.hyp j ∩ K).Nonempty}.Finite

Only finitely many components meet a compact set (local finiteness).

The empty divisor

theorem Manifold.HypersurfaceFamily.isSnc_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] : IsSnc ψ (empty M)

The empty family is a simple normal crossings divisor.

theorem Manifold.HypersurfaceFamily.hasSncWith_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : HasSncWith ψ (empty M) Y c

Every closed submanifold has simple normal crossings with the empty divisor.

Simple normal crossings with a submanifold

theorem Manifold.HypersurfaceFamily.HasSncWith.exists_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {Y : Set M} {c : ℕ} (h : HasSncWith ψ F Y c) {a : M} (ha : a ∈ Y) : ∃ (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n) (cidx : { j : F.ι // a ∈ F.hyp j } → Fin n), IsAdaptedChart ψ Y φ σ ∧ IsSncChartAt ψ F φ a cidx

At every point of Y there is a chart adapted to Y which is an snc chart of F [Kol07, Definition 24 (4)].

The support of the total transform

theorem Manifold.HypersurfaceFamily.support_totalTransform {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) (F : HypersurfaceFamily M) (hπ : Continuous π) (hF : ∀ (j : F.ι), IsClosed (F.hyp j)) : (totalTransform π Y F).support = π ⁻¹' F.support ∪ π ⁻¹' Y

For a continuous π and closed components, the support of the total transform is the preimage of the support together with the exceptional divisor: the set of points of Hironaka's red(f⁻¹(E) ∪ f⁻¹(D)) [Hir64, Main Theorem II'(N) (iii), p. 156] (from the inclusions between the strict transform of a closed set and its preimage).

Restricting an snc chart to an open set

theorem Manifold.HypersurfaceFamily.IsSncChartAt.restrOpen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} {φ : OpenPartialHomeomorph M.carrier E} {a : M.carrier} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ₀ F φ a c) {s : Set M.carrier} (hs : IsOpen s) (has : a ∈ s) : IsSncChartAt ψ₀ F (φ.restrOpen s hs) a c

The restriction of an snc chart at a to an open set containing a is an snc chart at a (the analogue of IsAdaptedChart.restrOpen').

Hironaka's normal crossings at the level of stalks

def AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} : M.IdealSheaf → (D : M.IdealSheaf) → Prop

Hironaka's normal crossings [Hir64, Definition 2, p. 141] at the level of stalks: at every point x of the subspace D, some regular system of parameters (z_1, …, z_n) of 𝒪_{M,x} (n generators of the maximal ideal, n the Krull dimension — the two clauses of the Hironaka library's regular systems of parameters, spelled out as in IsNormalCrossingsDivisor) contains an equation of each minimal prime of E_x and equations for D_x.

This body is stalk-local: "each irreducible component of E through x" is read as a minimal prime of the analytic stalk E_x, a local branch, whereas Hironaka quantifies over the global irreducible components of E containing x, so that his normal crossings is simple normal crossings (every global component smooth). The two readings differ on analytic spaces: the real nodal cubic y² = x²(1 + x) in ℝ² satisfies this body at every point (two smooth branch parameters at the node) while its one global component is singular there. On schemes they coincide, which is why the scheme form of this body is named AlgebraicGeometry.Scheme.IdealSheafData.IsSncBoundary (Hironaka.Sequence.isSncBoundary_iff_isSnc_componentFamily: Zariski-local components are the global ones). The analytic main theorems use IdealSheaf.IsSncBoundary and IdealSheaf.IsSncBoundaryWith instead; the ideal sheaf of a simple normal crossings family does satisfy this body (Hironaka/Manifold/Snc/Dictionary.lean).

Equations

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

def AnalyticManifold.IdealSheaf.HasOnlyNormalCrossings {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} : M.IdealSheaf → Prop

Hironaka's Definition 2 with D = M ("we simply say that E has only normal crossings"): HasOnlyNormalCrossingsWith E ⊥, the zero ideal sheaf ⊥ being the ideal of M itself. The stalk-local caveat of HasOnlyNormalCrossingsWith applies; the analytic main theorems use IdealSheaf.IsSncBoundary instead.

Equations

• E.HasOnlyNormalCrossings = E.HasOnlyNormalCrossingsWith ⊥