Families of divisors with simple normal crossings at a point

[Kol07, Definition 24] at a point x, for a family E : ι → X.IdealSheafData of closed subschemes: local coordinates z : Fin n → 𝒪_{X,x} (a regular system of parameters, Hironaka.Scheme.Snc.Coordinates) and an injective assignment c of a coordinate to each component through x with (E i)_x = (z_{c(i)}). The predicate DivisorFamily.IsSncAt is exactly this data, so the lemmas here take the data as explicit hypotheses.

• Kollár's (1)–(2): a component not through x has stalk ⊤ (stalkIdeal_eq_top_of_notMem_support), a component through x has stalk (z_j) (stalkIdeal_eq_top_or_exists_eq_span).
• Kollár's (3): distinct components through x have distinct stalks (stalkIdeal_ne_of_ne, from span_singleton_ne_of_ne).
• Each component is a smooth divisor (isSmoothDivisor_of_snc_data): its generator z_{c(i)} lies in 𝔪_x ∖ 𝔪_x².
• The empty family, a single smooth divisor (complete its local generator to a regular system of parameters), and an injective reindexing of a family all have the snc data.
• The product of the stalks of all components is the monomial ideal (∏_{i : x ∈ E i} z_{c(i)}) (prod_stalkIdeal_eq_span; [Hau14, Remark 3.16, Proposition 3.17, Remark 3.20]).

theorem AlgebraicGeometry.stalkIdeal_eq_top_or_exists_eq_span {X : Scheme} {ι : Type u_1} {E : ι → X.IdealSheafData} {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} (c : { i : ι // x ∈ (E i).support } → Fin n) (hc : ∀ (i : { i : ι // x ∈ (E i).support }), (E ↑i).stalkIdeal x = Ideal.span {z (c i)}) (i : ι) : (E i).stalkIdeal x = ⊤ ∨ ∃ (j : Fin n), (E i).stalkIdeal x = Ideal.span {z j}

Kollár (1)–(2): every component either misses x (stalk ⊤) or has stalk (z_j) at x.

theorem AlgebraicGeometry.stalkIdeal_ne_of_ne {X : Scheme} {ι : Type u_1} {E : ι → X.IdealSheafData} {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} [IsRegularLocalRing ↑(X.presheaf.stalk x)] (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x)) (c : { i : ι // x ∈ (E i).support } → Fin n) (hcinj : Function.Injective c) (hc : ∀ (i : { i : ι // x ∈ (E i).support }), (E ↑i).stalkIdeal x = Ideal.span {z (c i)}) {i i' : ι} (hi : x ∈ (E i).support) (hi' : x ∈ (E i').support) (hne : i ≠ i') : (E i).stalkIdeal x ≠ (E i').stalkIdeal x

Kollár (3): distinct components through x have distinct stalks.

theorem AlgebraicGeometry.isSmoothDivisor_of_snc_data {X : Scheme} {ι : Type u_1} (E : ι → X.IdealSheafData) (hreg : ∀ (i : ι), IsRegular (E i).subscheme) (h : ∀ (x : ↥X), ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x)) ∧ ∃ (c : { i : ι // x ∈ (E i).support } → Fin n), Function.Injective c ∧ ∀ (i : { i : ι // x ∈ (E i).support }), (E ↑i).stalkIdeal x = Ideal.span {z (c i)}) (hX : ∀ (x : ↥X), IsRegularLocalRing ↑(X.presheaf.stalk x)) (i : ι) : IsSmoothDivisor (E i)

Each component of a family with the snc data at every point of a regular scheme is a smooth divisor: at x ∈ E i the generator z_{c(i)} lies in 𝔪_x ∖ 𝔪_x².

theorem AlgebraicGeometry.exists_snc_data_of_injective {X : Scheme} {ι : Type u_1} {E : ι → X.IdealSheafData} {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} {κ : Type u_2} {F : κ → X.IdealSheafData} (φ : κ → ι) (hφ : Function.Injective φ) (hF : ∀ (j : κ), F j = E (φ j)) (c : { i : ι // x ∈ (E i).support } → Fin n) (hcinj : Function.Injective c) (hc : ∀ (i : { i : ι // x ∈ (E i).support }), (E ↑i).stalkIdeal x = Ideal.span {z (c i)}) : ∃ (c' : { j : κ // x ∈ (F j).support } → Fin n), Function.Injective c' ∧ ∀ (j : { j : κ // x ∈ (F j).support }), (F ↑j).stalkIdeal x = Ideal.span {z (c' j)}

The snc data transport along an injective reindexing (drop indices, keep the coordinates).

theorem AlgebraicGeometry.exists_snc_data_of_isEmpty {X : Scheme} {ι : Type u_1} {x : ↥X} [IsEmpty ι] [IsRegularLocalRing ↑(X.presheaf.stalk x)] (E : ι → X.IdealSheafData) : ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x)) ∧ ∃ (c : { i : ι // x ∈ (E i).support } → Fin n), Function.Injective c ∧ ∀ (i : { i : ι // x ∈ (E i).support }), (E ↑i).stalkIdeal x = Ideal.span {z (c i)}

The empty family has the snc data at every point of a regular scheme.

theorem AlgebraicGeometry.exists_snc_data_of_unique {X : Scheme} {ι : Type u_1} {x : ↥X} [Unique ι] [IsRegularLocalRing ↑(X.presheaf.stalk x)] (E : ι → X.IdealSheafData) (D : X.IdealSheafData) (hE : ∀ (i : ι), E i = D) (hD : IsSmoothDivisor D) : ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x)) ∧ ∃ (c : { i : ι // x ∈ (E i).support } → Fin n), Function.Injective c ∧ ∀ (i : { i : ι // x ∈ (E i).support }), (E ↑i).stalkIdeal x = Ideal.span {z (c i)}

A family with a single component, a smooth divisor D, has the snc data at every point of a regular scheme: at x ∈ D complete the local generator of D to a regular system of parameters; at x ∉ D any regular system of parameters serves.

theorem AlgebraicGeometry.prod_stalkIdeal_eq_span {X : Scheme} {ι : Type u_1} {E : ι → X.IdealSheafData} {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} [Fintype ι] [DecidablePred fun (i : ι) => x ∈ (E i).support] (c : { i : ι // x ∈ (E i).support } → Fin n) (hc : ∀ (i : { i : ι // x ∈ (E i).support }), (E ↑i).stalkIdeal x = Ideal.span {z (c i)}) : ∏ i : ι, (E i).stalkIdeal x = Ideal.span {∏ i : { i : ι // x ∈ (E i).support }, z (c i)}

The product of the stalks of all components — the ideal of the union of the components, taken as a scheme — is the monomial ideal generated by ∏_{i : x ∈ E i} z_{c(i)}; the components not through x contribute the factor ⊤ ([Hau14, Remark 3.16, Proposition 3.17, Remark 3.20]).