The ideal sheaf of a global section #
[Kol07, Theorem 80 (2)] is stated for "a section h_x ∈ H⁰(U_x, L ⊗ MC(I)) with zero divisor
H_x := (h_x = 0)": the hypersurface is given by an equation. Hypersurfaces are ideal sheaves in
this library, so the equation h has to become the ideal sheaf it generates: principal h is the
ideal sheaf whose ideal on every affine open U is the principal ideal (h|_U); its stalk at x
is (germ_x h), and h ∈ H⁰(X, J) for an ideal sheaf J (a section of J) is the inclusion
principal h ≤ J. The line bundle L of the printed statement is trivialized on the open U_x
the theorem produces, so a section of L ⊗ MC(I) there is a section of MC(I).
Only the definition lives here; its characterizing lemmas (principal_ideal,
stalkIdeal_principal, principal_le_iff, principal_one, ord_principal) and the proof of
Theorem 80 (2) are in Hironaka/Resolution/Algebraic/MaximalContact/Existence.lean.
The zero divisor (h = 0) of a section, as in [Kol07, Theorem 80 (2)]: the ideal sheaf
generated by a global section h, with (h|_U) on every affine open U. It is Mathlib's ideal
sheaf ofIdealTop of the principal ideal (h) of the global sections.