The ideal of a simple normal crossing divisor is invertible

[Kol07, Theorem 35 (2)] says Π^* I is the ideal sheaf of a simple normal crossing divisor (IsIdealOfSncDivisor: ∏ⁱ (E^i)^{a_i} for an snc family E); the uses of the principalization read this as invertibility — an effective Cartier divisor — as the proof of [Kol07, Corollary 22] does ("its ideal sheaf I is not locally principal at η_X, and therefore some blow-up centre must contain η_X"; a Cartier divisor as centre gives a trivial blow-up, [Kol07, Warning 20]). The bridge is [Kol07, Definition 24 (1)–(3)]: at a point of a member E^i of an snc family the stalk of E^i is (z_{c(i)}) for a member z_{c(i)} of a regular system of parameters (IsSncAt), a nonzerodivisor of the regular local ring 𝒪_{X,x} (a domain, isDomain_of_isRegularLocalRing of Hironaka.Algebra.Local.Regular); off E^i the stalk is the unit ideal. On a locally Noetherian scheme the stalkwise criterion isInvertible_of_forall_stalkIdeal_eq_span of Hironaka.Scheme.IdealSheaf.Invertible then gives IsInvertible, and products and powers of invertible ideal sheaves are invertible (IsInvertible.mul, isInvertible_pow).

• isSmoothDivisor_component_of_isSnc: each member of an snc family on a scheme smooth over a field is a smooth divisor (isSmoothDivisor_of_snc_data of Hironaka.Scheme.Snc.Family read on a DivisorFamily; BD.isSmoothDivisor_component is its special case for the boundary of a triple);
• isInvertible_of_isSmoothDivisor: a smooth divisor is invertible;
• IsSnc.isInvertible_component; AlgebraicGeometry.Scheme.IdealSheafData.IsIdealOfSncDivisor.isInvertible.

Used by Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36 (clause (2) of Theorem 35 as local principality) and Hironaka.Resolution.Algebraic.BoundaryClearing.Restriction.

Sources: [Kol07, Theorem 35 (2); Definition 24; Warning 20; Corollary 22]; [TSPA, Tag 01WS].

theorem Hironaka.Snc.isSmoothDivisor_component_of_isSnc {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} (hF : F.IsSnc) (j : F.ι) : AlgebraicGeometry.IsSmoothDivisor (F.component j)

[Kol07, Definition 24 (1)–(2)] on a divisor family: each member of a simple normal crossing family on a scheme smooth over k is a smooth divisor (regular, and locally (z_{c(i)} = 0) for a member of a regular system of parameters) — isSmoothDivisor_of_snc_data with the family's own snc data (the general form of BD.isSmoothDivisor_component, which is the case F = T.E of a triple T).

theorem Hironaka.Snc.isInvertible_of_isSmoothDivisor {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {D : X.IdealSheafData} (hD : AlgebraicGeometry.IsSmoothDivisor D) : D.IsInvertible

A smooth divisor on a locally Noetherian scheme smooth over k is an effective Cartier divisor ([Kol07, Warning 20]; [TSPA, Tag 01WS]) — at a point of the divisor its stalk is (a) with a ∈ 𝔪_x ∖ 𝔪_x², a nonzerodivisor of the regular local (hence integral) stalk; off the divisor the stalk is the unit ideal (1).

theorem Hironaka.Snc.IsSnc.isInvertible_component {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} (hF : F.IsSnc) (j : F.ι) : (F.component j).IsInvertible

Each member of a simple normal crossing family on a locally Noetherian scheme smooth over k is an effective Cartier divisor.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsIdealOfSncDivisor.isInvertible {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [Smooth f] {I : X.IdealSheafData} (h : I.IsIdealOfSncDivisor) : I.IsInvertible

[Kol07, Theorem 35 (2)] read as the proof of [Kol07, Corollary 22] does: the ideal sheaf of an effective divisor supported on a simple normal crossing family, ∏ⁱ (E^i)^{a_i}, is invertible — a finite product of powers of invertible ideal sheaves.