From formal to Zariski-local equality of ideal sheaves

Kollár's remark on Krull's intersection theorem in [Kol07, Definition 55]: in a Noetherian local ring (R, 𝔪) every ideal I equals ∩_s (I + 𝔪^s), so two subschemes Z, W ⊂ X with the same completion at x agree on an open neighbourhood U of x ("such that Z ∩ U = W ∩ U"). Kollár uses it to pass from the identities (91.1′–4′) between completions to an open neighbourhood U(p) ∋ (p, p) ([Kol07, 95], the proof of Theorem 92).

• stalkIdeal_eq_of_map_adicCompletion_eq: on a locally Noetherian scheme, two ideal sheaves with equal completions at q have equal stalks at q: R → R̂ is faithfully flat for a Noetherian local ring, so extension of ideals to the completion is injective (IsLocalRing.map_adicCompletion_injective).
• exists_comap_eq_of_stalkIdeal_eq: two ideal sheaves with equal stalks at q agree on an open neighbourhood of q: on an affine V ∋ q the ideals J(V), J'(V) are finitely generated (Noetherian) and have the same localization at the prime of q, so they agree after inverting some s ∉ 𝔭_q (exists_mem_map_eq_map_of_localization, Adapted.lean), i.e. on the basic open D(s) ∋ q; ideal sheaves on D(s) are determined by their stalks (ext_stalkIdeal).
• exists_comap_eq_of_map_adicCompletion_eq: the composite, Kollár's statement.

Used to pass from the formal equivalence of two hypersurfaces of maximal contact to their equivalence on an étale neighbourhood (Hironaka/Resolution/Algebraic/MaximalContact/AgreeOnSpread.lean).

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_eq_of_map_adicCompletion_eq {W : Scheme} [IsLocallyNoetherian W] (J J' : W.IdealSheafData) (q : ↥W) (h : Ideal.map (algebraMap (↑(W.presheaf.stalk q)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(W.presheaf.stalk q)) ↑(W.presheaf.stalk q))) (J.stalkIdeal q) = Ideal.map (algebraMap (↑(W.presheaf.stalk q)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(W.presheaf.stalk q)) ↑(W.presheaf.stalk q))) (J'.stalkIdeal q)) : J.stalkIdeal q = J'.stalkIdeal q

Two ideal sheaves with equal completions at q have equal stalks at q (Krull's intersection theorem, [Kol07, Definition 55], through the faithful flatness of R → R̂).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_comap_eq_of_stalkIdeal_eq {W : Scheme} [IsLocallyNoetherian W] (J J' : W.IdealSheafData) (q : ↥W) (h : J.stalkIdeal q = J'.stalkIdeal q) : ∃ (V : W.Opens), q ∈ V ∧ J.comap V.ι = J'.comap V.ι

Two ideal sheaves on a locally Noetherian scheme with equal stalks at q agree on an open neighbourhood of q (the geometric form of Krull's intersection theorem in [Kol07, Definition 55]; spreading out finitely many generators).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_comap_eq_of_map_adicCompletion_eq {W : Scheme} [IsLocallyNoetherian W] (J J' : W.IdealSheafData) (q : ↥W) (h : Ideal.map (algebraMap (↑(W.presheaf.stalk q)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(W.presheaf.stalk q)) ↑(W.presheaf.stalk q))) (J.stalkIdeal q) = Ideal.map (algebraMap (↑(W.presheaf.stalk q)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(W.presheaf.stalk q)) ↑(W.presheaf.stalk q))) (J'.stalkIdeal q)) : ∃ (V : W.Opens), q ∈ V ∧ J.comap V.ι = J'.comap V.ι

Two ideal sheaves with equal completions at q agree on an open neighbourhood of q ([Kol07, Definition 55]; used as "(91.1′–4′) also hold in an open neighborhood U(p) by (55)" in [Kol07, 95]).