Stalk identities of ideal sheaves spread to a neighbourhood #
An identity J_x = (g_1, …, g_k) between the stalk of a locally finitely generated ideal sheaf
J and the ideal spanned by the germs of finitely many sections g_i over an open set U ∋ x
holds at every point of an open neighbourhood W ⊆ U of x
(IdealSheaf.exists_opens_stalkIdeal_eq_span). Both sides are finitely generated: the local
generators f_j of J near x are combinations f_j = ∑ a_{ji} g_i at x, and each g_i has
the germ of a section of J at x; the coefficients a_{ji} are germs of sections, and an
identity of germs is an identity of sections on a smaller open set (TopCat.Presheaf.germ_eq),
so on the common open set the two ideals of germs coincide at every point. Also: finitely many
germs at a point are the germs of sections over one common open set (exists_sections_of_germs).
Stated for ideal sheaves over any sheaf of commutative rings; the step shared by the two dictionary
theorems isNonsingular_iff and hasOnlyNormalCrossingsWith_idealSheaf_iff (a stalk identity at a
point of a chart is spread to a neighbourhood on which the chart is adapted). Not in the sources;
standard.
Finitely many germs at x are the germs at x of sections over one open neighbourhood of
x.
A section whose germ at x lies in J_x lies in J on a neighbourhood of x.
If the stalk J_x is spanned by the germs of finitely many sections g_i over U ∋ x, the
same holds at every point of an open neighbourhood W ⊆ U of x.