The reduced ideal sheaf of an snc divisor: coherence and stalks

Hironaka's red of the support of a simple normal crossings divisor F is the ideal sheaf whose stalks are the vanishing ideals of |F| (vanishingStalk); this module shows that these stalks have local generators — so that HypersurfaceFamily.idealSheaf takes its first branch — and computes them: at a point a with snc chart φ and indices c, the vanishing ideal of |F| at every point b of the chart's source near a is generated by the single germ ∏_{j : a ∈ E^j} z_{c j} (Hironaka's "the ideal of each irreducible component of E is generated by one of the z_i" [Hir64, Definition 2, p. 141]; Bierstone–Milman's normal-crossings divisor, locally z_1 ⋯ z_k = 0, [BM97, Theorem 1.10]). The proof is the classical one, made algebraic:

• near a the support is the union of the finitely many components through a (local finiteness and closedness of the components: IsSnc.exists_nhds_support_eq);
• a germ vanishing on the coordinate hyperplane E^j = {z_k = 0} near b ∈ E^j lies in the kernel of the restriction of germs to the submanifold E^j, which is (z_k) (IsClosedSubmanifold.ker_restrictStalk_eq_span with the one-index adapted chart); off E^j the coordinate z_k is a unit;
• the coordinates vanishing at b are prime elements of the regular local ring 𝒪_{M,b} (𝒪_b/(z_k) is regular, IsRegularLocalRing.quotient_span_singleton, because z_k ∈ 𝔪_b ∖ 𝔪_b²: its linear part is the unit vector e_k), and no coordinate divides another (again by the linear parts), so a germ divisible by each of them is divisible by their product (IsLocalRing.prod_dvd_of_prime_of_not_dvd).

Consequences: the stalks of F.idealSheaf are the vanishing ideals (stalkIdeal_idealSheaf), its cosupport is |F| (cosupport_idealSheaf), and in an snc chart the stalk at the chart's point is (∏_{j : a ∈ E^j} z_{c j}) (stalkIdeal_idealSheaf_eq_span_prod). These are the inputs of the dictionary with Hironaka's predicates (Hironaka/Manifold/Snc/Dictionary.lean) and of the monomial description of the boundary along a resolution.

Vanishing ideals: monotonicity and the kernel of the restriction of germs

theorem Manifold.vanishingStalk_anti {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Z Z' : Set M} (h : Z ⊆ Z') (x : M) : vanishingStalk Z' x ≤ vanishingStalk Z x

A germ vanishing on Z' near x vanishes on any Z ⊆ Z' near x.

theorem Manifold.IsClosedSubmanifold.ker_restrictStalk_eq_vanishingStalk {𝕜 : 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) {a : M} (ha : a ∈ Y) : RingHom.ker (hY.restrictStalk ⟨a, ha⟩) = vanishingStalk Y a

The kernel of the restriction of germs to the closed submanifold Y at a ∈ Y is the vanishing ideal of Y at a.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.isAdaptedChart_hyp {𝕜 : 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} (hc : IsSncChartAt ψ F φ a c) (j : { j : F.ι // a ∈ F.hyp j }) : IsAdaptedChart ψ (F.hyp ↑j) φ (singleEmb (c j))

An snc chart at a is a chart adapted to each component through a, with the single index of that component (singleEmb).

theorem Manifold.HypersurfaceFamily.IsSncChartAt.mem_vanishingStalk_hyp_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} (hF : IsSnc ψ F) (hc : IsSncChartAt ψ F φ a c) (j : { j : F.ι // a ∈ F.hyp j }) {b : M} (hb : b ∈ φ.source) (hbj : b ∈ F.hyp ↑j) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk b)) : s ∈ vanishingStalk (F.hyp ↑j) b ↔ coord E ψ φ ⋯ hb (c j) ∣ s

At a point b of a component through a, a germ vanishes on that component near b iff the component's coordinate divides it.

The coordinates of a chart as elements of the stalk: units, primes, non-divisibility

theorem Manifold.coord_mem_maximalIdeal_of_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ φ.source) {k : Fin n} (h0 : ψ (↑φ b) k = 0) : coord E ψ φ hφ hb k ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk b)

A coordinate vanishing at b lies in the maximal ideal of the stalk.

theorem Manifold.isUnit_coord_of_ne_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ φ.source) {k : Fin n} (h0 : ψ (↑φ b) k ≠ 0) : IsUnit (coord E ψ φ hφ hb k)

A coordinate not vanishing at b is a unit of the stalk.

theorem Manifold.linearPart_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ φ.source) (k i : Fin n) : (linearPart E ψ φ hφ hb) (coord E ψ φ hφ hb k) i = if i = k then 1 else 0

The linear part of the coordinate z_k is the unit vector e_k.

theorem Manifold.coord_notMem_maximalIdeal_sq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ φ.source) {k : Fin n} : coord E ψ φ hφ hb k ∉ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk b) ^ 2

A coordinate vanishing at b is not in 𝔪_b².

theorem Manifold.prime_coord_of_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ φ.source) {k : Fin n} (h0 : ψ (↑φ b) k = 0) : Prime (coord E ψ φ hφ hb k)

A coordinate vanishing at b is a prime element of the regular local ring 𝒪_{M,b}: the quotient by it is regular (IsRegularLocalRing.quotient_span_singleton), hence a domain.

theorem Manifold.not_coord_dvd_coord_of_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ φ.source) {k l : Fin n} (hk0 : ψ (↑φ b) k = 0) (hkl : k ≠ l) : ¬coord E ψ φ hφ hb k ∣ coord E ψ φ hφ hb l

Two distinct coordinates vanishing at b do not divide each other in 𝒪_{M,b}: their linear parts are distinct unit vectors.

The support near a point

theorem Manifold.HypersurfaceFamily.IsSnc.exists_nhds_support_eq {𝕜 : 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) : ∃ (V : Set M), IsOpen V ∧ a ∈ V ∧ ∀ x ∈ V, x ∈ F.support ↔ ∃ (j : F.ι), a ∈ F.hyp j ∧ x ∈ F.hyp j

Near a point a the support of an snc divisor is the union of the components through a (local finiteness and closedness).

The vanishing ideal of the support in an snc chart

theorem Manifold.HypersurfaceFamily.IsSncChartAt.vanishingStalk_support_eq {𝕜 : 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} (hF : IsSnc ψ F) (hc : IsSncChartAt ψ F φ a c) {V : Set M} (hV : IsOpen V) (hVs : ∀ x ∈ V, x ∈ F.support ↔ ∃ (j : F.ι), a ∈ F.hyp j ∧ x ∈ F.hyp j) {b : M} (hb : b ∈ φ.source) (hbV : b ∈ V) (S : Finset F.ι) (hS : ∀ (j : F.ι), j ∈ S ↔ a ∈ F.hyp j) : vanishingStalk F.support b = Ideal.span {∏ j ∈ S.attach, coord E ψ φ ⋯ hb (c ⟨↑j, ⋯⟩)}

In an snc chart φ at a with indices c, on a neighbourhood V of a where the support is the union of the components through a, the vanishing ideal of the support at any b ∈ V ∩ φ.source is generated by the product of the coordinates of the components through a (indexed by any finset S of exactly those components) ([Hir64, Definition 2, p. 141]; [BM97, Theorem 1.10]).

Coherence of the vanishing ideal sheaf of the support, and its stalks

theorem Manifold.HypersurfaceFamily.IsSnc.hasLocalGenerators_vanishingStalk_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) : IdealSheaf.HasLocalGenerators fun (x : ↑↧M) => vanishingStalk F.support x

The vanishing ideals of the support of an snc divisor have local generators: near a, the product of the coordinates of the components through a (Hironaka's "the ideal of each irreducible component of E is generated by one of the z_i", [Hir64, Definition 2, p. 141]).

theorem Manifold.HypersurfaceFamily.IsSnc.stalkIdeal_idealSheaf {𝕜 : 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) (x : M) : F.idealSheaf.stalkIdeal x = vanishingStalk F.support x

The stalks of the reduced ideal sheaf of an snc divisor are the vanishing ideals of its support.

theorem Manifold.HypersurfaceFamily.IsSnc.cosupport_idealSheaf {𝕜 : 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) : F.idealSheaf.support = F.support

The cosupport of the reduced ideal sheaf of an snc divisor is its support.

theorem Manifold.HypersurfaceFamily.IsSnc.stalkIdeal_idealSheaf_eq_span_prod {𝕜 : 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} (hF : IsSnc ψ F) (hc : IsSncChartAt ψ F φ a c) : F.idealSheaf.stalkIdeal a = Ideal.span {∏ j ∈ ⋯.toFinset.attach, coord E ψ φ ⋯ ⋯ (c ⟨↑j, ⋯⟩)}

In an snc chart at a the reduced ideal sheaf of the divisor is generated at a by the product of the coordinates of the components through a ([Hir64, Definition 2, p. 141]; [BM97, Theorem 1.10]).